Reasoned Schemer (72) conj2

fuseされていなければ変数がdifferent
変数の名前が違うだけなら式の値は変わらない
xがyの中に現れることをoccurという

このあたりはOK

conj2登場

> (run* q (conj2 succeed succeed))
'(_0)

これはどうなっているか

  ((conj2 succeed succeed) empty-s)
= (append-map-inf succeed (succeed empty-s))
= (append-map-inf succeed '(()))
= (append-inf (succeed '()) '())
= '(())

ほかの例も見てみないとピンとこないな

> (run* q (conj2 succeed (== 'corn q)))
'(corn)

多少は動きが見えるだろう

  ((conj2 succeed (== 'corn q)) empty-s)
= (append-map-inf (== 'corn q) (succeed empty-s))
= (append-map-inf (== 'corn q) '(()))
= (append-inf ((== 'corn q) '()) '())
= (append-inf '(((#(q) . corn))) '())
= '(((#(q) . corn)))

いつも成功する(='())という条件に重ねて
qと``cornが同じなら成功する(=``((#(q) . corn)))という条件を重ねると
``(((#(q) . corn)) append ()) = ``(((#(q) . corn))) となる、ってわけか

最初にgoalに与えるsubstitutionは常にempty-sだけれども
(conj2 g1 g2)からのappend-map-infが(g2 s)のstreamからひとつずつ
substitutionを取り出してg1に食わせているんだな

goalがsubstitutionを引数に取るというのもなんとなく雰囲気でわかってきた

> (run* q (conj2 fail (== 'corn q)))
'()

こっちも同様に見ていくと

  ((conj2 fail (== 'corn q)) empty-s)
= (append-map-inf (== 'corn q) (fail empty-s))
= (append-map-inf (== 'corn q) '())
= '()

failは常に空のstreamを返すのでappend-map-infも()返す