定理証明手習い (49) align
align
か
それだ見覚えあったのは
確かそのときも全関数であることの証明だった
(defun align (x)
(if (atom x)
x
(if (atom (car x))
(cons (car x) (align (cdr x)))
(align (rotate x)))))
うんうん
前に出てきたalign
もなんだかよくわからない関数だった
でもよく見るとrotate
をコアとして
rotate
がうまく動かないケースをそれっぽく動くようにしてる、っていう感じはする
(size x)
は尺度として適切でしょうか?
そういう話ね
なるほど
全域性についての主張の作り方と
帰納法の作り方をやったから
最後に尺度の作り方をやろうってことだな
見え見えだけど話に乗って(size x)
で証明を進める
(if (atom x)
't
(if (atom (car x))
't
(< (size (rotate x)) (size x))))
まで来たところで(rotate x)
を展開かな?と思ったら
cons/car+cdr
を2回使うとどうなりますか?
何するの?
あー(rotate (cons (cons x y) z))
の形に寄せていくのか
洞察:繰り返しを避けるために補助定理を用意しよう
これ前に出てこなかったっけ?
大事なことだから2回言った?
洞察:帰納法の補助定理を作るべし
少し違った
大事なのは間違いないけど
しかしここで行き止まり
rotate
してもコンスの回数が変わらないことは章の冒頭で確認済み
たぶん、
(size x)
は適切な尺度ではないんですよ。
結局尺度っていうのは証明に使えるようなうまい式を探して書く、ってことなんだな