Reasoned Schemer (80) delrel再考

ところで(run 1 x (listo ``(a b c . ,x)))はdefrelにlambda ()がないと帰ってこない
やっとlambda ()の存在意義を確認

lambda ()なしのdefrelでやると

  ((listo x) empty-s)
= ((lambda (s) ((conde ((nullo x)) ((fresh (d) (cdro x d) (listo d)))) s)) empty-s)
= ((conde ((nullo x)) ((fresh (d) (cdro x d) (listo d)))) empty-s)
= ((disj2 (nullo x) (fresh (d) (cdro x d) (listo d))) empty-s)
= ((lambda (s) (append-inf (nullo s) ((fresh (d) (cdro x d) (listo d)) s))) empty-s)
= (append-inf ((nullo x) empty-s) ((fresh (d) (cdro x d) (listo d)) empty-s))
= (append-inf `(((,x . ()))) ((fresh (d) (cdro x d) (listo d)) empty-s))

ちょっと手でやるのはつらくなってきた
((nullo x) empty-s)は``(((,x . ())))だけど
REPLで((fresh (d) (cdro x d) (listo d)) empty-s)を評価すると帰ってこない
lambda ()がないとcdroやlistoの計算がずっと続きそうではある

lambda ()があると・・・どうなるの

  ((listo x) empty-s)
= ((lambda (s) (lambda () ((conde ((nullo x)) ((fresh (d) (cdro x d) (listo d)))) s))) empty-s)
= (lambda () ((conde ((nullo x)) ((fresh (d) (cdro x d) (listo d)))) empty-s))

ここでいったんtake-infに戻ってくるってことかな
たぶんそうだと思うけど
そうするとどうなるの

  (take-inf 1 ((listo x) empty-s))
= (take-inf 1 (lambda () ((conde ((nullo x)) ((fresh (d) (cdro x d) (listo d)))) empty-s)))
= (take-inf 1 ((lambda () ((conde ((nullo x)) ((fresh (d) (cdro x d) (listo d)))) empty-s))))
= (take-inf 1 ((conde ((nullo x)) ((fresh (d) (cdro x d) (listo d)))) empty-s))
= (take-inf 1 (append-inf ((nullo x) empty-s) ((fresh (d) (cdro x d) (listo d)) empty-s)))

ここでREPLの力を借りることに
lambda ()があるので

> ((nullo x) empty-s)
#<procedure:...r/minikanren.rkt:147:9>
> (((nullo x) empty-s))
'(((#(x))))
> ((fresh (d) (cdro x d) (listo d)) empty-s)
#<procedure:...r/minikanren.rkt:76:10>

とstreamが返ってくる

  (take-inf 1 (append-inf ((nullo x) empty-s) ((fresh (d) (cdro x d) (listo d)) empty-s)))
= (take-inf 1 (append-inf ((fresh (d) (cdro x d) (listo d)) empty-s) (((nullo x) empty-s)))
= (take-inf 1 (append-inf ((fresh (d) (cdro x d) (listo d)) empty-s) `(((,x . ())))))
= (take-inf 1 (append-inf  `(((,x . ()))) (((fresh (d) (cdro x d) (listo d)) empty-s))))
= (take-inf 1 `(((,x . ())) . (((fresh (d) (cdro x d) (listo d)) empty-s))))
= `(((,x . ()))

うーん
まだ核心部分が腹に落ちるところまではいってないけど
cdroやlistoのようにdefrelで定義されたものは
substitutionを与えられるといったんsuspensionを返してくるわけだから
((fresh (d) (cdro x d) (listo d)) empty-s)みたいなのもいったんsuspensionを返す、でいいかなあ
nulloもそうだし
suspensionを返さない版のdefrelだとここで止まってしまうと