Reasoned Schemer (88) nevero 続き2

> (run 1 q (conde (succeed) ((nevero))) fail)

これが止まるのはだいたいイメージできるけど練習でやってみよう

  ((conj2 (conde (succeed) ((nevero))) fail) [])
= (append-map-inf fail ((conde (succeed) ((nevero))) []))
= (append-map-inf fail [[] {{{...}}}])
= (append-inf (fail []) (append-map-inf fail {{{...}}}))
= (append-inf [] {(append-map-inf fail {{{...}}})}) ; append-map-infはsuspensionを返す
= {(append-map-inf fail {{{...}}})}
= {{(append-map-inf fail {{{...}}})}}
= {{{(append-map-inf fail {{{...}}})}}}

いくらforceしてもappend-map-infのsuspensionしか返ってこない
次行こう

> (run 5 q (conde ((nevero)) ((alwayso)) ((nevero))))
'(_0 _0 _0 _0 _0)

短く書けるようにすこし工夫したけどもう無理かな
先に答え合わせをしておくと

> ((conde ((nevero)) ((alwayso)) ((nevero))) '())
#<procedure:...r/minikanren.rkt:56:10>
> (((conde ((nevero)) ((alwayso)) ((nevero))) '()))
#<procedure:...r/minikanren.rkt:56:10>
> ((((conde ((nevero)) ((alwayso)) ((nevero))) '())))
#<procedure:...r/minikanren.rkt:56:10>
> (((((conde ((nevero)) ((alwayso)) ((nevero))) '()))))
#<procedure:...r/minikanren.rkt:56:10>
> ((((((conde ((nevero)) ((alwayso)) ((nevero))) '())))))
#<procedure:...r/minikanren.rkt:56:10>
> (((((((conde ((nevero)) ((alwayso)) ((nevero))) '()))))))
'(() . #<procedure:...r/minikanren.rkt:56:10>)

5回forceしてやっとsubstitutionが出てくる

いきなり三段重ねもアレなのでまず2段から練習

  ((conde ((alwayso)) ((nevero))) [])
= ((disj2 (alwayso) (nevero)) [])
= (append-inf ((alwayso) []) ((nevero) []))
= (append-inf {[[] {[[] {[[] ... ]}]}]} {{{{...}}}})
= {(append-inf {{{{...}}}} [[] {[[] {[[] ... ]}]}])}
= {{(append-inf [[] {[[] {[[] ... ]}]}] {{{{...}}}})}}
= {{[[] (append-inf {[[] {[[] ... ]}]} {{{{...}}}})]}}
= {{[[] {(append-inf {{{{...}}}} [[] {[[] ... ]}])}]}}
= {{[[] {{(append-inf [[] {[[] ... ]}] {{{{...}}}})}}]}}
= {{[[] {{[[] (append-inf {[[] ... ]} {{{{...}}}})]}}]}}
= {{[[] {{[[] {(append-inf {{{{...}}}} [[] ... ])}]}}]}}
= {{[[] {{[[] {{[[] ... ]}}]}}]}}

なんとかなった・・・かな？
目がちかちかする
2回forceすればsubstitutionが現れるはず
cdrを取ったらまた2回

> ((((conde ((alwayso)) ((nevero))) '())))
'(() . #<procedure:...r/minikanren.rkt:56:10>)
> (((cdr ((((conde ((alwayso)) ((nevero))) '()))))))
'(() . #<procedure:...r/minikanren.rkt:56:10>)
> (((cdr (((cdr ((((conde ((alwayso)) ((nevero))) '())))))))))
'(() . #<procedure:...r/minikanren.rkt:56:10>)

予言的中
では本番

  ((conde ((nevero)) ((alwayso)) ((nevero))) [])
= ((disj2 (nevero) (disj2 (alwayso) (nevero))) [])
= (append-inf ((nevero) []) ((disj2 (alwayso) (nevero)) []))

ここでさっきの結果を利用

= (append-inf {{{{...}}}} {{[[] {{[[] {{[[] ... ]}}]}}]}})
= {(append-inf {{[[] {{[[] {{[[] ... ]}}]}}]}} {{{{...}}}})}
= {{(append-inf {{{{...}}}} {[[] {{[[] {{[[] ... ]}}]}}]})}}
= {{{(append-inf {[[] {{[[] {{[[] ... ]}}]}}]} {{{{...}}}})}}}
= {{{{(append-inf {{{{...}}}} [[] {{[[] {{[[] ... ]}}]}}])}}}}
= {{{{{(append-inf [[] {{[[] {{[[] ... ]}}]}}] {{{{...}}}})}}}}}
= {{{{{[[] (append-inf {{[[] {{[[] ... ]}}]}} {{{{...}}}})]}}}}}
= {{{{{[[] {(append-inf {{{{...}}}} {[[] {{[[] ... ]}}]})}]}}}}}

5回だ

very-recursiveoは追っかけないよ！

(defrel (very-recursiveo)
  (conde
    ((nevero))
    ((very-recursiveo))
    ((alwayso))
    ((very-recursiveo))
    ((nevero))))

止まらないことはわかる