Reasoned Schemer (106) logo 続き5
(base-three-or-moreo n b q r)
はb
が3以上のときのn = b^q + r
の関係
この(今まで出てきた関係の中では)巨大な関係がしかもconde
で分かれてないってすごいな
全部同時に成り立つってことだもんな
やっぱり(+o bq r n)
からさかのぼっていこうと思うけどその前に
(*o b bq bq1)
と(<o n bq1)
はセット
bq1 = b * bq = b^(q + 1)
で、もともとb^q <= n
だから
n < bq1
とあわせてb^q <= n < b^(q + 1)
r
が大きくなりすぎないための条件とみればよさそう
ではさかのぼり
n = bq + r
n = bqlow * bqd + r # (*o bqlow bqd bq) から
n = bqlow * b^qd + r # (repeated-mulo b qd bqd) から
n = b^qlow * b^qd + r # (repeated-mulo b qlow bqlow) から
n = b^qlow * b^(q - qlow) + r # (+o qlow qd q) から
n = b^q + r
これで計算はできてしまう
q
をqlow
とqd
に分けて何をやっているのか
qd
のd
ってなんだろう
qhigh
ってものあるんだよな
ほかの行では何をやっているのか
計算自体じゃないから条件を設定しているのかガードをかけているのか
そのへんを気にしつつ
(defrel (base-three-or-moreo n b q r)
(fresh (bw1 bw nw nw1 qlow1 qlow s)
(exp2o b '() bw1)
(+o bw1 '(1) bw)
bw1
がfreshなときは(exp2o b '() bw1)
はb
からbw1
を求める向きに考えていいのかなあ
そうでもないか
両方freshなときもありうるか
(exp2o b '() bw1) (+o bw1 '(1) bw)
でbw1
がb
の長さになる
wはwidthのwかな
lengtho
と同じ?と思ったけどlengtho
は一般のリストが対象だからちょっと違うか
(<lo q n)
それはそうだろう
b
は3以上でn
はb
より長いときしかbase-three-or-moreo
は評価されない
n
の長さは3以上
間違いない
続きのゴールを評価する前に範囲を狭めておく効果もあるかな