kb84tkhrのブログ

何を書こうか考え中です あ、あと組織とは関係ないってやつです 個人的なやつ

定理証明手習い (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)は適切な尺度ではないんですよ。

結局尺度っていうのは証明に使えるようなうまい式を探して書く、ってことなんだな