kb84tkhrのブログ

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

定理証明手習い (11) J-Bob/define

正誤表ができてますね

github.com

どっちかというとScheme手習いやScheme修行の方が正誤表ほしかったかなあ
この本はだいたい安心して読めてる感じ
訳も自然な気がする

さて本題
証明できた関数や定理はJ-Bob/defineを使って他の証明で使いまわせるようにできます

J-Bob/defineの書き方はJ-Bob/proveとほとんど同じ感じ

(J-Bob/define (<公理・定義済みの関数/定理>)
  '((<関数・定理の定義>
     <種>
     <証明>)
     ...))

実例

> (J-Bob/define (my/prelude)
    '(((defun pair (x y)
         (cons x (cons y '())))
       nil)))
((dethm atom/cons (x y) (equal (atom (cons x y)) 'nil))
  :
 (dethm if-nest-e (x y z) (if x 't (equal (if x y z) z)))
 (defun pair (x y) (cons x (cons y '()))))

値は公理や関数・定理のリストになってます
証明済みかどうかのチェックして、リストの末尾に定義をくっつける、ということを
やってるようですね

で、J-Bob/defineが返してきたリストに名前をつけてやることにより使いまわします

(defun defun.pair () ; 名前をつける
  (J-Bob/define (my/prelude)
    '(((defun pair (x y)
         (cons x (cons y '())))
       nil))))

(defun defun.first-of ()
  (J-Bob/define (defun.pair) ; ここで使いまわしてる
    '(((defun first-of (x)
         (car x))
       nil))))

付録Bで1章2章の例をわざわざ関数の形で書いてたのは
こういう書き方にあわせたのかも?

付録Aではいくつかの関数や定理をまとめて定義してますが
付録Bでは関数や定理をひとつずつ定義していきます
この違いはなんなんでしょうか
分けておけば必要な部分だけ使える、ていっても分けて使う場面は出てくるんでしょうか