Reasoned Schemer (56) 10章 reify-s, reify, run-goal

reifyするっぽい何か

(define (reify-s v r)
  (let ((v (walk v r)))
    (cond
      ((var? v)
       (let ((n (length r)))
         (let ((rn (reify-name n)))
           (cons `(,v . ,rn) r))))
      ((pair? v)
       (let ((r (reify-s (car v) r)))
         (reify-s (cdr v) r)))
      (else r))))

rはreified-name substitution
``((,z . _2) (,y . _1) (,x . _0))みたいなやつ（のはず
(walk v r)すると_1とかが返ってくるのかな？
でもそうするとpairが返ってくることはないか
いや（普通の）変数すら返ってこないか
``((,x . _0) (,w . (,x e ,z)))みたいなのでもいいのかな

とりあえずwalkはできたとしよう
vが変数だったら（vはfreshってことだな）rにreified variableとのassociationをくっつける
vがpairだったらcarをreify-sしてからcdrをreify-sする
elseはなんだ
atomかreified nameかな
ということはつまりrの中のvをとことんまでreifyする
ってことでよろしいでしょうか

何か思い出しませんか？
unifyを思い出します

まったく思い出しませんでした
こういうの

(define (unify u v s)
  (let ((u (wal1k u s)) (v (walk v s)))
    (cond
      ((eqv? u v) s)
      ((var? u) (ext-s u v s))
      ((var? v) (ext-s v u s))
      ((and (pair? u) (pair? v))
       (let ((s (unify (car u) (car v) s)))
         (and s (unify (cdr u) (cdr v) s))))
      (else #f))))

似てると言えば似てる
uとvだったのがvだけになって、それに関連して変わるところが変わってるくらい
だから何というのはわからない

実例が出てこないので自前の例でちょっと試す

> (reify-s w `((,x . (d ,z)) (,z . ,y) (,w . (,x e ,v))))
((#(v) . _4)
 (#(y) . _3)
 (#(x) d #(z))
 (#(z) . #(y))
 (#(w) #(x) e #(v)))

そういう感じね
そしてreify
reified-name substitutionを使ってwalk*するだけ

(define (reify v)
  (lambda (s)
    (let ((v (walk* v s)))
      (let ((r (reify-s v empty-s)))
        (walk* v r)))))

これは一瞬goalかと思う形だけど返す値がsubstitutionのstreamじゃないな

> (reify w)
#<procedure:...r/minikanren.scm:100:2>
> ((reify w) `((,x . (d ,z)) (,z . ,y) (,w . (,x e ,v))))
((d _0) e _1)

たしかにwをreifyしてる

次はrun-goal
runっていう言葉が出てきたということは大詰めが近いってことだよな

(define (run-goal n g)
  (take-inf n (g empty-s)))

substitutionにgoalを適用して出てきたsubstitutionのstreamからいくつかとってくる

> (map (reify x) (run-goal 5 (disj2 (== 'olive x) (== 'oil x))))
(olive oil)

こういうのはどうだろう

> (map (reify x) (run-goal 5 (alwayso)))
(_0 _0 _0 _0 _0)

mapとreifyもまとめて関数に入れてないのはなぜですか