Reasoned Schemer (98) わり算

わり算
ここだな
一番わからなかったところ

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

うまい具合に0割をさけている
本体はfreshの中身
n=mq+r (m≠0、r<m)となるn、m、q、rを探す

<oじゃなくて<=loでガードをかけてるのはその方が簡単だから、だけの話？
このあとガードの話がややこしくなるので少しゆっくり考える

上の/oだと
(run* m (fresh (r) (/o '(1 0 1) m '(1 1 1) r)))は
mが5になるとガードにひっかかって探すのをやめる
qが1より大きければmがnより保証してくれるから、っていうのは
(<=lo mq n)のことを言ってそうだけどでもそもそも(<o m n)があるよね？
何を言おうとしているのか

わり算の定義は一見これでもよさそうに見えるけど、

(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)))が止まらなくなる
こっちはqが1より大きいときにmがnより小さいことを保証しないという
(<=lo mq n)のことを言ってるのではないのかなあ
(<o m n)はなくなってる

qが0だとmはなんでもありになってしまうけど
ここではqは7ってことになってるし

nが5で
最初の定義だとmはnより小さい
二番目の定義ではmはnより小さいというゴールはなくて
mqがnより小さいというゴールがあるだけ
mqはfreshだからなんでもありになってしまう？
いやそんなことはないよな

> (run* mq (<=lo mq '(1 0 1)))
'(() (1) (_0 _1 1) (_0 1))

2番目の定義に(<o m n)を追加してやると値を返すようになる
(<o m n)の有無が大事なんだろうか
なにかしっくりこない