定理証明手習い (35) 9 ルールを変えるには

8章では関数の全域性の主張の作り方をやりました
9章では定理の帰納法の作り方をやります
具体的に言うと、list-inductionとかstar-inductionに当たるものを作るということです
いやちょっと違うな

list-inductionやstar-inductionと定理から作られる、主張そのものを作るんですね

list-inductionやstar-inductionは種で、主張じゃないですね
帰納法が作れれば定理を証明することができます

なんですが

まだ、関数add-atomsの定義を理解できていません

この再帰ね

(defun add-atoms (x ys)
  (if (atom x)
    (if (member? x ys)
        ys
        (cons x ys))
    (add-atoms (car x)
               (add-atoms (cdr x) ys))))

アトムを全部一列に並べてリストにする、って書くと簡単なんですけど
コードを１行１行追っていくとけっこう難しいんですよね
ミクロに見ればそうなりそうな気がするけど、
全体が本当にそうなっているかというとちょっと心もとないっていうか

ちょっと久しぶりにアレやってみよう
アレっていっちゃうのがもうオッサンですね！

  (add-atoms '((a . b) . (c . a)) '(d a e))
= (add-atoms '(a . b) (add-atoms '(c . a) '(d a e)))
= (add-atoms '(a . b) (add-atoms 'c (add-atoms 'a '(d a e))))
= (add-atoms '(a . b) (add-atoms 'c '(d a e)))
= (add-atoms '(a . b) (cons 'c '(d a e)))
= (add-atoms '(a . b) '(c d a e))
= (add-atoms 'a (add-atoms 'b '(c d a e)))
= (add-atoms 'a (cons 'b '(c d a e)))
= (add-atoms 'a '(b c d a e))
= '(b c d a e)

ふむ
うまく行くのはわかった
でも、うまく行き「そう」っていう感じはまだしてない
ほんとにこれで木の要素が一列になってならんでくれるのか

言葉にしてみよう

add-atomsは
リストをcarとcdrに分けて
まずcdrの要素を一列のリストにして
その結果とcarを一列のリストにする
ような関数です！

（いろいろ省いてる）

でもまだ違うなあ
なんで一列になるのかがピンときてない

ん、cdrに注目するといいのかな

add-atomsは
木ををcdrがアトムになるまで分解して、リストにconsしていく関数です
cdrの分が終わったらcarについても同じことを行います

省きすぎ大ざっぱすぎでどっちかというともうほとんど間違ってる気もするけど
一列になりそうな気はするようになった

こういう書き方は何かのときに使えるパターンではあると思うんだけど
適用範囲は木を線形リストにならすときだけかな？
普通に木を見て回るときにはあまり使わない？

数字の木の合計を求めるなら、普通はこうで

(define (sum-tree t)
  (if (atom? t)
      t
      (+ (sum-tree (car t)) 
         (sum-tree (cdr t)))))

こうじゃないよな・・・答えは合うけど

(define (sum-tree2 t)
  (define (st t sum)
    (if (atom? t)
        (+ t sum)
        (st (car t) (st (cdr t) sum))))
  (st t 0))

こっちの書き方にメリットってあるかな？
スタックは余計に消費しそうだし

帰納法にはまったく触れてませんが今日はここまで

9章まで来て、細切れの時間でちょっとずつ考えるだけだと頭が整理しきれなくなってきてます
8章と行ったり来たりです
ちょっとまとまった時間を取らないとかなあ

（行ったり来たりしてる間にやっと気づいたんだけどp.107の下の方で句点が抜けてるらしいところが）
（正誤表がGitHub Issuesにあるとは言え勝手にNew Issueをあげたりするところじゃないんだろうな）