kb84tkhrのブログ

何を書こうか考え中です あ、あと組織とは関係ないってやつです 個人的なやつ

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

これで計算はできてしまう

qqlowqdに分けて何をやっているのか
qddってなんだろう
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)bw1bの長さになる
wはwidthのwかな
lengthoと同じ?と思ったけどlengthoは一般のリストが対象だからちょっと違うか

    (<lo q n)

それはそうだろう
bは3以上でnbより長いときしかbase-three-or-moreoは評価されない
nの長さは3以上
間違いない

続きのゴールを評価する前に範囲を狭めておく効果もあるかな