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
も()
返す