Reasoned Schemer (014) nevero
こんどはいっそうシンプルに
(defrel (nevero)
(nevero))
-
#u
は失敗するが、(nevero)
は成功も失敗もしない -
(run 1 q (nevero))
→ 値なし -
(run 1 q #u (nevero))
→()
1回目に#u
で失敗するから
(run 1 q (conde (#s) ((nevero))))
→(_0)
1回目に#s
で成功するから
(run 1 q (conde ((nevero)) (#s)))
→(_0)
1回目に#s
で成功するから、らしいですよ
The Law of Swapping conde Linesによりひとつ前の式と同じ値を
持つはずだから、とのこと
でも素直に上から評価していくと(nevero)
で止まっちゃうんじゃないかなあ
評価する前にこれは(#s)
からやったほうがいいぞ・・・ってわかる?
そんなことはなさそうな気がするけど
(run 1 q
(conde
(#s)
((nevero)))
#u)
1回目はconde
が#s
になるけど#u
との連言で#u
2回目は違うルートを通ろうとして(nevero)
を評価するので値なし
やっぱ「(nevero)
を評価するので値なし」なんだよなあ
さっきのはどうやって(nevero)
を避けてるんだろうか
(run 5 q
(conde
((nevero))
((alwayso))
((nevero))))
(_0 _0 _0 _0 _0)
を返すそうですが、やっぱり不思議なチカラで
(nevero)
を避けてるとしか思えない
(defrel (very-recursiveo)
(conde
((nevero))
((very-recursive))
((alwayso))
((very-recursive))
((nevero))))
今までの例からして何度でも成功しそうなことはわかるけれども
どうやって無限ループを避けているのかはわからない
それとも無限ループじゃないんだろうか