Reasoned Schemer (010) 戒律・法則・unwrap
いろんなパターンを試します
(run 5 x
(fresh (y)
`(appendo `(cake & ice . ,y) '(d t) x)))
の値は
(()
(_0)
(_0 _1)
(_0 _1 _2)
(_0 _1 _2 _3))
run*
だと帰ってこないパターンですね
なのに
(run* x
(fresh (z)
`(appendo '(cake & ice cream) `(d t . ,z) x)))
の値は`((cake & ice cream d t . _0))
だけ
なぜこのリストにはひとつしか値がないのですか?
再帰の間、t
が変化しないからです。そのため、z
はfreshなままです。リストがただひとつの値のみ含むのは、(cake & ice cream)
が変数を含んでおらず、また、appendo
のすべてのconde
行で考慮されるただひとつの値だからです。
「appendo
のすべてのconde
行で考慮されるただひとつの値だからです」がよくわからん
英語がわかってないのか、内容がわかってないのかもわからん
まあ、コードはわかるからいいか
l
はプロパーなリストでないといけないけどt
は何でもいい、ってのも関係してる気がする
(run 7 (x y) (appendo x y '(cake & ice d t)))
は帰ってこないらしい
7つめの値を探し続けるらしい
そうなの?6つ見つけたところであきらめてくれるんじゃないの?
と思ったら、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)))))
理由の説明はなし
関係型プログラミング一般の話なんだろうか
実装の問題な気もする
上から読んでいったときにわかりやすいのは入れ替える前の形なんだけどなあ
順番についてもうひとつ
conde
行の入れ替えの掟
ふたつのconde
行を入れ替えてもconde
が貢献する値には影響しない
掟っていうか法則かな
守るものじゃないんもんな
Scheme手習いとかで掟って出てきてたけど、あれは違う単語なんだろうか
ところで気になってたんですけど d t ってなんですか
時間の増分ですか
アイスクリームとなにか関係あるんですか
わかりません
(define (unwrap x)
(cond
((pair? x) (unwrap (car x)))
(#t x)))
実行すると
> (unwrap '((((pizza)))))
pizza
これを翻訳して簡略化
(defrel (unwrapo x out)
(conde
((fresh (a)
(caro x a)
(unwrapo a out)))
(== x out)))
実行すると
> (run* x (unwrapo '(((pizza))) x))
((((pizza)))
((pizza))
(pizza)
pizza)
おや
パニクるな
ありがとう、Douglas Adams (1952-2001)。
そこまでびっくりはしてませんけどね
ダグラスさんて誰?
unwrapo
はトリッキーな関係で、ふるまいが関数のunwrap
と一致しません。fuseを追いかけていけばpizza
の例も理解できるでしょう。
(省略されてしまうけど)#s
で始まる行は、正確にはelse
じゃないんだな