定理証明手習い (88) J-Bob/step
(rewrite/step defs claim step)
claim
をstep
で書き換える
equality/def
で組み込み関数を置き換えるとき、def
には組み込み関数の
「定義」では(当然ながら)なく、関数名が単に入っていました
どっかでわざわざ組み込み関数かどうかを判断して渡してるのかな、と思ってましたが
lookup
で名前を探して見つからなかったときは名前を返すという、
以前ちょっと不思議に感じていた仕様はこのためだったんですね
ちょっとわかりづらいぞ
(rewrite/continue defs steps old new)
new
をsteps
で(いけるところまで)書き換える
old
は、直前の書き換えが成功したかどうかを判定するためにだけ使われます
ほかに失敗を伝える手段があればold
は不要そう
直前の書き換えが失敗したか、steps
の最後に到達するまで続けます
(rewrite/steps defs claim steps)
claim
をsteps
で書き換える
rewrite/continue
をキックするだけですがほぼJ-Bob/step
になってそうです
すこし先回りしてJ-Bob/step
まで定義してみましょうか
(defun J-Bob/step (defs e steps)
(if (defs? '() defs)
(if (expr? defs 'any e)
(if (steps? defs steps)
(rewrite/steps defs e steps)
e)
e)
e))
引数を確認してrewrite/steps
を呼んでるだけですね
公理はまだありませんが動くんじゃないかな
> (J-Bob/step '()
'(car (cons 'ham '(eggs)))
'(((1) (cons 'ham '(eggs)))
(() (car '(ham eggs)))))
'ham
動きました
axiomsも入れちゃうか
このへんは見ながらやってきたし
preludeはまだフルには実装できないのでちょっとごまかして
(defun prelude () (axioms))
これで2章まで動きました