Reasoned Schemer (53) 10章 substitusionのstreamとは

何か見えた気もするんだよな

substitusionのstreamってなんなのかってのがイメージできてない
(unify u v s)はuとvは同じですっていうことにしたsを返すこと、
っていうあたりまではわかった気になっている

この間のギャップが埋められるだろうか

(define (== u v)
  (lambda (s)
    (let ((s (unify u v s)))
      (if s `(,s) '()))))

uとvが同じですってことにできると、sだけを要素に持つstreamを返す関数を返す
substitutionを渡すとuとvが同じですってことにしたsubstitutionだけを要素に持つstreamを返す
言葉にするとややこしい

> ((== 'olive x) empty-s)
(((#(x) . olive)))

これだけ見ても意味がわからなかったんだよな
説明がないところに実例も少なすぎた

今はもうちょっと知ってる
disj2の結果はこうなる

> ((disj2 (== 'olive x) (== 'oil x)) empty-s)
(((#(x) . olive)) ((#(x) . oil)))

xはoliveであるというsubstitutionと
xはoilであるというsubstitutionを要素に持つstreamになった

さらにconj2

> ((disj2 (conj2 (== 'olive x) (== 'oil y))
          (conj2 (== 'cream x) (== 'cheese y))) empty-s)
(((#(y) . oil) (#(x) . olive))
 ((#(y) . cheese) (#(x) . cream)))

ふたつのassociationをもつsubstitutionがふたつできた

streamのなかのひとつのsubstitutionがえーとなんて言えばいいのかなあ
andでつながってて、っていうかconj2でつながってるんだけど
同時に満たすっていうか全部は満たさないこともありそうなきがするけど
なんかそんなもので

でstreamのなかのsubstitutionのうちどれかを満たせればいい
orみたいなもの
って感じっぽいね

> ((conj2 (disj2 (== 'olive x) (== 'cream x))
          (disj2 (== 'oil y) (== 'cheese y))) empty-s)
(((#(y) . oil) (#(x) . olive))
 ((#(y) . cheese) (#(x) . olive))
 ((#(y) . oil) (#(x) . cream))
 ((#(y) . cheese) (#(x) . cream)))

xがoliveかcreamのどちらかで、かつyがoilかcheeseのどちらかという
組み合わせをすべてあげて4通り

> ((disj2 (disj2 (== 'olive x) (== 'cream x))
          (disj2 (== 'oil x) (== 'cheese x))) empty-s)
(((#(x) . olive))
 ((#(x) . cream))
 ((#(x) . oil))
 ((#(x) . cheese)))

これも4とおり

> ((conj2 (conj2 (== 'olive x) (== 'cream y))
          (conj2 (== 'oil u) (== 'cheese v))) empty-s)
(((#(v) . cheese)
  (#(u) . oil)
  (#(y) . cream)
  (#(x) . olive)))

全部conj2でつなぐとひとつのsubstitutionに
この組み合わせしかない

> ((conj2 (conj2 (== 'olive x) (== 'cream y))
          (conj2 (== 'oil u) (== 'cheese x))) empty-s)
()

無理な時は無理

イメージができた気がする