Reasoned Schemer (81) Chapter 3 残り

defrelもわかったことにするとだいたいわかった感じになるかなあ

> (run 5 x (lolo `((a b) (c d) . ,x)))
'(() (()) ((_0)) (() ()) ((_0 _1)))

こういうのもまじめに追いかければなぜこの順になるかわかるはずだけどそこまで元気は出ない
defrelのlambda ()とdisj2の(append-inf t-inf (s-inf))が複雑で

s-infがsuspensionだったら(append-inf t-inf (s-inf))で
forceされるからいつかは評価されるね、くらいまでだなあイメージできるのは
再帰の1場面を切り取って、確かにこの場合はうまくいくね、と場面場面で納得するくらいまでで
全体を一度にイメージすることはできなくて一抹の不安が残る感じ
Friedman先生たちはふんふんそうなるよね、くらいまで動きをイメージできるんだろうか

逆に言うと、この場合はこれで正しい、っていうのが書けると全体がイメージできてなくても
ちゃんと動いちゃったりするのが再帰で書く時のいいところってことなのかもしれんね

もうちょっとざっくりだとどうだろう

(defrel (lolo l)
  (conde
    ((nullo l))
    ((fresh (a) (caro l a) (listo a))
     (fresh (d) (cdro l d) (lolo d)))))

で(lolo ``((a b) (c d) . ,x))を評価する

condeの中はきっとnulloの行から先に評価すると信じる

(nullo ``((a b) (c d) . ,x)じゃないから
aが'(a b)で(listo a)は成功
dが``((c d) . ,x)で(lolo `((c d) . ,x))を評価

(nullo `((c d) . ,x)じゃないから
aが'(c d)で(listo a)は成功
dがxで(lolo x)を評価

ここで(null x)が成功してx=()
次は(listo a)が成功するaと(lolo d)が成功するdをconsしたxができるんだろう
つまりaもdも()
次となるとそろそろappend-infがどの項からforceするのか見えなくなってくる
結果からするとまず(listo a)のaが(_0)になってdはそのまま
その次はaは()でloloのdが(())になって
その次aが(_0 _0)でdが()か
まあそう動いてもいいよね、くらいの感じではある

あとはいろいろ入力して試していく
singletono loso membero proper-membero
不思議なことは起こってないようだ

うそです

> (run 1 x (membero 'e `(pasta e ,x fagioli)))
'(_0)

のあと試しにやってみた

> (run* x (membero 'e `(pasta e ,x fagioli)))
'(_0 e)

で一瞬おやっとなりました
でもわかるよ！