Reasoned Schemer (68) 勘違い

まだ理解したっていう手ごたえを感じてないんだけどどうするっていうアイデアもないので進める

> (run* q succeed)
'(_0)

qはfresh

10章までsucceedって何かあんまり意識してなかったりもした

> (fail empty-s)
'()
> (succeed empty-s)
'(())

要するに()以外は全部成功でsucceedはその中の一番単純な形
CでTRUEを1と定義してるようなもんだな
(succeed empty-s)が(())でqをreifyすると(_0)になる

> (run* q (== 'pea 'pea))
'(_0)
> (run* q (== q q))
'(_0)

qはfreshなまま

freshの導入

> (run* q (fresh (x) (== 'pea q)))
'(pea)
> (run* q (fresh (x) (== 'pea x)))
'(_0)
> (run* q (fresh (x) (== (cons x '()) q)))
'((_0))

この最後の式、なんでうまくいくんだろう
処理系は特にconsに関する知識は持ってないはずだけど

どこがうまいことやってんのかなあ

> (run-goal #f (fresh (x) (== (cons x '()) q)))
'(((#(q) #(x))))
> ((fresh (x) (== (cons x '()) q)) empty-s)
'(((#(q) #(x))))
> ((== (cons x '()) q) empty-s)
'(((#(q) #(x))))
> (unify (cons x '()) q empty-s)
'((#(q) #(x)))

あっ
(cons x '())ってただの(#(x) . '())じゃないか
あー
(lambda (x) (cons x '()))みたいなものと思い込んじゃってたよ
schemeの変数とminikanrenの変数がごっちゃになっている
変数じゃなくてただの値ですよ
(#(x))にconsの知識も何もないよ、っていうと変か
unifyがconsセルの知識を持ってるからこそunifyできるわけだな

うーん
いろいろ考え直さないとか？
特にcall/freshがなんかピンときてなかったのはそのせいだきっと