J-Bobを作ってみよう(6) バグ発見

テストが書けるようになりましたのでj-bob.jbbにテストを移植しつつ調査していきました
へんな値が返されるのを発見

implication/1exp
actual  :(if (equal x 'a) (equal (quote-c 't) 'b) 't)
expected:(if (equal x 'a) (equal y 'b) 't)

このテストで発生

(my/test "implication/1exp"
         (implication '((equal x 'a)) '(equal y 'b))
         '(if (equal x 'a) (equal y 'b) 't))

REPLでも発生

> (repl)
>> (implication '((equal x 'a)) '(equal y 'b))
(if (equal x 'a) (equal (quote-c 't) 'b) 't)

yが(quote-c 't)になってしまってるな

関連ソース

(defun list0 () '())
(defun list1 (x) (cons x (list0)))
(defun list2 (x y) (cons x (list1 y)))
(defun list3 (x y z) (cons x (list2 y z)))
(defun tag (sym x) (cons sym x))
(defun if-c (Q A E) (tag 'if (list3 Q A E)))
(defun implication (es e)
  (if (atom es)
    e
    (if-c (car es)
      (implication (cdr es) e)
      (quote-c 't))))

ソースは合ってるように思われるので（当然）処理系の問題なんだろうなあ
やっぱり何か足りてないか？
さてどうやって調べたものやら

こうなるはずなんだよな

  (implication '((equal x 'a)) '(equal y 'b))
= (if-c '(equal x 'a) (implication '() '(equal y 'b)) ''t)
= (if-c '(equal x 'a) '(equal y 'b) ''t)
= (tag 'if (list3 '(equal x 'a) '(equal y 'b) ''t))
= (cons 'if (list3 '(equal x 'a) '(equal y 'b) ''t))
= (cons 'if (cons '(equal x 'a) (list2 '(equal y 'b) ''t)))
= (cons 'if (cons '(equal x 'a) (cons '(equal y 'b) (list1 ''t))))
= (cons 'if (cons '(equal x 'a) (cons '(equal y 'b) (cons ''t list0))))
= (cons 'if (cons '(equal x 'a) (cons '(equal y 'b) (cons ''t '()))))
= '(if (equal x 'a) (equal y 'b) 't)

範囲を狭めていこう

>> (if-c '(equal x 'a) '(equal y 'b) ''t)
(if (equal x 'a) (equal ''t 'b) 't)

これはまだおかしい
継続

>> (tag 'if (list3 '(equal x 'a) '(equal y 'b) ''t))
(if (equal x 'a) (equal ''t 'b) 't)
>> (cons 'if (list3 '(equal x 'a) '(equal y 'b) ''t))
(if (equal x 'a) (equal ''t 'b) 't)
>> (list3 '(equal x 'a) '(equal y 'b) ''t)
((equal x 'a) (equal ''t 'b) 't)
>> (list2 '(equal y 'b) ''t)
((equal ''t 'b) 't)
>> (list1 ''t)
('t)

(list2 '(equal y 'b) ''t)がマズいという結果

どうもyという名前がまずいっぽい気がする
ゲーデルの証明でも、名前がスコープ内に現れない、とかやってたもんな
きっとあれだ

>> (list2 '(equal z 'b) ''t)
((equal z 'b) 't)

zなら大丈夫

(japply 'list2 '((equal y 'b) ''t)))を追いかけてみます
(defun list2 (x y) (cons x (list1 y)))だから最初はこんな状態

f = '(list2 (x y) (cons x (list1 y)))
vars = '(x y)
args = '((equal y 'b) ''t))
res = '(cons x (list1 y))

あ、もうわかっちゃったかも
ここから2段階で置き換え

  (subst '(cons x (list1 y)) (car '(x y)) (car '((equal y 'b) ''t)))
= (subst '(cons x (list1 y)) 'x '(equal y 'b))
= '(cons (equal y 'b) (list1 y))

  (subst '(cons (equal y 'b) (list1 y)) (car '(y)) (car '('t)))
= (subst '(cons (equal y 'b) (list1 y)) 'y ''t)))
= '(cons (equal 't 'b) (list1 't))

結論：
xを置き換えた式の中にyが含まれていると、yの置き換えでそこもいっしょに置き換えられてしまう
対策：
引数の置き換えは全引数同時に行う

(define (subst e vars args)
  (cond ((null? e) '())
        ((atom? e)
         (let loop ((vars vars)
                    (args args))
           (cond ((null? vars) e)
                 ((eq? e (car vars)) (car args))
                 (else (loop (cdr vars) (cdr args))))))
        (else (cons (subst (car e) vars args)
                    (subst (cdr e) vars args)))))

(define (japply name args)
  (jeval
   (let* ((f (findfunc name))
          (vars (cadr f)))
     (subst (caddr f) vars args))))

それいけ

>> (implication '((equal x 'a)) '(equal y 'b))
(if (equal x 'a) (equal y 'b) 't)

直りました

もしかしてこれでJ-Bob/stepから処理が帰ってこないのも
直ったりしないかなーと思いましたが変わらず
道は険しい