lisp勉強１０日目ユニフィケーション - c21coterie @ ウィキ

http://www.geocities.jp/m_hiroi/xyzzy_lisp/abclisp23.html

変数のユニフィケーションについてリンク先で勉強。

リンク先コードで私が理解できた範囲のコメントを記述。

変数の統合は色々なパタンを考えると意外と難しそう。

 

 

; unify.l : ユニフィケーション

;

;           Copyright (C) 2003 Makoto Hiroi

;

 

;

; 要素はパターン変数か

; 

(defun variablep (pattern)

  (and (symbolp pattern)

       (char= #\? (char (string pattern) 0))));束縛変数だった

variablep

 

(defun add-binding (var value binding)

  (cons (cons var value) binding));束縛変数のkeyとvalueを追加

add-binding

 

;

; ユニフィケーション

;

(defun unify (pattern datum binding)

  (cond ((variablep pattern);束縛変数一つだったら

         (unify-variable pattern datum binding));束縛変数がいままで出てきたものだったらvalueにしてからこの関数に帰ってくる

        ((variablep datum)

         (unify-variable datum pattern binding));同じく束縛変数をvalueにしてからこの関数に帰ってくる

        ((and (atom pattern) (atom datum))

         (unify-atoms pattern datum binding));アトムになったので普通に変数として比較

        ((and (consp pattern) (consp datum))

         (unify-pieces pattern datum binding));まだリストなのでアトムになるまで分解していく

        (t 'fail)))

unify

 

 

;

; アトムとのユニフィケーション

;

(defun unify-atoms (pattern datum binding)

  (if (equal pattern datum) binding 'fail));比較したアトムが同じなら駄目

unify-atoms

 

 

;

; リストのユニフィケーション

;

(defun unify-pieces (pattern datum binding)

  (let ((result (unify (car pattern) (car datum) binding)));ここでcar patternとcar datumで一つのアトムにまで分解する作業を続ける

    (if (eq result 'fail)

        'fail

        (unify (cdr pattern) (cdr datum) result))));アトムの分解が終わったのでリストの次へ移動する

unify-pieces

 

 

;

; 変数とのユニフィケーション

;

(defun unify-variable (pattern datum binding);関数の呼び出し場所でこの関数のpatternは束縛変数一個になることが保証

  (let ((value (assoc pattern binding)));でてきた束縛変数が今まで出てきたものと同じか調べる

    (if (and value

             (not (eq pattern (cdr value))));今まで出てきた束縛変数と同じだった

        (unify (cdr value) datum binding);束縛変数を具体的な値にして再度unifyを実行

        (if (insidep pattern datum binding);束縛変数が残りのリストで出てこないことをチェック

            'fail

            (add-binding pattern datum binding)))));出てこなかったので追加

unify-variable

 

 

;

; datum の中に var があるか

;

(defun insidep (var datum binding)

  (unless (eq var datum);変数の統合が目的なので同じ束縛変数は無視する

    (inside-sub-p var datum binding)))

insidep

 

 

;

; insidep 本体

;

(defun inside-sub-p (var datum binding);この関数はチェックしか行わなわず他の関数と関係を持たない

  (cond ((eq var datum) t);同じ変数ならユニフィケーションする意味がない

        ((atom datum) nil);nilまで分解したのでnilを返す

        ((variablep datum);datumがアトムにまで分解されこれが束縛変数だった

         (let ((value (assoc datum binding)));datumは束縛変数になっているので探す

           (if value

               (inside-sub-p var (cdr value) binding))));束縛変数に対応するvalueを返す

        (t

         (or (inside-sub-p var (car datum) binding);datumをアトムになるまで分解しリストの残り全部と変数を照合する

             (inside-sub-p var (cdr datum) binding)))))

inside-sub-p