Reasoned Schemer (19) gen-addero

さてgen-addero
ある意味こっちが本体？

genは何のgenかな
特殊ケースを除いた残りだから、genericのgenだろうか

(defrel (gen-addero b n m r)
  (fresh (a c d e x y z)
    (== `(,a . ,x) n)

nの最下位ビットがa、上位ビットがx
nは1以上でないと困るね

    (== `(,d . ,y) m) (pos y)

mの最下位ビットがd、上位ビットがy ただしyは正
ってことはmは2以上？そんな条件だったかな？
・・・お、そうだな 明示はされてないけど
nが1のときもあるからxにはこの条件はつけない、って書いてある

なんでcdrでもないのにdなん？

    ((== `(,c . ,z) r) (poso z))

rの最下位ビットがc、上位ビットがz
とすると、addero7行目のrの条件は自動的に満たされそうな気がするけど・・・？
なにか想定できてないケースがあるかな？

    (full-addero b a d c e)

下からのキャリーと、nの最下位ビットと、mの最下位ビットを足す

    (addero e x y z)))

最下位ビットからのキャリーと、nの上位ビットと、mの上位ビットを足す

なるほど足し算されるな
(run* (x y) (addero x y '(1 0 1)))ってすると足すと5になる組み合わせがすべて出てくる

しかしどうも、想定外のルートがないかどうかが自信持てない
nonground valueみたいなのもあるし
数と思い込んでるから、2進数表現から外れた形のことまで考えてないし

影法師に注意しなければなりません。(Scheme手習い)

ここで113コマめ
ここまでは必須じゃないってこと！