定理証明手習い(a2) しゅくだい(10)
再考します、と言ってはみたもののイメージはつかめてなかったり
(reverse/reverse
だって証明はもっと簡単にできるイメージだった・・・)
再掲
reverse2/reverse2 の証明は、私も考えてみましたが、累積変数を使った定義と逆consを使った定義とが同じである、ということを証明してしまうのが一番易しいようです。でも、末尾再帰になっている関数を証明する技法を考えてみるのも面白そうですね。
— SUHARA Hiromichi (@suharahiromichi) 2018年4月28日
同じである、というのはふたつのバージョンのreverse
が同じ、ということでしょう
(reverse/reverse
とreverse2/reverse2
が同じということではなくて)
「同じ」というのは一方を変換して他方と同じ形にできる、ってことかな
それとも(equal (reverse x) (reverse' x))
を証明するのかな
似てるようだけど違う
同じであるということを証明するにはまず、同じでないといけないわけですが(当然
ドット対が出てくると同じになりません(涙
ここは何か値が帰ればいいことにしておいて進む
これはダメだったか・・・
reverse/reverse
が成り立つようにしようとすると、ドット対の情報も
残さないといけないのがきびしい
定義域に含まれないことにしてなんでも、といっても'()
を返したりする訳にはいかない
ドット対かどうかの情報を残そうとするとリストを最後までたどらなければ
いけないというのが面倒
コードを書くのはすぐだけど、証明がなあ
reverse
との関係で言うと(reverse2 x '())
の'()
は実はx
の最後の要素なんだよな
それを知ってるふりをして計算を進めてるってところがよろしくない
まじめにやるなら、reverse
の中身は(reverse2 x (lastelem x))
みたいな感じになる?
あきらめてreverse/reverse
の条件に入れるくらい?
いやちょっと違うか
証明しようとしてるのはふたつのreverse
が同じっていうことだから
reverse/reverse
ではドット対になるケースは除外します
だからreverse
でもドット対になるケースは除外します、か
どっちみちドット対になるケースの判定が必要になるけど
ゴテっとするのはどこかコレジャナイ感があるんだけどなあ
全域って面倒?
でもそろそろ煮詰まったから手を動かしてみるか
lastelem
でやるほうから
(defun reverse2 (x res)
(if (atom x)
res
(reverse2 (cdr x) (cons (car x) res))))
(defun lastelem (x)
(if (atom x) x (lastelem (cdr x))))
(defun reverseA (x)
(reverse2 x (lastelem x)))
(dethm reverseA/reverseA (x)
(equal (reverseA (reverseA x)) x))
いちおう名前をかぶらせないようにreverse
の名前を変えました
結果は揃ってます
reverseA/reverseA
も成り立ってる模様
・・・
うーコレジャナイ感が
変形して形を合わせる方からてをつけてみる
式の変形だけだからひさしぶりにJ-Bob/step
を使う
(J-Bob/step (defun.reverseA)
'(reverse x)
'((() (reverse x))
; (if (atom x) x (rcons (reverse (cdr x)) (car x)))
((E) (rcons (reverse (cdr x)) (car x)))
; (if (atom x)
; x
; (if (atom (reverse (cdr x)))
; (cons (car x) (reverse (cdr x)))
; (cons (car (reverse (cdr x)))
; (rcons (cdr (reverse (cdr x)))
; (car x)))))
))
(J-Bob/step (defun.reverseA)
'(reversea x)
'((() (reversea x))
; (reverse2 x (lastelem x))
(() (reverse2 x (lastelem x)))
; (if (atom x)
; (lastelem x)
; (reverse2 (cdr x) (cons (car x) (lastelem x))))
))
まったく形が揃う気がしませんね