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日