Reasoned Schemer (83) appendo 続き2

でも!
appendoの再帰を最後に持ってくると終わるんだって

(defrel (appendo l t out)
  (conde
    ((nullo l) (== t out))
    ((fresh (a d res)
       (conso a d l)
       (conso a res out)
       (appendo d t res)))))

確かに

> (run 4 (x y) (appendo x y '(ice cream)))
'((() (ice cream))
  ((ice) (cream))
  ((ice cream) ()))

ふんいきはわかる
再帰する前に可能性を搾っておいた方が扱いやすくはなりそう

昨日と同じように考えてみる

(appendo x y '(ice))

はまずcondeの1行目で(nullo x) (== y '(ice))から
x == '(), y == '(ice)になる
ここは同じ

condeの2行目では
(conso a1 d1 x)からx == ``(,a1 . ,d1)となって
前回は(appendo d1 y res1)を評価してたけど今回は(conso a1 res1 '(ice))の評価が先
a1 == 'ice、res1 == '()となって(appendo d1 y '())を評価
（実際にはそうじゃなくて(appendo d1 y res1)にres1 == '()を渡してる形だけど）
（たぶんこう考えても大丈夫なんじゃ）

condeの1行目で(nullo d1) (== y res1)からd1 == '(), y == '()になって
ひとつ上に戻りx == ``(,a1 . ,d1) == '(ice)

ここからが山場
appendoのcondeの2行目
(conso a2 d2 d1)からd1 == ``(,a2 . ,d2)
(conso a2 res2 '())を満たすa2、res2の組は存在しないのでここで空のstreamが返されて
のこりの式は評価されない

ここで止まる
ということ
たぶん

止まるパターンと比較すると要するに`(appendo x y z)でxもyもzもfreshな状態で
評価したらそりゃ終わらんよねもうちょっと条件与えてやれって話

しかしちょっと変えただけで止まらなくなるというのはデリケートが過ぎるのではないか
delayすることで無限ループ避けたみたいな手法が何かないのか

でもcondeの中の行を入れ替えても結果には影響はない
というのがLawになっているし実際そうなんだけど
処理系の実装のどこがそれを保証しているのか

condeの本体はdisj2でdisj2はほぼappend-inf
append-infの(append-inf t-inf (s-inf))のあたりが雰囲気を醸し出しているけど
勝手に雰囲気を割り当てているだけかもしれない
前後の行の評価結果に影響を受けないからってだけかな

unwrapはcondeはどこかで成功しても残りの行を忘れたりしないことがわかってれば不思議なところはない
はずだ！

どういうときに「意外な」結果になるのかというと？
condeの行が複数有効なとき、ってどんなとき？
ってそんなときだけど
行がそれぞれ排他じゃないとき、っていうとそれっぽいのか