next up previous
Next: 3.1 同一変数のバインディングが起こる場合 Up: ソフトウェア第三 講義資料 パターンマッチ,前向き推論,ユニフィケーション,後向き推論 Previous: 後ろ向き推論


3 変数を含むパターン同士のマッチングUnifyの定義

これまでのマッチング関数は,第一引数に変数が含まれていて,第二引数の方 には変数がないというものを考えていた.しかし,

<cl> (match '(?x a) '(a ?x))
FAIL
というように,?xがaにマッチングすることで本来マッチングが とれそうなものに対して用いることができない. そこで,変数を含むパターン同士のマッチングをとる関数unifyを 考える. 考え方は,マッチングと同じであるが, パターンが変数であった場合に変数のマッチングを行なっただけでなく, データ側も変数であった場合にその変数のマッチングを行なうとい形に なる.
(defun unify (p d &optional bindings)
  (cond
   ((variable-p p)
    (unify-variable p d bindings))
   ((variable-p d)
    (unify-variable d p bindings))
   ((or (atom p) (atom d))
    (unify-atom p d bindings))
   (t
    (unify-list p d bindings))))
そして,unify-variableの中で,バインディング情報の中から変数の バインディング値を得た場合に,その値とデータがunifyするかどうか を調べることで可能となる.
(defun unify-variable (p d bindings)
  (cond
   ((get-binding p bindings)
    (unify (lookup p bindings) d bindings))
   (t (add-binding p d bindings))))
どちらかがアトムの場合と,どちらもリストの場合には,マッチングと同様の 定義になる.
(defun unify-atom (a b bindings)
  (if (eql a b) bindings 'fail))
(defun unify-list (pat data bindings)
  (let ((car-bindings
         (unify (first pat)
                (first data)
                bindings)))
    (if (eq car-bindings 'fail)
        'fail
      (unify (rest pat) (rest data)
             car-bindings))))
このように定義すると,以下のように matchでは対応できなかったものが 扱えるようになる.
<cl> (match '(?x b) '(b ?x))
FAIL 
<cl> (unify '(?x b) '(b ?x))
((?X . B)) 
<cl> (match '(?x a b) '((?y) a ?y))
FAIL 
<cl> (unify '(?x a b) '((?y) a ?y))
((?Y . B) (?X ?Y)) 
<cl> (match '(?x a b ?x) '((?y) a ?y (b)))
FAIL 
<cl> (unify '(?x a b ?x) '((?y) a ?y (b)))
((?Y . B) (?X ?Y))
しかし,これは以下に示すように無限ループになってしまうバグがある.



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