Reasoned Schemer (89) リベンジ？

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

  ((teacupo x) [])
= ((lambda (s) {((disj2 (== 'tea x) (== 'cup x)) s)}) [])
= {((disj2 (== 'tea x) (== 'cup x)) [])}
= {(append-inf ((== 'tea x) []) ((== 'cup x) []))}
= {(append-inf [[x:'tea]] [[x:'cup]])}
= {[[x:'tea] [x:'cup]]}

たぶんこれだと長すぎて要点が見えなくて暗算できない
短く書けばこれくらいかな

  ((teacupo x) [])
= {((disj2 (== 'tea x) (== 'cup x)) [])}
= {(append-inf [[x:'tea]] [[x:'cup]])}
= {[[x:'tea] [x:'cup]]}

goalをdefrelで書き直すときは1回delayする、ってだけでいいだろうか
でもdisj2の中にまたdefrelで定義されたgoalが出てくるとそんな単純じゃないか
あんまり短くはできないかもしれない

append-infを中置演算子風に書くともっと短くできるか
でも行数が減るわけじゃないしなあ

  ((conj2 (teacupo x) (teacupo y)) [])
= (append-map-inf (teacupo y) ((teacupo x) []))
= (append-map-inf (teacupo y) {[[x:'tea] [x:'cup]]})
= {(append-map-inf (teacupo y) [[x:'tea] [x:'cup]])}
= {(append-inf ((teacupo y) [x:'tea]) (append-map-inf (teacupo y) [[x:'cup]]))}
= {(append-inf {[[y:'tea x:'tea] [y:'cup x:'tea]]} (append-map-inf (teacupo y) [[x:'cup]]))}
= {{(append-inf (append-map-inf (teacupo y) [[x:'cup]]) [[y:'tea x:'tea] [y:'cup x:'tea]])}}
= {{(append-inf (append-inf ((teacupo y) [[x:'cup]]) (append-map-inf (teacupo y) [])) [[y:'tea x:'tea] [y:'cup x:'tea]])}}
= {{(append-inf (append-inf {[[y:'tea x:'cup] [y:'cup x:'cup]]} []) [[y:'tea x:'tea] [y:'cup x:'tea]])}}
= {{(append-inf {(append-inf [] [[y:'tea x:'cup] [y:'cup x:'cup]])} [[y:'tea x:'tea] [y:'cup x:'tea]])}}
= {{(append-inf {[[y:'tea x:'cup] [y:'cup x:'cup]]} [[y:'tea x:'tea] [y:'cup x:'tea]])}}
= {{{(append-inf [[y:'tea x:'tea] [y:'cup x:'tea]] [[y:'tea x:'cup] [y:'cup x:'cup]])}}}
= {{{[[y:'tea x:'tea] [y:'cup x:'tea] [y:'tea x:'cup] [y:'cup x:'cup]]}}}

conj2が入るといきなり面倒
append-map-infのせい
forceの数とかに影響しそうでちょっと途中を抜くのがこわいせいもある
短くしたいけど、どこ省いていいかわからない
暗算は無理かー

次はfreshのあるパターンを

  ((caro '(a c) q) [])
= ((lambda (s) (lambda () ((fresh (d) (== `(,q . ,d) '(a c))) s))) [])
= (lambda () ((fresh (d) (== `(,q . ,d) '(a c))) []))
= {((fresh (d) (== `(,q . ,d) '(a c))) [])}
= {((call/fresh 'd (lambda (d) (== `(,q . ,d) '(a c)))) [])}
= {(((lambda (d) (== `(,q . ,d) '(a c))) (var 'd)) [])}
= {((== `(,q . ,d) '(a c)) [])}
= {[d:'(c) q:'a]}

なんか途中ゴマカしたけどfreshは考えなくていいことにしておこう
前に見たときもここはゴマカした

  ((caro '(a c) q) [])
= {((== `(,q . ,d) '(a c)) [])}
= {[d:'(c) q:'a]}

これくらいにしてしまう

あと再帰をできるところまでやってみよう
freshは省く

  ((nullo x) [])
= {((== x '()) [])}
= {[[x:'()]]}

  ((cdro x d) [])
= {((== (cons a d) x) [])}
= {[[x:(a . d)]]}

  ((listo x) []])
= {((conde ((nullo x)) ((cdro x d1) (listo d1))) [])}
= {((disj2 (nullo x) (conj2 (cdro x d1) (listo d1))) [])}
= {(append-inf ((nullo x) []) ((conj2 (cdro x d1) (listo d1)) [])}
= {(append-inf {[[x:'()]]} (append-map-inf (listo d1) ((cdro x d1) [])))}
= {(append-inf {[[x:'()]]} (append-map-inf (listo d1) {[[x:(a1 . d1)]]}))}
= {(append-inf {[[x:'()]]} (append-map-inf (listo d1) {[[x:(a1 . d1)]]}))}
= {(append-inf {[[x:'()]]} {(append-map-inf (listo d1) [[x:(a1 . d1)]])})}
= {{(append-inf {(append-map-inf (listo d1) [[x:(a1 . d1)]])} [[x:'()]])}}
= {{{(append-inf [[x:'()]] (append-map-inf (listo d1) [[x:(a1 . d1)]]))}}}
= {{{(append-inf [[x:'()]] (append-inf ((listo d1) [x:(a1 . d1)]) [])}}}
= {{{(append-inf [[x:'()]] (append-inf {((conde ((nullo d1)) ((cdro d1 d2) (listo d2))) [x:(a1 . d1)])} [])}}}
= {{{(append-inf [[x:'()]] (append-inf [] ((conde ((nullo d1)) ((cdro d1 d2) (listo d2))) [x:(a1 . d1)]))}}}
= {{{(append-inf [[x:'()]] ((disj2 (nullo d1) (conj2 (cdro d1 d2) (listo d2))) [x:(a1 . d1)]))}}}
= {{{(append-inf [[x:'()]] (append-inf ((nullo d1) [x:(a1 . d1)]) ((conj2 (cdro d1 d2) (listo d2)) [x:(a1 . d1)])))}}}
= {{{(append-inf [[x:'()]] (append-inf {[d1:'() x:(a1 . d1)]} (append-map-inf (listo d2) ((cdro d1 d2) [x:(a1 . d1)]))))}}}
= {{{(append-inf [[x:'()]] (append-inf {[d1:'() x:(a1 . d1)]} (append-map-inf (listo d2) {[[d1:(a2 . d2) x:(a1 . d1)]]})))}}}
= {{{(append-inf [[x:'()]] (append-inf {[d1:'() x:(a1 . d1)]} {(append-map-inf (listo d2) [[d1:(a2 . d2) x:(a1 . d1)]])}))}}}
= {{{(append-inf [[x:'()]] {(append-inf {(append-map-inf (listo d2) [[d1:(a2 . d2) x:(a1 . d1)]])} [d1:'() x:(a1 . d1)])})}}}
= {{{[[x:'()] . {(append-inf {(append-map-inf (listo d2) [[d1:(a2 . d2) x:(a1 . d1)]])} [d1:'() x:(a1 . d1)])}]}}}

3回forceしてx==()が出てきたということで満足しよう
途中で集中力が切れてちょっとあってる気がしない