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
から処理が帰ってこないのも
直ったりしないかなーと思いましたが変わらず
道は険しい