Reasoned Schemer (71) ==をさらに

すこしだけ複雑なやつ

> (run* q (fresh (x) (== `(((,q)) ,x) `(((,x)) pod))))
'(pod)

とはいっても==を評価したstreamの要素がふたつになったくらい

> ((== `(((,q)) ,x) `(((,x)) pod)) empty-s)
'(((#(x) . pod) (#(q) . #(x))))
> ((reify q) '((#(x) . pod) (#(q) . #(x))))
'pod

同じ変数は同じreified variableになる

> (run* q (fresh (x) (== `(,x ,x) q)))
'((_0 _0))
> ((== `(,x ,x) q) empty-s)
'(((#(q) #(x) #(x))))
> (unify `(,x ,x) q empty-s)
'((#(q) #(x) #(x)))
> ((reify q) '((#(q) #(x) #(x))))
'(_0 _0)

reifyの中を見てみる

> (walk* q '((#(q) #(x) #(x))))
'(#(x) #(x))
> (reify-s '(#(x) #(x)) empty-s)
'((#(x) . _0))
> (walk* '(#(x) #(x)) '((#(x) . _0)))
'(_0 _0)

そりゃ同じreified variableになるよなと
walk*がひとつの関数でふたつの用途に使えてるのがちょっとおもしろいかも

さらに複雑に

> (run* q (fresh (x) (fresh (y) (== `(,q ,y) `((,x ,y) ,x)))))
'((_0 _0))
> ((== `(,q ,y) `((,x ,y) ,x)) empty-s)
'(((#(y) . #(x)) (#(q) #(x) #(y))))
> (unify `(,q ,y) `((,x ,y) ,x) empty-s)
'((#(y) . #(x)) (#(q) #(x) #(y)))
> ((reify q) '((#(y) . #(x)) (#(q) #(x) #(y))))
'(_0 _0)

reifyの中

> (walk* q '((#(y) . #(x)) (#(q) #(x) #(y))))
'(#(x) #(x))
> (reify-s '(#(x) #(x)) empty-s)
'((#(x) . _0))
> (walk* '(#(x) #(x)) '((#(x) . _0)))
'(_0 _0)

大枠はわかってきたかもな
あとはconjとかdisjとかでgoalが組み合わさってきたときかなー