Reasoned Schemer (27) わり算 続き
でどうやるかなんですけど
どうやったらもっといい
/o
を定義して、66コマめのrun*
が値を持つようにすることができるでしょうか?
数がビットのリストで表されているので、リストを「head」と「rest」のふたつの部分に分けて問題を分割してみてはどうでしょう?
なにを言っているんだかわかりません
2進数で表現された数を2で割ってるんだから一桁ずつなにかするっていうのはわからなくもない
でもそれって2で割ったときのため用?他の数で割ったときにも適用できるのかな?
練習だから?
(defrel (splito n r l h)
n を l と h に分ける
head と rest はどこいった
r はよくわからないけど、(l の長さ)が (r の長さ + 1) になるように分けているっぽい
(conde
((== '() n) (== '() h) (== '() l))
n が()
なら h も l も()
((fresh (b ^n)
(== `(0 ,b . ,^n) n) (== '() r)
(== `(,b . ^n) h) (== '() l)))
n の最下位ビットが 0 で r が()
なら
h は n の cdr で l は()
`(0 . ,^n)
じゃないのは(0)
にならないようにするため
だよな?
((fresh (^n)
(== `(1 . ,^n) n) (== '() r)
(== ^n h) (== '(1) l)))
n の最下位ビットが 1 で r が()
なら
h は n の cdr で l は(1)
((fresh (b ^n a ^r)
(== `(0 ,b . ,^n) n) (== `(,a . ,^r) r)
(== '() l) (splito `(,b . ,^n) ^r '() h)))
n の最下位ビットが 0 で r が1個以上の要素を持つリストなら
l は()
で h は(splito (cdr n) (cdr r) '() h)
を満たすような h
左側のビットから削っていくわけだな
r の値は関係なし
・・・でもなんか変だなあ
(splito '(0 1 1) '(1) l h)
の l が()
になってしまいそうだけど・・・
l は(0 1)
になるはずでは?
((fresh (^n a ^r)
(== `(1 . ,^n) n) (== `(,a . ,^r) r)
(== '(1) l) (splito ^n ^r '() h)))
n の最下位ビットが 1 で r が1個以上の要素を持つリストなら
l は(1)
で h は(splito (cdr n) (cdr r) '() h)
を満たすような h
同上
((fresh (b ^n a ^r ^l)
(== `(,b . ,^n) n) (== `(,a . ,^r) r) (== `(,b . ,^l) l)
(poso l) (splito ^n ^r ^l h)))
上記以外なら・・・じゃないか
ここはoverlapしてるんだな(いいの?
n も r も1個以上の要素を持つリストなら
l、h は(splito (cdr n) (cdr r) ^l h)
を満たすようなl、hで
l は n の最下位ビットに l をつないだもの
こっちはそれっぽい気がする
4つめ、5つめのconde行の存在価値がよくわからない