Reasoned Schemer (45) 10章 unify

unify
Prologといえばユニフィケーションって出てくるくらいだからきっと何か大事なもの

(define (unify u v s)
  (let ((u (walk 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をsでwalkする

uとvはvariableでsはsubstitution、でいいんだっけ？
sはいいけどuとかvはvalueだったかな
vだとどっちもあるな
そういうとこ忘れるから理解できなくなってくんだよ

(ext-s x v s)のxはvariableでvはvalueって書いてある
((var? u) (ext-s u v s))も((var? v) (ext-s v u s))もあるから
どっちもvariableだったりvalueだったりするのか

(walk v s)のvもどっちでもいいんだっけ？
(var? v)って判定してるくらいだからやっぱりvariableとは限らないのか
associationのcarは必ずvariableってことでいいんだよな

walkの値っていうのはひとことでなんと言えばいいのかな
変数の値、とまではまだ行っていないし
walkしたもの、としか表現できない
まだ概念として呑み込めてないってことだろう
といっても本にも “walk’d value” って書いてあるからそんなものか

unifyはひとことで言えるだろうか

uをwalkしたものとvをwalkしたものが同じならsをそのまま返す
つまりunifyはsubstitutionを返す

そうでなくて
uがvariableなら(ext-s u v s)を返す
(ext-s u v s)はuからvへのassociationをsに追加したものを返す
そうでなくて
vがvariableなら同様にしてvからuへのassociationをsに追加したものを返す

uとvが両方variableなら両方追加、はしなくていいのかな
両方variableだったら必ず((eqv? u v) s)?
いやそんなことはないな
てことは片方やっておけば用はたりるっていうことなんだな

片方しか追加してないけど、uとvは同じです、っていうことにするのが
unifyがやることらしい

そうでなくて
uもvもpairならuのcarとvのcarは同じです、っていうことにして
さらにuのcdrとvのcdrは同じです、ってことにする

そうでなければ#f
これはunifyできませんでしたってことだろう

なんかelseの前にもう少しありそうな気がするんだけどどうなの
片方がpairでもう片方が・・・pairでない・・・って何だ
variableならも引っかかってるか
pairとアトムじゃ同じになりようがないし
どうやら大丈夫

ところでwalkやext-sには具体的な例があったのにunifyにはない
ちょっと自前で練習する

> (unify x y empty-s)
((#(x) . #(y)))
> (unify x 'e empty-s)
((#(x) . e))
> (unify x y `((,x . ,y)))
((#(x) . #(y)))
> (unify x 'e `((,x . ,y)))
((#(y) . e) (#(x) . #(y)))
> (unify 'e x `((,x . ,y)))
((#(y) . e) (#(x) . #(y)))
> (unify `(,u ,v ,w) `(,x ,y ,z) empty-s)
((#(w) . #(z))
 (#(v) . #(y))
 (#(u) . #(x)))
> (unify `(,u ,v) 'e empty-s)
#f

だいたい把握
ext-sする前にwalkしてることを忘れそうになるけど
（あんまり実害はないかもしれない）