Reasoned Schemer (17) addero中身

• はじめて読む人は114コマ目まで飛ばしていいよ

でも読む

やっぱり2回は読めってことだな
Preface には書いてなかったけど
処理系まで理解してからもう一度読めばそりゃ間違いなく理解度は上がるもんな

nとmを足した答えがr 下からの繰り上がりはb

(defrel (addero b n m r)
  (conde
    ((== 0 b) (== '() m) (== n r))

キャリーが0、mが0なら答えはn
これはもんだいないな

    ((== 0 b) (== '() n) (== m r) (poso m))

キャリーが0、nが0なら答えはm
かと思いきやなぜかこっちだけmが正かどうかチェックが入っている
なんだこれ
nもmも()だっていいんじゃない？
あ、non-overlapping propetyってやつになるようにするためか
nもmも()なのは上の行でカバーしてるから

気分的には条件を左に書きたいような？

    ((== 0 b) (== '() n) (poso m) (== m r))

一長一短か
それとも見かけ以外にも理由があるかな？

    ((== 1 b) (== '() m) (addero 0 n '(1) r))
    ((== 1 b) (== '() n) (poso m) (addero 0 '(1) m r))

キャリーが1でnが0なら、キャリーが0でnが1の足し算と同じ
キャリーが1でmが0なら、キャリーが0でmが1の足し算と同じ

こっちはposoのほうが左だな・・・

    ((== '(1) n) (== '(1) m)
     (fresh (a c) (== `(,a ,c) r) (full-addero b 1 1 a c)))

nもmも1ならfull-adderが使える、と
full-adderで出てきたキャリーは末尾に付け足す

    ((== '(1) n) (gen-addero b n m r))

ここ、ひとつ上と条件カブってない？
いいの？

    ((== '(1) m) (>1o n) (>1o r) (addero b '(1) n r))    

上の反対だけど、gen-adderoを呼ぶときにnとmを入れ替えてadderoを呼び直す
とひとつ上の行にマッチする、って寸法だな
たぶんnが0ではgen-adderoがちゃんと動かないんだろう
rの条件が何を守っているのかは不明
adderoがへんな値を返してくるから防ぐ、みたいな感じ？
でもn=1のときはそんなガードしてないからなあ
なんだろうなあ

    (>1o n) (gen-addero b n m r)))

それ以外はgen-adderoで