3.3 同一変数を内部に含むパターンとのバインディングの場合

Next: 3.4 ユニファイの応用例 Up: 3 変数を含むパターン同士のマッチングUnifyの定義 Previous: 3.2 変数のバインディングが循環する場合

3.3 同一変数を内部に含むパターンとのバインディングの場合

上に述べた循環以外に，


<cl> (unify '?x '(f ?x))
((?X F ?X)) 
<cl> (unify '(?x ?x) '(?y (f ?y)))
((?Y F ?Y) (?X . ?Y))

という場合も問題で，FAILを返す必要があります．そこで，データの中にその変数が入っているかどうかを調べる occur-check を行なう．

(defun unify-variable (p d bindings)
  (cond
   ((eql p d) bindings)
   ((get-binding p bindings)
    (unify (lookup p bindings) d bindings))
   ((and (variable-p d) (get-binding d bindings))
    (unify p (lookup d bindings) bindings))
   ((occurs-check p d bindings)  'fail)
   (t (add-binding p d bindings))))

(defun occurs-check (v x bindings)
  (cond
   ((eq v x) t)
   ((and (variable-p x) (get-binding x bindings))
    (occurs-check v (lookup x bindings) bindings))
   ((consp x)
    (or (occurs-check v (car x) bindings)
        (occurs-check v (cdr x) bindings)))
   (t nil)))

これを用いると，


<cl> (unify '?x '(f ?x))
FAIL 
<cl> (unify '(?x ?x) '(?y (f ?y)))
FAIL

のようにマッチングされなくなる．

generated through LaTeX2HTML. M.Inaba 平成18年5月7日