Reasoned Schemer (94) 符号付き 続き2
なんで止まるのか考えないと
でも今回書いたコードには再帰してるとこないんだよな
+o
とか-o
とかで止まってるのか?
いくつか値を試してみたけどそういう雰囲気はない(あくまで雰囲気
ちょっとずつ範囲を狭めていくか
(run* n (sumo n '(0 1) '(0 1))) → 止まる
(run* (ns nn) (poso nn) (gen-sumo ns nn 0 '(1) '(0 1))) → 止まる
(run* (nn) (poso nn) (gen-sumo 0 nn 0 '(1) '(0 1))) → 止まる
(run* (nn res) (poso nn) (+o nn '(1) res) (== `(0 . ,res) '(0 1))) → 止まる
ここか!
(+o nn '(1) res)
がどんどんnn
とres
の組み合わせを作り続けて
(== ``(0 . ,res) '(0 1))
で失敗し続けてるんだな
(+o nn '(1) res)
と(== ``(0 . ,res) '(0 1))
を入れ替えて・・・
(run* (nn res) (poso nn) (== `(0 . ,res) '(0 1)) (+o nn '(1) res)) → '()
よし
・・・あれ?答えがなくていいんだっけ
いいのか nが0より大きいときってしてるからそうなるか
もうちょっと普通の場合だと?
(run* (nn res) (poso nn) (+o nn '(1) res) (== `(0 . ,res) '(0 0 1))) → 止まる
(run* (nn res) (poso nn) (== `(0 . ,res) '(0 0 1)) (+o nn '(1) res)) → '(((1) (0 1)))
よし
gen-sumo
を書き換えて・・・
(defrel (gen-sumo ns nn ms mn k)
(conde
((== ns ms) (fresh (res)
(== `(,ns . ,res) k) ; ここ
(+o nn mn res))) ; ここ
((== ns 0) (== ms 1) (diff-sign-sumo ns nn ms mn k))
((== ns 1) (== ms 0) (diff-sign-sumo ns nn ms mn k))))
これでいけるだろう
(run* n (sumo n '(0 1) '(0 0 1))) → 止まる
くっそー
あーここね
(defrel (diff-sign-sumo ns nn ms mn k)
(fresh (res)
(conde
((== nn mn) (== '() k))
((-o nn mn res) (poso res) (== `(,ns . ,res) k)) ; ここ
((-o mn nn res) (poso res) (== `(,ms . ,res) k))))) ; ここ
同じ同じ
(defrel (diff-sign-sumo ns nn ms mn k)
(fresh (res)
(conde
((== nn mn) (== '() k))
((poso res) (== `(,ns . ,res) k) (-o nn mn res)) ; こう
((poso res) (== `(,ms . ,res) k) (-o mn nn res))))) ; こう
(run* n (sumo n '(0 1) '(0 0 1))) → '((0 1))
よっしゃー
テストも通るよね
> (for ((m (range -5 5)))
(for ((r (range -5 5)))
(check-sumo-augend m r)))
>
よし
もうひとパターン
(define (check-sumo-addend n r)
(check-equal? (run* m (sumo (build-signed-num n)
m
(build-signed-num r)))
(list (build-signed-num (- r n)))))
> (for ((n (range -5 5)))
(for ((r (range -5 5)))
(check-sumo-addend n r)))
>
ok