kb84tkhrのブログ

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

Reasoned Schemer (18) adderoまとめ

表にしてみた

b n m r overlap 計算
1 =0   =0   6(n=1 m=0) 8(n=2 m=0) (== n r)
2 =0 =0 >0   -- (== m r)
3 =1   =0   6(n=1 m=0) 8(n=2 m=0) (addero 0 n '(1) r)
4 =1 =0 >0   -- (addero 0 '(1) m r)
5   =1 =1   6(n=1 m=1) (full-addero b 1 1 a c)
6   =1     1 3 5 (gen-addero b n m r)
7   >1 =1 >1 8(n=2 m=1) (addero b '(1) n r)
8   >1     1 3 7 (gen-addero b n m r)

1〜4行目で0が出現する場合、5〜7行目で1が出現する場合、8行目でその他の場合をカバーしてる

ところどころ non-overlapping にしようとしてるように見えたけど
全体的には overlapp のことは気にしてない感じかな
どういうポリシーなんだろう

条件つけてないとちゃんと動かない部分をガードしてるだけかな?
overlapしないようにするっていうのはそこまで絶対守るべきものではないのかな
掟とか戒律とかにはなってないし
重複してると同じ結果が複数回出てくることがある(んだよな?)程度の話、ってこと?

あと7行目のrの条件は何をガードしているの
これがないとどんな答えが出るの

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
これはもんだいないな

続きを読む

Reasoned Schemer (16) addero

90
adderoの定義は104コマめにあります。

なぜ前方参照?
しかもadderoややこしそう・・・

(run 3 (x y r) (addero 0 x y r))の値はなんですか。

((_0 () _0)
 (() (_0 . _1) (_0 . _1))
 ((1) (1) (0 1)))

値がそうなることは(順番を除けば)理解できる

((1) (1) (0 1))は ground value を表現していますか?
はい。
(_0 () _0)は ground value を表現していますか?
いいえ、具象化された変数を含んでいますから。

ground valueってのはまだ出てきてないよな
一般用語でもないよな(たぶん
これが定義と思ってればいいのか

次のコマに進む前に
ホットファッジサンデーを召し上がれ!

ホットが熱いなのか辛いなのかはわかりません
その後(run 19 (x y r) (addero 0 x y r))の値を見ながら

  • nonground value の x 、 yはどちらか一方に変数が現れるけれども両方に現れることはない
  • ground valueはnonground valueの形に表されないものばかりである
  • これは非重複属性の例

ふむ

Reasoned Schemer (015) 自然数

自然数の表現

  • ビット(0、1)のリスト
  • リストの先頭が20の位、末尾が最上位
  • 表現は一意
    • 最上位は0にならない
    • 自然数0の表現は()

自然数をビットによる表現に変換する

続きを読む

Reasoned Schemer (015) ビット演算

7. A Bit Too Much

bitです

(defrel (bit-xoro x y r)
  (conde
    ((== 0 x) (== 0 y) (== 0 r))
    ((== 0 x) (== 1 y) (== 1 r))
    ((== 1 x) (== 0 y) (== 1 r))
    ((== 1 x) (== 1 y) (== 0 r))))

これは単純

(defrel (bit-xoro x y r)
  (fresh (s t u)
    (bit-nando x y s)
    (bit-nando s y u)
    (bit-nando x s t)
    (bit-nando t u r)))

とも定義できるらしいけど意味がわからない

続きを読む

Reasoned Schemer (014) nevero

こんどはいっそうシンプルに

(defrel (nevero)
  (nevero))
  • #uは失敗するが、(nevero)は成功も失敗もしない

  • (run 1 q (nevero)) → 値なし

  • (run 1 q #u (nevero))()

1回目に#uで失敗するから

  • (run 1 q (conde (#s) ((nevero))))(_0)

1回目に#sで成功するから

  • (run 1 q (conde ((nevero)) (#s)))(_0)

1回目に#sで成功するから、らしいですよ

続きを読む

Reasoned Schemer (013) alwayso

6. The Fun Never Ends...

何がNever Endsなのかというと

(defrel (alwayso)
  (conde
    (#s)
    ((alwayso))))

これが終わらないってことか?

Schemeに戻せば (define (always) (cond (#t) (else (always))))
ただ#tを返すだけのコードだけれどもalwaysoはどう動くんだ?

  • (run 1 q (alwayso))(_0)を返す
  • #sは一度しか成功しないが(alwayso)は何度でも成功する
  • (run* q (alwayso))は値を返さない

run*は違った見つけ方が考えられる限りずっと探すってことのようだ
再帰の回数が違うだけでも違ってることになるらしい

  • (run 5 q (alwayso))(_0 _0 _0 _0 _0)を返す

q=_0を返す場合でも
いきなり#sのときと、1回再帰してから#sの場合は別として考える

  • (run 1 q (alwayso) #u)は値を返さない

(run* q (alwayso))は無限に値が見つかって値を返さない
こっちはひとつも見つからないけど探し続けて値を返さない

(run 1 q
  (== 'garlic q)
  (alwayso)
  (== 'onion q))

これは終わらないらしい
無理だってわかってもよさそうなものだけど
どうなったら探すのをやめるんだ?

(run 2 q
  (conde
    ((== 'garlic q) (alwayso))
    ((== 'onion q)))
  (== 'onion q))

これは値を返さない
とりあえずonionでひとつ値が見つかるけれども
qgarlicになってしまうといくらalwaysoを呼んでももうonion
見つけてくれない、ってことかなあ?

(run 5 q
  (conde
    ((== 'garlic q) (alwayso))
    ((== 'onion q) (alwayso)))
  (== 'onion q))

いっぽうこれなら好きなだけ値を出させることができる
こんどはonionコースでも繰り返しが起きるから、でいいのかな