kb84tkhrのブログ

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

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の書き方のせいでそうなるらしい

第1の戒律
ゴールの列の中で、再帰しないゴールは再帰するゴールよりも先に書くこと

つまりこう書けと

(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じゃないんだな