定理証明手習い (63) j-bob-lang

SchemeでJ-Bobを使うには

(define s.car car)
(define (car x) (if (pair? x) (s.car x) '()))

こうやって関数を上書きして全域にしていくのね

(define (if/nil Q A E)
  (if (equal? Q 'nil) (E) (A)))

あれ
これってifは関数では書けませんよ、っていうパターンにハマってないんだっけ？

(define-syntax if
  (syntax-rules ()
    ((_ Q A E)
     (if/nil Q (lambda () A) (lambda () E)))))

ほう
Aをlambdaで囲んでるのか
これで式が評価されちゃうのを防ごうってことだな
言われてみれば上のifの定義、単にA、Eじゃなくて
(A)、(E)ってなってるな
これだと

  (if (atom 'a) (+ 1 1) (+ 1 2))
= (if/nil (atom 'a) (lambda () (+ 1 1)) (lambda () (+ 1 2)))
= (if 't (+ 1 1) (+ 1 2))
= (+ 1 1)

となって(+ 1 2)の方は評価されない、ってわけか

マクロとか関数とかで組み込みを上書きしすぎてて何がどうなっているかわからないけど

(define (natp x)
  (if (integer? x) (if (< x 0) 'nil 't) 'nil))

は

(define (natp x)
  (if (integer? x) (if (s.< x 0) 'nil 't) 'nil))

が正しい模様
ダウンロードしてきた方ではそうなってる

でもなんでだっけ？
えーと

  (natp 0)
= (if (integer? 0) (if (< 0 0) 'nil 't) 'nil))

だけどこのifや<はnatpが定義された時のifや<だよな
いやでもそれだとうまくいくはずか

s.<にして正しく動くようになるところからすると
ifは上書き前、<は上書き後の意味になってるということだろうな
でもnatpが定義されたときの<は上書き前の<のはずだけど
うーん
わからん
どうやったら調べられるかな

(define-syntax dethm
  (syntax-rules ()
    ((_ name (arg ...) body)
     (define (name arg ...) body))))

へー定理も関数と同じでいいんだ

ってこれ、使いみちある？
defunは使うとしてもdethmってJ-Bob/proveのクォートの中にしか
出てこないと思ってたけど

(defun size (x)
  (if (atom x)
      '0
      (+ '1 (size (car x)) (size (cdr x)))))

これもだ
このままじゃエラー
ダウンロードしたj-bob-langではこうなってる

(defun size (x)
  (if (atom x)
      '0
      (+ '1 (+ (size (car x)) (size (cdr x))))))

あるいは+のかわりにs.+でも大丈夫
これは何か単なる誤植じゃない何かがあるのかも？

kb84tkhrのブログ