Reasoned Schemer (100) わり算 続き2
(split n r l h)
はn
からr
の長さ+1だけ取ってl
とし残りをh
とする
ただしl
やh
がちゃんとした数字になるようにする
n: (0 0 1 0 1 1)
r: (1 0 1)
↓
l: (0 0 1 )
h (1 1)
これは、r
がpビットの長さの数だとするとn = h*2^(p + 1) + l
となる関係に相当
((== '() n) (== '() h) (== '() l))
n=()
ならh=()、l=()
っていう見方だけじゃないんだけどな
n=()、h=()、l=()
なら成功、って読んだほうがいいのかな
ピンときづらい
((fresh (b n^)
(== `(0 ,b . ,n^) n) (== '() r)
(== `(,b . ,n^) h) (== '() l)))
r=()
でn
の最下位ビットが0ならばl=()
でh
は最下位ビットを取り払った数
^
はhigh
のことっぽい
((fresh (n^)
(== `(1 . ,n^) n) (== '() r)
(== n^ h) (== '(1) l)))
r=()
でn
の最下位ビットが1ならばl=(1)
でh
は最下位ビットを取り払った数
上のゴールと合わせるとn
が0でなくてr
が()
のときをカバーしている
((fresh (b n^ a r^)
(== `(0 ,b . ,n^) n)
(== `(,a . ,r^) r) (== '() l)
(splito `(,b . ,n^) r^ '() h)))
n
の最下位ビットが0でr
の長さが1以上ならば
l=()
としてn
とr
の最下位ビットを取り払って()
とh
に分け直し
((fresh (n^ a r^)
(== `(1 . ,n^) n)
(== `(,a . ,r^) r) (== '(1) l)
(splito n^ r^ '() h)))
n
の最下位ビットが1でr
の長さが1以上ならば
l=(1)
としてn
とr
の最下位ビットを取り払って()
とh
に分け直し
このふたつはl
の上位ビットが0だったときの対応をやってるってことみたい
とりあえずl
を()
なり(1)
なりにして試してみるけど
l
の上位ビットに1が出てくると失敗するっていう寸法
n=(0 1 1) r=(1)
とするとl=()
で(splito (1 1) () () h)
を評価する→失敗
n=(1 1 1) r=(1)
とするとl=(1)
で(splito (1 1) () () h)
を評価する→失敗
n=(0 0 1) r=(1)
とするとl=()
で(splito (0 1) () () h)
を評価する→h=(1)
n=(1 0 1) r=(1)
とするとl=(1)
で(splito (0 1) () () h)
を評価する→h=(1)
たぶんそう
((fresh (b n^ a r^ l^)
(== `(,b . ,n^) n)
(== `(,a . ,r^) r)
(== `(,b . ,l^) l)
(poso l^)
(splito n^ r^ l^ h)))))
n
もr
もl
も長さが1以上ならば最下位ビットを取り払って分け直し
1周目よりはわかってる感じするぞ