Reasoned Schemer (74) disj2

disj2のほうがconj2よりもイメージしやすい気がする
ちょっと加速しよう
((disj2 fail fail) empty-s)は追ってもあっさりしすぎててわからなさそうだから
このへんで

> (run* q (disj2 (== 'olive q) (== 'oil q)))
'(olive oil)

こうね

  ((disj2 (== 'olive q) (== 'oil q)) empty-s)
= (append-inf ((== 'olive q) empty-s) ((== 'oil q) empty-s))
= (append-inf `(((,q . olive))) `(((,q . oil))))http://blog.hatena.ne.jp/kb84tkhr/kb84tkhr.hatenablog.com/edit?editinplace=1#wysiwyg
= `(((,q . olive)) ((,q . oil)))

  (map (reify `,q) `(((,q . olive)) ((,q . oil))))
= '(olive oil)

これも一見ややこしくなったように見えてそんなに変わらない

> (run* q (fresh (x) (fresh (y) (disj2 (== `(,x ,y) q) (== `(,y ,x) q)))))
'((_0 _1) (_0 _1))

(_0 _1)がふたつでいっしょじゃん、って見えるけれども
最初の(_0 _1)は(,x ,y)でふたつめの(_0 _1)は(,y ,x)
こうだから

> ((disj2 (== `(,x ,y) q) (== `(,y ,x) q)) empty-s)
'(((#(q) #(x) #(y))) ((#(q) #(y) #(x))))

といっても実際のところ同じっちゃあ同じ

ところでこのdisj2をconj2にしたらどうなるだろう

> (run* q (fresh (x) (fresh (y) (conj2 (== `(,x ,y) q) (== `(,y ,x) q)))))
'((_0 _0))

おおかしこいな
ちゃんとわかってる

> ((conj2 (== `(,x ,y) q) (== `(,y ,x) q)) empty-s)
'(((#(y) . #(x)) (#(q) #(x) #(y))))

xとyがおなじっていうのはどうやって導き出されてるんだっけ

  ((conj2 (== `(,x ,y) q) (== `(,y ,x) q)) empty-s)
= (append-map-inf (== `(,y ,x) q) ((== `(,x ,y) q) empty-s))
= (append-map-inf (== `(,y ,x) q) `(((,q . (,x ,y)))))
= ((== `(,y ,x) q) `((,q . (,x ,y))))
= (unify `(,y ,x) q `(((,q . (,x ,y)))))

ときて(walk q ``((,q . (,x ,y))))は``(,x ,y)だから
``(,y ,x)と見比べてxとyが同じと気づくってわけか

なるほどわかってきた

いくつかconj2とdisj2をもうすこし複雑に組み合わせた式がでてくるけど
イメージはできる

substitutionっていうのは結局、この変数は何ですよ、っていうのを並べただけのものなんだよな
schemeの言葉で言えば？束縛のリストというか
この変数とこの変数は同じ(=fuseされてる)、っていう表現はこっち独特かな？どうだっけ？
でも循環しないようになってるから木になっててたどっていく(=walkする)と
同じものは同じところにたどり着くという
unifyすると束縛ができてconj2するとsubstitutionに束縛が追加されて
disj2するとsubstitutionが追加される
大枠はそれくらいっぽいでいいんじゃないか