kb84tkhrのブログ

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

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-infappend-map-infifteoncedefrel(で定義されたgoal)の5つだけ
ifteonceのふたつはしばらく忘れてていいはずだから実質三つか