Reasoned Schemer (79) Translationとか

さらっといく
nulloとpairo

> (defrel (nullo x) (== '() x))
> (run* q (nullo '(grape raisin pear)))
'()
> (run* q (nullo '()))
'(_0)
> (run* x (nullo x))
'(())
> (defrel (pairo p) (fresh (a d) (conso a d p)))
> (run* q (pairo (cons q q)))
'(_0)
> (run* q (pairo '()))
'()
> (run* q (pairo 'pair))
'()
> (run* x (pairo x))
'((_0 . _1))
> (run* r (pairo (cons r '())))
'(_0)

ひとつだけすこし詳しく見てみよう

  ((pairo x) empty-s)
= ((conso a d x) empty-s)
= ((== `(,a . ,d) x) empty-s)
= `(((,x . (,a ,d))))

  ((reify x) `((,x . (,a ,d))))
= '((_0 . _1))

もんだいない

このへんからTranslationの導入
Translationは処理系なくてもわかる話なんで読むだけ

singletono

(defrel (singletono l) (fresh (d) (cdro l d) (nullo d)))

例は出てこないので読み替えて作る

> (run* q (singletono '()))
'()
> (run* q (singletono (cons 'pea '())))
'(_0)
> (run* q (singletono '(sauerkraut)))
'(_0)