microKanrenで始めるlogic programming入門 (2)

scheme logic programming

単一化しようぜ

==の動作を見てみよう。

(define (== u v)
  (lambda (s/c)
    (let ((s (unify u v (car s/c))))
      (if s (unit `(,s . ,(cdr s/c))) mzero))))

前にも説明したように(== u v)はuとvが同一であることを宣言している。この時==は引数のstateであるs/cを拡張してuとvが同じ値になるような代入を持つstateを作る関数を生成する。実際にある代入sの下でuとvが同じ値になるような代入を探すのがunifyだ。

(define (unify u v s)
  (let ((u (walk u s)) (v (walk v s)))
    (cond
      ((and (var? u) (var? v) (var=? 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 (and (eqv? u v) s)))))

unifyの動作例を並べてみる。

(unify #(0) 3 ())
; => ((#(0) . 3))

(unify 3 #(1) ())
; => ((#(1) . 3))

(unify 4 4 ())
; => ()

(unify 2 4 ()
; 単一化に失敗すると#fを返す
; => #f

(unify #(0) #(1) '((#(0) . 1)))
; => ((#(1) . 1) (#(0) . 1))

(unify #(0) 2 '((#(0) . 1)))
; 代入と矛盾してるので失敗
; => #f

(unify (list #(0) 2) (list 3 #(1)) mzero)
; リスト同士の単一化もできる
; => ((#(1) . 2) (#(0) . 3))