kb84tkhrのブログ

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

定理証明手習い (88) J-Bob/step

(rewrite/step defs claim step) claimstepで書き換える

equality/defで組み込み関数を置き換えるとき、defには組み込み関数の
「定義」では(当然ながら)なく、関数名が単に入っていました
どっかでわざわざ組み込み関数かどうかを判断して渡してるのかな、と思ってましたが
lookupで名前を探して見つからなかったときは名前を返すという、
以前ちょっと不思議に感じていた仕様はこのためだったんですね
ちょっとわかりづらいぞ

(rewrite/continue defs steps old new) newstepsで(いけるところまで)書き換える

oldは、直前の書き換えが成功したかどうかを判定するためにだけ使われます
ほかに失敗を伝える手段があればoldは不要そう

直前の書き換えが失敗したか、stepsの最後に到達するまで続けます

(rewrite/steps defs claim steps) claimstepsで書き換える

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章まで動きました