Reasoned Schemer (95) *o

かけ算わり算の章
ここが最難関だったような

*oは特に難しいところはない
non-overlappingで再帰は最後ね 

odd-*o

(defrel (odd-*o x n m p)
  (fresh (q)
    (bound-*o q p n m)
    (*o x m q)
    (+o `(0 . ,q) m p)))

bound-*oを除けば偶数のかけ算にもう1回かけられる数を足すってだけ
bound-*oがやってることの意味は体感しているけど本にしたがって進む

bound-*oを仮にこう定義する

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

当然これだとうまく行かない場合がでてくるわけだけど
これはどんな計算ならできるのかな

> (for ((n (range 0 5)))
    (for ((m (range 0 5)))
      (let ((bp (run* p (*o (build-num n) (build-num m) p))))
        (printf "~a * ~a = ~a\n" n m (show-num (car bp))))))
0 * 0 = 0
0 * 1 = 0
0 * 2 = 0
  :
4 * 2 = 8
4 * 3 = 12
4 * 4 = 16

ふたつの数をかけ算するのは普通にできるみたい

(run 1 n (*o n '(1) '(1 1))) → '((1 1))
(run 2 n (*o n '(1) '(1 1))) → '((1 1))
(run* n (*o n '(1) '(1 1))) → '((1 1))

これはいいみたい

(run 1 n (*o n '(1 1) '(1 1))) → '((1))
(run 2 n (*o n '(1 1) '(1 1))) → 帰ってこない

これでもうだめか
そうするとこれもだめだな

(run 1 n (*o n '(1 1) '(1))) → 帰ってこない

変数ふたつでも

(run 1 (n m) (*o n m '(1 1))) → '(((1) (1 1)))
(run 2 (n m) (*o n m '(1 1))) → '(((1) (1 1)) ((1 1) (1)))
(run 3 (n m) (*o n m '(1 1))) → 帰ってこない

やめどきがわからない、と
なんでわからないか確認しておこう
(*o n '(1 1) '(1 1))でいうと最初に(1)がみつかるのはいいとして
condeの6行目

         ((fresh (x y)
            (== `(1 . ,x) n) (poso x)
            (== `(1 . ,y) m) (poso y)
            (odd-*o x n m p))

で(==(,a . ,d)odd-*oを評価する
odd-*oを評価すると(== x ``(,a . ,d))っていうユルい条件で*oを呼んでしまう
でまたcondeの各節を評価する
再帰してるけど基底状態に近づいてないし
condeの全部の節が再帰しないうちに成功なり失敗なりしてくれないといつまでたっても終わらない
4行目はnが小さくなってるし5行目はnとmを入れ替えるだけだから問題ない