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))))

今までの例からして何度でも成功しそうなことはわかるけれども
どうやって無限ループを避けているのかはわからない
それとも無限ループじゃないんだろうか