Reasoned Schemer (21) かけ算続き

• bound-*oが仕事をしないとたとえば(run 1 (n m) (>1o n) (>1o m) (*o n m '(1 1)))が値を返さない

それはそうですね
それはそういうものかと思ってた
終われるようにするんだ
bound-*oが何をすれば終わる？失敗しても次のn、mで試すだけなのでは？

というのはおいといて判定条件
n*m=rでn=rになったら止まる、ってことだけど
リストと見たときのnやmの長さがrの長さを超えないように、のほうがわかりやすいとのこと

でもrはわかってないけどいいんだっけ？
いいんだろうな

をふまえて定義を眺める

(defrel (bound-*o q p n m)

q = x * m = ((n - 1) / 2) * m
p = n * m

だけど、リストの長さで言えば
qは答え(p)を1ビット分短くしたもの、ってことでいいのかな

  (conde
    ((== '() q) (poso p))

同じくqは0、じゃなくて単に'()と見る
qが'()でpが正なら成功＝計算を続ける

    ((fresh (a0 a1 a2 a3 x y z)
       (== `(,a0 . ,x) q)
       (== `(,a1 . ,y) p)

xはqのcdr、yはpのcdr

      (conde
        ((== '() n) (== `(,a2 . ,z) m) (bound-*o x y z '()))

nが'()ならzはmのcdrとしてbound-*oを評価
(bound-*0 (cdr q) (cdr p) (cdr m) '())ってことだな
つぎは(元の)mを(元の)nの位置に持ってきてこっち減らしていくぞ、と

        ((== `(,a3 . ,z) n) (bound-*o x y z m)))))))

(bound-*o (cdr q) (cdr p) (cdr n) m)を評価
この形だとnが'()でない、っていう条件も入るわけか
お、ということは上の形もそうか
nもmも'()になっちゃったらどちらもマッチしないんだ つまり失敗

再帰していってnもmも'()になる前にqが'()になれば成功なんだな

qもpも'()になることってあるのか、が疑問だけどだいたいわかった
単体では

しかしそれでどうして(run 2 (n m) (*o n m '(1)))が(((1) (1)))を返して
終了するようになるんだろう
n=2、m=2でbound-*oが失敗しても、n=3、m=3を試したらもしかして成功するかもしれないじゃないですか
そんなはずはない、ってわかるほど賢いの？