Reasoned Schemer (011) memo、rembero (わからん)

5. Members Only

またわからんタイトルを

(define (mem x l)
  (cond
    ((null? l) #f)
    ((equal? (car l) x) l)
    (#t (mem x (cdr l)))))

memだからか安直な
いやダブルミーニングが隠されてるかもしれないぞ気をつけろ

で、見つかると#tじゃなくてリストを返すやつね
翻訳して簡略化
真偽じゃない値を返すから引数を追加

(defrel (memo x l out)
  (conde
    ((caro l x) (== l out))
    ((fresh (d)
       (cdro l d)
       (memo x d out)))))

これもunwrapoと同じく、関数と違う答えを返します

> (run* out (memo 'fig '(fig fig pea out)))
((fig fig pea) (fig pea))

覚えておきましょう

はい

(define (rember x l)
  (cond
    ((null? l) '())
    ((equal? (car l) x) (cdr l))
    (#t (cons (car l) (rember x (cdr l))))))

見ないで翻訳してみる

(defrel (rembero x l out)
  (conde
    ((nullo l) (== '() out)
    ((fresh (a)
       (caro l a)
       (== a x))
     (cdro l out))
    (#s
      (fresh (res)
        (fresh (d)
          (cdro l d)
          (rembero x d res))
        (fresh (a)
          (caro l a)
          (cons a res out)))))))

おｋ
見ないで簡略化したり式を入れ替えたり

(defrel (rembero x l out)
  (conde
    ((nullo l) (== '() out)
    ((conso x out l))
    ((fresh (a d res)
       (conso a d l)
       (conso a res out)
       (rembero x d res))))))

ちょこちょこ間違えた ↑は修正済み
こいつも同様に、可能な答えを全部出す
カブってもおｋ

> (run* out (rembero 'pea '(pea pea) out))
((pea) (pea) (pea pea))

ということで

> (run* out
    (fresh (y z) (rembero y `(a b ,y d ,z e) out)))
((b a d _0 e)
 (a b d _0 e)
 (a b d _0 e)
 (a b d _0 e)
 (a b _0 d e)
 (a b e d _0)
 (a b _0 d _1 e))

なんだそうですがここでちょっとわからないところが

なぜ4番目の値が(a b d _0 e)なのですか。
リストからdが削除されているからです。
なぜまだリストがdを含んでいるのですか。
dを消すには、dがyと関連付けられてないといけません。

消えたdはもともとリストにあったdかと思ったんですが
yがdだとすると、そっちのdのほうが消えそうですね
そっちのほうが左だから
どっちが消えてるんだろう

さらに輪をかけて

なぜ5番目の値が(a b _0 d e)なのですか。
リストからzが削除されたからです。
なぜリストが_0を含んでいるのですか。
zをリストから削除するには、zがyとfuseされている必要があります。
これらの変数はfreshなままであり、リスト中のyは_0と具象化されます。

zに値が結びつかないうちに削除されるの？
てっきり具体的な値と結び付けられてから削除されるものと思ってた
そしてfuseされたのならより左にあるyの方が削除されそうな気がする
これはどういうことなんだ