kb84tkhrのブログ

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

Reasoned Schemer (91) addero, +o, -o, lengtho

adderogen-addero
genとはなんだろう

(defrel (addero b n m r)
  (conde ((== 0 b) (== '() m) (== n r))
         ((== 0 b) (== '() n) (== m r) (poso m))
         ((== 1 b) (== '() m) (addero 0 n '(1) r))
         ((== 1 b) (== '() n) (poso m) (addero 0 '(1) m r))
         ((== '(1) n) (== '(1) m)
          (fresh (a c)
            (== `(,a ,c) r)
            (full-addero b 1 1 a c)))
         ((== '(1) n) (gen-addero b n m r))
         ((== '(1) m) (>1o n) (>1o r) (addero b '(1) n r))
         ((>1o n) (gen-addero b n m r))))

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

adderoは横幅あったほうが見やすいな
どれどれ

> (run 19 (x y r) (addero 0 x y r))
'((_0 () _0)
  (() (_0 . _1) (_0 . _1))
  ((1) (1) (0 1))
  ((1) (0 _0 . _1) (1 _0 . _1))
  ((1) (1 1) (0 0 1))
  ((0 _0 . _1) (1) (1 _0 . _1))
  ((1) (1 0 _0 . _1) (0 1 _0 . _1))
  ((1) (1 1 1) (0 0 0 1))
  ((1 1) (1) (0 0 1))
  ((1) (1 1 0 _0 . _1) (0 0 1 _0 . _1))
  ((0 1) (0 1) (0 0 1))
  ((1) (1 1 1 1) (0 0 0 0 1))
  ((1 0 _0 . _1) (1) (0 1 _0 . _1))
  ((1) (1 1 1 0 _0 . _1) (0 0 0 1 _0 . _1))
  ((1) (1 1 1 1 1) (0 0 0 0 0 1))
  ((1 1 1) (1) (0 0 0 1))
  ((1) (1 1 1 1 0 _0 . _1) (0 0 0 0 1 _0 . _1))
  ((1) (1 1 1 1 1 1) (0 0 0 0 0 0 1))
  ((1 1 0 _0 . _1) (1) (0 0 1 _0 . _1)))

これ、本と出てくる順番が違うんだけど大丈夫かな
この3つが出てこない

((1 1) (0 1) (1 0 1))
((0 1) (1 1) (1 0 1))
((1 1) (1 1) (0 1 1))

見つけられないわけではなさそう

> (run 11 out (fresh (x y r) (addero 0 `(,x 1) y r) (== `((,x 1) ,y ,r) out)))
'(((_0 1) () (_0 1))
  ((0 1) (1) (1 1))
  ((1 1) (1) (0 0 1))
  ((0 1) (0 1) (0 0 1))
  ((0 1) (0 0 _0 . _1) (0 1 _0 . _1))
  ((0 1) (1 1) (1 0 1))
  ((0 1) (0 1 1) (0 0 0 1))
  ((0 1) (0 1 0 _0 . _1) (0 0 1 _0 . _1))
  ((0 1) (1 0 _0 . _1) (1 1 _0 . _1))
  ((1 1) (0 1) (1 0 1))
  ((1 1) (1 1) (0 1 1)))

ただ中身まで考えるとこれで見つかってるのが本当にadderoが正しく動いてる
証拠になるのかというとすこし自信がない
まあいいか順番関係ないって言ってたしな

overlappingしてるんだよな
1周目で表にしてた

+o-olengthoは特に気になるところなし