定理証明手習い(a3) しゅくだい(11)

またもアドバイスいただきました

(rev2 (rev2 l nil) nil) = l なら (rev2 (rev2 l (cons a nil)) nil) = (cons a l)
ですね。この証明にも、rev2の引数がrcons（またはappend）である場合の補題が必要になるとおもいます。

— SUHARA Hiromichi (@suharahiromichi) 2018年5月13日

意味はわかるような気がする
J-Bobが出してくれた主張の方も見直してみよう

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

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

再掲

reverse2/reverse2 の証明は、私も考えてみましたが、累積変数を使った定義と逆consを使った定義とが同じである、ということを証明してしまうのが一番易しいようです。でも、末尾再帰になっている関数を証明する技法を考えてみるのも面白そうですね。

— SUHARA Hiromichi (@suharahiromichi) 2018年4月28日

同じである、というのはふたつのバージョンのreverseが同じ、ということでしょう
(reverse/reverseとreverse2/reverse2が同じということではなくて)
「同じ」というのは一方を変換して他方と同じ形にできる、ってことかな
それとも(equal (reverse x) (reverse' x))を証明するのかな
似てるようだけど違う

定理証明手習い(a1) しゅくだい(9)

rcons版のreverse/reverseを証明します
reverse2/reverse2はどうしようかな

rconsとreverseの定義・証明

(defun defun.rcons ()
  (J-Bob/define (prelude)
    '(((defun rcons (x y)
         (if (atom x)
             (cons y x)
             (cons (car x) (rcons (cdr x) y))))
       (size x)
       ((Q) (natp/size x))
       (() (if-true (if (atom x) 't (< (size (cdr x)) (size x))) 'nil))
       ((E) (size/cdr x))
       (() (if-same (atom x) 't))))))

(defun defun.reverse ()
  (J-Bob/define (defun.rcons)
    '(((defun reverse (x)
         (if (atom x)
             x
             (rcons (reverse (cdr x)) (car x))))
       (size x)
       ((Q) (natp/size x))
       (() (if-true (if (atom x) 't (< (size (cdr x)) (size x))) 'nil))
       ((E) (size/cdr x))
       (() (if-same (atom x) 't))))))

ここまでは簡単
reverse/reverseもこの調子で証明できるかな

定理証明手習い(a0) しゅくだい(8)

想定以上に寝かせることになってしまいましたがアドバイスいただきましたので考えてみます
寝かせたわりには特にアイデアは思いついていません

reverse2/reverse2 の証明は、私も考えてみましたが、累積変数を使った定義と逆consを使った定義とが同じである、ということを証明してしまうのが一番易しいようです。でも、末尾再帰になっている関数を証明する技法を考えてみるのも面白そうですね。

— SUHARA Hiromichi (@suharahiromichi) 2018年4月28日

reverse2/reverse2　を直接証明しようとすると、おそらく、
(rcons (rev2 x nil) a) = (rev2 x '(a)) と (cons a (rev2 x nil)) = (rev2 (rcons x a) nil) のふたつの補題を証明する必要があり、どちらも帰納法が必要で、ちょっと大変な気がします。rcons はリストの後ろにconsする関数です。

— SUHARA Hiromichi (@suharahiromichi) 2018年4月29日

さてアドバイスが雰囲気でしかわかってないので最初から考えていきます

J-Bobを作ってみよう(11) おしまい

まあ一度真正面からどう動いているのか見てやろうかと
ソースは組み込み関数を増やす前のものに戻しました

とりあえずこんな感じのベタなことをしてみました
これでも意外とつかめるかもしれないし

J-Bobを作ってみよう(10) 組み込み関数を追加する

たかだか証明を数ステップ進めるだけで関数を何百万会も呼ばなきゃいけないのかという
疑問を脇に押しのけてたくさん呼ばれてる関数を組み込み関数にしてみます
なんにも頭を使わない力技

J-Bobを作ってみよう(9) J-Bobをプロファイリング

J-Bobを動かしてみます

>> (load "j-bob.jbb")
Welcome to J-Bob
#<void>
>> (J-Bob/step
     '((dethm car/cons (x y) (equal (car (cons x y)) x)))
     '(car (cons 'ham '(eggs)))
     '((() (car/cons 'ham '(eggs)))))
'ham
>> (show-profile)
     '((untag 18159)
       (elem1 9304)
       (tag? 6366)
       :

意外とたくさん動いてる感じ