kb84tkhrのブログ

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

定理証明手習い(a2) しゅくだい(10)

littleprover

再考します、と言ってはみたもののイメージはつかめてなかったり
(reverse/reverseだって証明はもっと簡単にできるイメージだった・・・)

再掲

同じである、というのはふたつのバージョンの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))))
    
    ))

まったく形が揃う気がしませんね