定理証明手習い (93) しゅくだい
「
(reverse (reverse x))
がどんなリストについてもx
になるか」…(略)…読者への宿題にしておきます。
付録Cやってるあいだに証明も忘れかけてる気がするのでちょうどいいおさらい
最初は、これを証明すればいいかな、と思ったんですけどね
(defun reverse2 (x res)
(if (atom x)
res
(reverse2 (cdr x) (cons (car x) res))))
(defun reverse (x)
(reverse2 x '()))
(dethm reverse/reverse (x)
(equal (reverse (reverse x)) x))
証明するとうまく行きません
よく見たらx
が'()
以外のアトムだとそもそもreverse/reverse
が成り立ってません
そんなのは定義域じゃありませんといいたいところですがそうも行かず
ということでバグ発見しました!ブラボー証明(そうか?
ところで、付録Cやってみて気がついたんですが、上のように直接定義してやると
dethm
もそのまま評価できるんですね
J-Bob/prove
とかJ-Bob/define
の中だけの存在だと思ってました
J-Bob/langの定義中にはdethm
はでてこないのになんでマクロが定義されてるんだろう、と思ったら
こんな感じです
> (reverse/reverse '(a b c))
t
で、
> (reverse/reverse 'a)
nil
だめじゃん、と
reverse/reverse
の形は変えたくないから、(reverse 'a)
が'a
になるようにしましょうか
reverse
のほうで吸収するのが自然ですかね
こうかな
(defun reverse (x)
(if (atom x)
x
(reverse2 x '())))
どれ
> (reverse/reverse '(a b c))
t
> (reverse/reverse 'a)
t
おk
(J-Bob/prove (prelude)
'(((defun reverse2 (x res)
(if (atom x)
res
(reverse2 (cdr x) (cons (car x) res))))
(size x))
((defun reverse (x)
(if (atom x)
x
(reverse2 x '())))
nil)
ここまでの全域性の証明は後回しにします
まずは定理の証明から
((dethm reverse/reverse (x)
(equal (reverse (reverse x)) x))
(list-induction x)
reverse
が入れ子になってるけど、reverse2
は普通にリストをたどる再帰だから
list-induction
でいいのかなあ
一応そうだと信じでるけどちょっと自信がないところもある
ここでの主張はこう
(if (atom x)
(equal (reverse (reverse x)) x)
(if (equal (reverse (reverse (cdr x))) (cdr x))
(equal (reverse (reverse x)) x)
't))
A部から
((A 1 1) (reverse x))
((A 1 1) (if-nest-A (atom x) x (reverse2 x '())))
((A 1) (reverse x))
((A 1) (if-nest-A (atom x) x (reverse2 x '())))
((A) (equal-same x))
すんなり't
に
(if (atom x)
't
(if (equal (reverse (reverse (cdr x))) (cdr x))
(equal (reverse (reverse x)) x)
't))
ではE部
E A
の内側のreverse
から展開していく感じかな
まずはreverse
をreverse2
に
((E A 1 1) (reverse x))
((E A 1 1) (if-nest-E (atom x) x (reverse2 x '())))
↓
(if (atom x)
't
(if (equal (reverse (reverse (cdr x))) (cdr x))
(equal (reverse (reverse2 x '())) x)
't))
そしてreverse2
を展開
((E A 1 1) (reverse2 x '()))
((E A 1 1) (if-nest-E (atom x) '() (reverse2 (cdr x) (cons (car x) '()))))
↓
(if (atom x)
't
(if (equal (reverse (reverse (cdr x))) (cdr x))
(equal (reverse (reverse2 (cdr x)
(cons (car x) '()))) x)
't))
どうもうまく行きそうな気がしませんね
繰り返しタイプの再帰だったりするのがよくないのかなあ?
でもそのために不自然な書き方や非効率な書き方をするのでは本末転倒だしなあ
もうちょっとやってみよう
いじるとしたら前提のほうじゃないか
((E Q 1 1) (reverse (cdr x)))
↓
(if (atom x)
't
(if (equal (reverse (if (atom (cdr x))
(cdr x)
(reverse2 (cdr x) '())))
(cdr x))
(equal (reverse (reverse2 (cdr x)
(cons (car x) '()))) x)
't))
どうにかなる気がしませんね
作戦を考える必要がありそうです