kb84tkhrのブログ

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

reasonedschemer

Reasoned Schemer (111) bumpo、gen&test+o、enumerate+o、enumerateo

bumpo (defrel (bumpo n x) (conde ((== n x)) ((fresh (m) (-o n '(1) m) (bumpo m x))))) これは問題ない

Reasoned Schemer (110) condu、onceo

condaは成功した節で止まってくれるとはいえ成功した節から帰ってこなくては無力 > (run* q (conda ((alwayso) succeed) (succeed fail))) (no value) run 1なら帰ってくる > (run 1 q (conda ((alwayso) succeed) (succeed fail))) '(_0) そこでconduの登場…

Reasoned Schemer (109) conda

なんだか/oで完結したみたいな気分になってましたが ここで少し流れが変わってconda、conduが登場 ここらへん、“The Second Commandment”が何を言っているのかよくわからなかった記憶 ひさしぶりに処理系の中身と関連付けながら見ていく こんどはわかるかな

Reasoned Schemer (108) logo 続き7

logoを使って足し算を定義する (defrel (++o n m k) (logo k n '(1) m))でいいんじゃね > (run* k (++o '(1 1) '(1 0 1) k)) '((0 0 0 1))

Reasoned Schemer (107) logo 続き6

(fresh (q1 bwq1) (+o q '(1) q1) (*o bw q1 bwq1) (

Reasoned Schemer (106) logo 続き5

(base-three-or-moreo n b q r)はbが3以上のときのn = b^q + rの関係 この(今まで出てきた関係の中では)巨大な関係がしかもcondeで分かれてないってすごいな 全部同時に成り立つってことだもんな

Reasoned Schemer (105) logo 続き4

base-three-or-moreoには恐れをなして先にlogo本体 (defrel (logo n b q r) (conde ((== '() q) (<=o n b) (+o r '(1) n)) n = b^q + rの関係であること、とは(という読み方をしてみる)

Reasoned Schemer (104) logo 続き3

bの意味がどうもつかめてないんだよな わかった bはやっぱりbaseなんだ exp2oは2の累乗(とその仲間たち)を求めるんだけどそれはbが()のときで bが(1)なら4の累乗、bが(1 1)なら8の累乗、bが(1 1 1)なら16の累乗って 考えたらいいんだ つまり(2の(bの長さ+1…

Reasoned Schemer (103) logo 続き2

確かに同じだ なんで同じなの bの意味がどうもつかめてないんだよな

Reasoned Schemer (102) logo 続き

ではコードを1行ずつ ((== '(1) n) (== '() q))はわかる ((>1o n) (== '(1) q) (fresh (s) (splito n b s '(1))))のnは bの長さ+1をpとしてp個の0または1に1をくっつけたもの 式で書けば2^(p + q) <= n < 2^(p + q + 1)

Reasoned Schemer (101) logo

1周目ではほとんどあきらめていたlogo とりあえずlogo以下コードを入力して動かしながらやっていこう 入力するだけでもなかなか大変 目がちかちかする ↓くらいで書けたら関係プログラミングすげー、っていうところなんだけどなあ

Reasoned Schemer (100) わり算 続き3

/o自体は問題ない (defrel (/o n m q r) (conde ((== '() q) (== r n) (

Reasoned Schemer (100) わり算 続き2

(split n r l h)はnからrの長さ+1だけ取ってlとし残りをhとする ただしlやhがちゃんとした数字になるようにする n: (0 0 1 0 1 1) r: (1 0 1) ↓ l: (0 0 1 ) h (1 1)

Reasoned Schemer (99) わり算 続き

さてそうやってガードを入れた/oもこういう式では値を返さない 確かにこれを途中で止めるのは難しそう > (run 3 (y z) (/o `(1 0 . ,y) '(0 1) z '())) user break しっくりこないところもあるけどだいたいストーリーは見えてきた

Reasoned Schemer (98) わり算

わり算ここだな一番わからなかったところ

Reasoned Schemer (97) 比較

えーとここからしばらくはわり算の準備、だったかな?ガードかける用に

Reasoned Schemer (96) *o 続き

本物のbound-*o (*o n m p)でn>pだったりm>pだったりしたら失敗するようにする んだけどそのかわりにnやmをリストとみてnやmがpより長かったら失敗するようにするらしい

Reasoned Schemer (95) *o

かけ算わり算の章 ここが最難関だったような *oは特に難しいところはない non-overlappingで再帰は最後ね

Reasoned Schemer (94) 符号付き 続き2

なんで止まるのか考えないと でも今回書いたコードには再帰してるとこないんだよな +oとか-oとかで止まってるのか? いくつか値を試してみたけどそういう雰囲気はない(あくまで雰囲気

Reasoned Schemer (93) 符号付き 続き

えーと どうなってんの > (check-sumo-augend -5 -5) user break > (check-sumo-augend 1 1) user break > (run* n (sumo n '(0 1) '(0 1))) user break > (run 1 n (sumo n '(0 1) '(0 1))) '(()) なるほど 2個めを探しにいこうとして見つからないってことか

Reasoned Schemer (92) 符号付き

符号付きの数を作ってそれ用の足し算を作る話 1周目に脳内で書いたコードはカッコの対応がついてないところだらけ あとdiff-sign-sumoで答えが0になるときの対応が抜けてることに気づいた

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

adderoとgen-addero genとはなんだろう

Reasoned Schemer (90) half-adder, full-adder, poso, >1oあたりまで

7. A Bit Too Much ビット演算から加算器作ったりする話 というか数を作る話と言った方がいいのかな

Reasoned Schemer (89) リベンジ?

delayしてるところがわかんねえ、って言ってスルーしてきたとこ、今ならわからないかなあ どういう順で答えが出てくるとか、何回forceすると答えが出てくるとか

Reasoned Schemer (88) nevero 続き2

> (run 1 q (conde (succeed) ((nevero))) fail) これが止まるのはだいたいイメージできるけど練習でやってみよう

Reasoned Schemer (87) nevero 続き

後者は1回forceした後同じになるのかな このへん、勘でもREPL頼りでもなくちゃんとわかって言えないものだろうか 一度は追ってみないとダメかなあ

Reasoned Schemer (86) nevero

今回のネタはこれ (defrel (nevero) (nevero)) 単純極まりない でも1周目では腑に落ちないところがいくつかあった

Reasoned Schemer (85) alwayso

6. The Fun Never Ends … この章(も)、1周目は消化不良気味だったけど今回はどうだろう (defrel (alwayso) (conde (succeed) ((alwayso)))) とりあえず一回succeedしてさらにもう一度 ということはすんなりわかるようになった

Reasoned Schemer (83) appendo 続き2

でも! appendoの再帰を最後に持ってくると終わるんだって

Reasoned Schemer (82) appendo

appendoはoutに結果をunifyするだけだから動き的に新しいところはない、かな? (defrel (appendo l t out) (conde ((nullo l) (== t out)) ((fresh (a d res) (conso a d l) (appendo d t res) (conso a res out))))) たとえば