Reasoned Schemer (49) 10章 nevero 続き

次はこれ

> (let ((s-inf ((disj2 (== 'olive x) (nevero)) empty-s))) s-inf)
(((#(x) . olive))
 .
 #<procedure:...r/minikanren.scm:52:29>)

(== 'olive x)の値と(nevero)の値がappendされているようではある
ところでこの式って((disj2 (== 'olive x) (nevero)) empty-s)と何が違うの
letの意味あるの

(== 'olive x)と(nevero)を入れ替えるとちょっと結果が変わる

> (let ((s-inf ((disj2 (nevero) (== 'olive x)) empty-s))) s-inf)
#<procedure:...r/minikanren.scm:50:10>

人力評価してみる
無駄にしか見えないletは手抜きで

  (let ((s-inf ((disj2 (nevero) (== 'olive x)) empty-s))) s-inf)
= ((disj2 (nevero) (== 'olive x)) empty-s)
= ((lambda (s) (append-inf ((nevero) s) ((== 'olive x) s))) empty-s)
= (append-inf ((nevero) empty-s) ((== 'olive x) empty-s))
= (append-inf (lambda () ((nevero) empty-s)) `(((,x . olive))))
= (lambda () (append-inf `(((,x . olive))) ((lambda () ((nevero) empty-s)))))

もう一度評価するとさっきの値と同じになる

> ((let ((s-inf ((disj2 (nevero) (== 'olive x)) empty-s))) s-inf))
(((#(x) . olive))
 .
 #<procedure:...r/minikanren.scm:52:29>)

たしかめ

  ((let ((s-inf ((disj2 (nevero) (== 'olive x)) empty-s))) s-inf))
= ((lambda () (append-inf `(((,x . olive))) ((lambda () ((nevero) empty-s))))))
= (append-inf `(((,x . olive))) ((lambda () ((nevero) empty-s))))
= (cons `((,x . olive)) (append-inf '() ((nevero) empty-s)))
= (cons `((,x . olive)) ((nevero) empty-s))
= (cons `((,x . olive)) (lambda () ((nevero) empty-s)))
= `(((,x . olive)) . ,(lambda () ((nevero) empty-s)))

ちょっとバッククオートの中の書き方が自信ないけど
replに入れてみるとそれっぽくなるからこれでいいんだろう

「もう一度評価する」は本の方だとこういう式
これでも同じ
letを使ってたのはこのため？違うかな

(let ((s-inf ((disj2 (nevero) (== 'olive x)) empty-s))) (s-inf))

ってことを言ってるんだと思うんだけど実は英語がよくわからなかったりした
このへんは(nevero)みたいに一見無限ループしそうな式が
streamによってちょっとずつ評価される様子を見ました、ってことでいいのかな