Reasoned Schemer (78) caro、cdro、conso

リストの操作
まずはcaro

> (defrel (caro p a) (fresh (d) (== (cons a d) p)))
> (run* q (caro '(a c o r n) q))
'(a)

なんでconsが理解できるんだろうと思ってたけどunifyとかがリストを前提とした作りになってるからだな
ていうかむしろリストしか知らない
たとえばvectorもunifyできるようにしようと思ったらunifyを拡張しないといけないんだろうな

やっていく

> (run-goal #f (caro '(a c o r n) q))
'(((#(d) c o r n) (#(q) . a)))

そういうstreamができるのか
なるほど

  ((caro '(a c o r n) q) empty-s)
= ((fresh (d) (== (cons q d) '(a c o r n))) empty-s)
= ((fresh (d) (== `(,q . ,d) '(a c o r n))) empty-s)
= ((call/fresh 'd (lambda (d) (== `(,q . ,d) '(a c o r n)))) empty-s)
= (((lambda (d) (== `(,q . ,d) '(a c o r n))) (var 'd)) empty-s)
= ((== `(,q . ,d) '(a c o r n)) empty-s)
= `((,d c o r n) (,q . a)))

そういえばfreshからcall/freshのあたりどうなってんだっけと思って
書いてみたところ(var 'd)がいい感じに書けずに少々ゴマかした感がある
結局もとに戻る感じなんだけどどう書くとすんなりするの

それはそれとして(cons a d)が実は'(#(q) . #(d))だったりすることがわかってれば
普通にunifyできて不思議はない

cdroも同じ

> (defrel (cdro p d) (fresh (a) (== (cons a d) p)))
> (run* r (fresh (v) (cdro '(a c o r n) v) (fresh (w) (cdro v w) (caro w r))))
'(o)

いきなりunnestしてる例でややこしい
これはどんなstreamができているのか

> ((fresh (v) (cdro '(a c o r n) v) (fresh (w) (cdro v w) (caro w r))) empty-s)
'(((#(d) r n)
   (#(r) . o)
   (#(w) o r n)
   (#(a) . c)
   (#(v) c o r n)
   (#(a) . a)))

defrelを普通の定義に戻すと・・・？

> ((fresh (v) (cdro '(a c o r n) v) (fresh (w) (cdro v w) (caro w r))) empty-s)
#<procedure:...r/minikanren.rkt:76:10>
> (((((fresh (v) (cdro '(a c o r n) v) (fresh (w) (cdro v w) (caro w r))) empty-s))))
'(((#(d) r n)
   (#(r) . o)
   (#(w) o r n)
   (#(a) . c)
   (#(v) c o r n)
   (#(a) . a)))

forceしていけば同じstreamができる
disj2があれば順番が変わってきそうな気がする

conso

> (defrel (conso a d p) (caro p a) (cdro p d))
> (run* l (conso '(abc) '(d e) l))
'(((abc) d e))
> (run* x (conso x '(a b c) '(d a b c)))
'(d)

こっちの定義でも同じ

> (defrel (conso a d p) (== `(,a . ,d) p))
> (run* l (conso '(abc) '(d e) l))
'(((abc) d e))
> (run* x (conso x '(a b c) '(d a b c)))
'(d)

むしろこっちの定義をもとにしてcaro、cdroを定義するのでは
こうして

(defrel (caro p a) (fresh (d) (conso a d p)))
(defrel (cdro p d) (fresh (a) (conso a d p)))

こう

> (run* q (caro '(a c o r n) q))
'(a)
> (run* r (fresh (v) (cdro '(a c o r n) v) (fresh (w) (cdro v w) (caro w r))))
'(o)

って後で出てきてたわ
完全に忘れてた