定理証明手習い(99) しゅくだい(7)

わからん

わかるのは、自分の定義したreverseでは常に(reverse (reverse x))がxに
なるとは限らない、ということだけ
あらかじめxを最後まで見て'()で終わっているかを確認して、っていうことは
できるかもしれないけどそこまでするものかよくわからない
それなら証明できるかって言うと大分自信ない

reverseを累積変数を使わない形で実装するという作戦もあるかもしれない

毎回リストの最後までたどってくっつけるとか
でもreverseってこういう形で作るものだと思ってるしこれで証明できないとなあ

そしてさらに困ったことに
帰納法の前提が（たいへん今更ながら）どうもおかしい気がする

         (if (if (equal (cons (car x) res) '())
                 (if (atom (cdr x))
                     't
                     (equal (reverse2 (reverse2 (cdr x) (cons (car x) res)) (cons (car x) res)) (cdr x)))
                 't)

(cons (car x) res)が'())に等しいはずがないのでこの前提は単に'tになってしまって
(equal (reverse2 (reverse2 (cdr x) (cons (car x) res)) (cons (car x) res)) (cdr x)))が
消えてなくなってしまう

reverse2/reverse2から帰納法の前提を作ると確かにこうなってしまいそうなんだけど
(equal res '())っていう条件を入れたのがおかしかった？
そういう気はあんまりしないけど・・・

いちばん最初にもどってみる

(defun reverse2 (x res)
  (if (atom x)
      res
      (reverse2 (cdr x) (cons (car x) res))))

(defun reverse (x)
  (if (atom x)
      x
      (reverse2 x '())))

(dethm reverse/reverse (x)
  (equal (reverse (reverse x)) x))

(dethm reverse2/reverse2 (x res)
  (if (equal res '())
      (if (atom x)
          't
          (equal (reverse2 (reverse2 x res) res) x))
      't))

うむ
アイデアなし

これは・・・

いったんあきらめるかな
何か思いついたら戻ってこよう

ところでちょっと話は変わりますが
reverseが正しいかどうか証明してください、って言われたら何をするんでしょうね？
reverse/reverseがreverseの性質をよく表しているとはいえないし
(identityでも成り立つ)
xのn番目の要素が((len x) - n)番目の要素と等しい、って言うんですかね
(car (cons a b))はaに等しい、みたいな形にくらべるとごちゃっとした感じですが
xのn番目の要素が((len x) - n)番目の要素と等しい、っていうのが
reverseが正しい、ってことと同じだっていうのはどうやって確かめるのかな
いや、それは始めからそういう仕様が定められているってだけなのかな
仕様に「ドット対でなければ」とか「ドット対の場合は」とか書いてあるのかな

どうなんですかFriedman先生Eastlund先生