Reasoned Schemer (64) 読み返し10章(続き2)

次からappend-infが登場
うまく追っかけられるだろうか

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

ここで

  ((== 'olive x) empty-s)
= ((lambda (s) (let ((s (unify 'olive x s))) (if s `(,s) '()))) empty-s)
= `(((,x . olive)))

だから

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

This stream, s-inf, is a pair whose car is the substitution ``((,x .olive)) and whose cdr is a stream.

あってる
これは１個だけ値がとれて2個めを取ろうとするとno valueになる形かな

  (run-goal 1 (disj2 (== 'olive x) (nevero)))
= (take-inf 1 ((disj2 (== 'olive x) (nevero)) empty-s))
= (take-inf 1 `(((,x . olive)) . (lambda () ((nevero) empty-s))))
= (cons `((,x . olive)) (take-inf 0 (lambda () ((nevero) empty-s))))
= (cons `((,x . olive)) '())
= `(((,x . olive)))

は値が取れるけど

  (run-goal 2 (disj2 (== 'olive x) (nevero)))
= (take-inf 2 ((disj2 (== 'olive x) (nevero)) empty-s))
= (take-inf 2 `(((,x . olive)) . (lambda () ((nevero) empty-s))))
= (cons `((,x . olive)) (take-inf 1 (lambda () ((nevero) empty-s))))
= (cons `((,x . olive)) (take-inf 1 ((lambda () ((nevero) empty-s)))))
= (cons `((,x . olive)) (take-inf 1 ((nevero) empty-s)))
= (cons `((,x . olive)) (take-inf 1 (lambda () ((nevero) empty-s))))
= ...

は返ってこないってわけだな
うんちょっと見えてきた気がする