Reasoned Schemer (26) わり算 続き

三つ目のconde行は十分一般的に見えますが、なぜはじめの二つのconde行が必要なんですか？

これでいいんじゃないの、って話

(defrel (/o n m q r)
  (fresh (mq)
    (<o r m)
    (<=lo mq n)
    (*o m q mq)
    (+o mq r n))

これでは(run* m (fresh (r) (/o '(1 0 1) m '(1 1 1) r)))が値を返さなくなる、らしい
どういうとき値を返してどういうとき無限に試し続けるのか、気になってたんだよな

なぜかというと、こっちの/oは q が 1 より大きいとき m が n より小さいことを保証しないので
いつまでも 5 を割ると 7 になるような m を探し続けるとのこと
まあ探し続ける方はいいんですよ

もとの定義だと、 m が n より小さいことを保証してくれるので、m が n になったら
探索を止めることができる、というんですが
保証してくれると言ってもそれは(<o m n)のこと
実際やってみれば確かに m が n 以上のときには成功しないということはわかりますが
ここでは実際やってみることもなくやめてしまします
<oが組み込み関数だったらあらかじめそういうものだと教えておくこともできると思うんですが
ここでは

(defrel (<o n m)
  (conde
    ((<lo n m))
    ((=lo n m)
     (fresh (x) (poso x) (+o n x m)))))

から始まり<lo、=lo、+o、addero、gen-adder、full-adderなどといった
それほど単純ではない関係をいろいろ使ってて
これがm=(0 0 1)までは成功するけどm=(1 0 1)から先はずっと成功することはない、と
言い切るのはそれほど簡単じゃない気がするんですが

いったいどうやってるというの
little schemerシリーズに出てくる処理系でそこまで複雑で賢いことしてるとは思えないしなあ

さてここで

⇒ Hold on! It's going to get subtle! ⇐

ちょっと微妙なところだから気をつけろ、と言ってるんでしょうか
subtleは難しい

• (run 3 (y z) (/o `(1 0 . ,y) '(0 1) z '()))だと元の/oでもいろんな y や z を探してしまって値を返さない

さっきのよりも範囲を絞りづらいことはわかる
しかしこれもなにやら工夫すると即あきらめられるらしい