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

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

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

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

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

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

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

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

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

ではコードを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)

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

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

(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)

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

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

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

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

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

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

えーと どうなってんの > (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個めを探しにいこうとして見つからないってことか

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

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

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

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

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

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

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

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

でも! 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))))) たとえば