Reasoned Schemer (100) わり算 続き3

/o自体は問題ない

(defrel (/o n m q r)
  (conde
    ((== '() q) (== r n) (<o n m))
    ((== '(1) q) (=lo m n) (+o r m n) (<o r m))
    ((poso q) (<lo m n) (<o r m) (n-wider-than-mo n m q r))))

n-wider-than-moは数式と見比べつつ読んでいきたい
n-wider-than-moっていうのは何をするか、じゃなくて
nがmよりも長いとき（のわり算）ってことなんだな
今ごろ納得した

(defrel (n-wider-than-mo n m q r)

これはn = m*q + rに対応

  (fresh (nhigh nlow qhigh qlow)
    (fresh (mqlow mrqlow rr rhigh)

freshを2回に分けているのはどういうことか
1行にまとめても動きは変わらないっぽい
本の横幅の都合上かな？それだけ？

      (splito n r nlow nhigh)
      (splito q r qlow qhigh)

pをrの長さ+1とするとこれは

n = nhigh*2^p + nlow
q = qhigh*2^p + qlow

に対応
次はcondeに入って

      (conde
        ((== '() nhigh)
         (== '() qhigh)
         (-o nlow r mqlow)
         (*o m qlow mqlow))

これは基底ケースになっているのかな
（相互に再帰してるので基底ケースは/oにもある）

nhigh=0でqhigh=0だからn = nlowでq = qlow
nlow - r = m*qlowとなるnlow、r、m、qlowを探す
r<mであることは/o内で指定済みなのでいいとして
これはここで上限なしの再帰に入らない保証があるの？

        ((poso nhigh)
         (*o m qlow mqlow)
         (+o r mqlow mrqlow)
         (-o mrqlow nlow rr)
         (splito rr r '() rhigh)
         (/o nhigh m qhigh rhigh))))))

nhighが0でない
m*qlow + r - nlowをrでsplitoして()とrhighにする

(splito rr r '() rhigh)はrhigh*2^p ＝ m*qlow + r - nlowに対応
そういうnやらmやらqやらrがあることを確認してから
(/o nhigh m qhigh rhigh))を計算する
ここが数式で説明のあったところだな

ここで再帰する
nhighをmで割ってみる、ってのはこのことか
いくらか問題が小さくなってることは間違いないのでいつか止まるってことだろう
q = qhigh*2^p + qlowで出てくるqhighと
nhigh = m*qhigh + rhighに出てくるqhighは（当然ながら）同じもので、
そうするとrhighは決まってしまうけれども
そのrhighは(splito rr r '() rhigh)を満たさなければならない
そうすると無限にいろんな値を試し続けることはなくなる、ということだね
わかってないけど

ここでnhighだとかが決まれば残りも芋づるで決まる、と

式との対応はついたがさて

何がいいかっていうと、最後のふたつの方程式をチェックするとき、nlowもqlowもみんな範囲が制限されててpビットに収まってるってこと

(splito n r nlow nhigh)で(splito q r qlow qhigh)で
((== '() nhigh)で(== '() qhigh)だと
nlowやqlowの長さはせいぜいrの長さ+1で、
そういう範囲に制限されてから(-o nlow r mqlow)が評価されて
（だからmrqlowの長さも制限されて）
そのあと(*o m qlow mqlow)が評価されるから止まる

とか

(splito n r nlow nhigh)で(splito q r qlow qhigh)だから
nlowやqlowの長さはせいぜいrの長さ+1で、
rhighも条件を満たすから(/o nhigh m qhigh rhigh)も止まるであろうと

うーん、ここまでかな
頭よすぎる人の考えることはわからない