Reasoned Schemer (87) nevero 続き
後者は1回forceした後同じになるのかな
このへん、勘でもREPL頼りでもなくちゃんとわかって言えないものだろうか
一度は追ってみないとダメかなあ
((teacupo x) empty-s)
= ((lambda (s) (lambda () ((disj2 (== 'tea x) (== 'cup x)) s))) empty-s)
= (lambda () ((disj2 (== 'tea x) (== 'cup x)) empty-s))
= ((disj2 (== 'tea x) (== 'cup x)) empty-s)
= (append-inf ((== 'tea x) empty-s) ((== 'cup x) empty-s))
= (append-inf `(((,x . tea))) `(((,x . cup))))
= `(((,x . tea)) ((,x . cup)))
ってやってくのめんどいんだよなあ
もうちょっと見通しよく書けないか
(lambda () ...)
を{...}
、
`(((,x . tea)) ((,x . cup)))
を[[x:'tea]] [x:'cup]]
、とでも書いてみようか
`(((,x . tea) (,y . cup)))
なら[[x:'tea y:cup]]
((teacupo x) [])
= ((lambda (s) {((disj2 (== 'tea x) (== 'cup x)) s)}) [])
= {((disj2 (== 'tea x) (== 'cup x)) [])}
ここで止まってしまうんだけどtake-inf
がいるつもりでforceすると
= ((disj2 (== 'tea x) (== 'cup x)) [])
= (append-inf ((== 'tea x) []) ((== 'cup x) []))
= (append-inf [[x:'tea]] [[x:'cup]])
= [[x:'tea] [x:'cup]]
これだとただ1行が短くなってるだけだしそんなかわらないかなあ
forceしたことにするのではなくてそのまま中を評価してみるのはどうか
↓の延長線で
雰囲気的に書けば
((alwayso) empty-s)
は(() () () ...
て感じなんだな
こう
{((disj2 (== 'tea x) (== 'cup x)) [])}
= {[[x:'tea] [x:'cup]]}
forceすれば[[x:'tea] [x:'cup]]
が出てくるよってことで
alwayso
をやってみる
((alwayso) [])
= {((disj2 (succeed) (alwayso)) [])}
= {(append-inf ((succeed []) ((alwayso) [])))}
= {(append-inf [[]] {((disj2 (succeed) (alwayso)) [])})}
= {[[] {((disj2 (succeed) (alwayso)) [])}]}
さらに続ける
= {[[] {[[] {((disj2 (succeed) (alwayso)) [])}]}]}
= {[[] {[[] {[[] {((disj2 (succeed) (alwayso)) [])}]}]}]}
= {[[] {[[] {[[] {[[] ... ]}]}]}]}
ふんいきは出てる気がしないでもない
forceしてcarを取ると[]
がでてきてcdrはsuspensionだもんな
nevero
はどうか
((nevero) [])
= ((lambda (s) {((nevero) s)}) [])
= {((nevero) [])}
= {{((nevero) [])}}
= {{{((nevero) [])}}}
= {{{{...}}}}
こっちもそれっぽくはある
forceするとsupensionが返ってくるけどいくらforceしてもsubstitutionは出てこない
でこれが(conde ((nevero)) (succeed))
の理解に役立つのか
((conde ((nevero)) (succeed)) [])
= ((disj2 ((nevero)) (succeed)) [])
= (append-inf ((nevero) []) (succeed []))
= (append-inf {{{...}}} [[]])
= {(append-inf [[]] {{{...}}})} ; append-infはsuspensionを返す
= {[[] {{{...}}}]}
1回forceしてcarを取れば[]
が出てきてそのあとはいくらforceしてもsuspensionしか返ってこない
見やすくなっているのでは
うまくいってるみたいな感じ(自信なし
ちなみにdelayを返してくるのはappend-inf
、append-map-inf
、ifte
、once
、defrel
(で定義されたgoal)の5つだけ
ifte
、once
のふたつはしばらく忘れてていいはずだから実質三つか