Lisp / Scheme はリスト処理が得意なプログラミング言語ですが、もうひとつの得意分野に「記号処理」があります。今回は記号処理の例題として Lisp / Scheme の教科書では定番となっている「記号のパターンマッチング」というプログラムを説明します。
パターンマッチング (pattern matching) は「型合わせ」という検索方法のひとつです。たとえば、「太郎はコーヒーが好き」、「太郎はココアが好き」、「花子は紅茶が好き」というデータを、次のようなリストで表すことにします。
(taro like coffee) (taro like cocoa) (hanako like tea)
パターンマッチングは、このようなデータから情報を抽出するために使われます。データと同様にパターンもリストで表すのですが、リストの中に「パターン変数 (pattern variable)」を使うことができるのが特徴です。パターン変数はいろいろな表現方法があるのですが、ここでは ? で始まるシンボル [*1] と定義します。パターン変数を含む例を次に示します。
(taro like ?x) (taro ?y coffee) (hanako ?x ?y) (hanako ?z ?z)
パターン中にパターン変数を含まない場合は述語 equal によるリストの比較と同じ動作になります。したがって、(taro like coffee) というパターンはデータ (taro like coffee) と一致しますが、データ (taro like cocoa) とは一致しません。
パターン中にパターン変数を含んでいる場合、パターン中で最初に出現するパターン変数はワイルドカードのように働きます。たとえば、(taro like ?x) というパターンと (taro like coffee) というデータをマッチングさせてみましょう。この場合、各要素を比較していくと、taro と like は一致しますが、最後の要素 ?x と coffee が残ります。
(taro like coffee)
↑ ↑ ↑
○ ○ ○
↓ ↓ ↓
(taro like ?x) ?x = coffee
図 : パターン変数の動作 (その１)
?x はパターン変数ですが、このパターンの中で最初に現れたので、?x と coffee は一致するのです。したがって、(taro like ?x) と (taro likecoffee) は一致します。同様に、(taro like ?x) と (taro like cocoa) も一致します。
(taro like coffee)
↑ ↑ ↑
○ ○ ○
↓ ↓ ↓
(taro ?y coffee) ?y = like
(taro like coffee)
↑ ↑ ↑
○ ○ ×
↓ ↓ ↓
(taro ?y cocoa)
?y = like だが最後で不一致となる
図 : パターン変数の動作 (その２)
パターン変数はパターン中のどこに現れてもかまいません。(taro ?y coffee) と (taro like coffee) は ?y が like と一致するので、マッチングは成功します。(taro like cocoa) とマッチングさせると、?y は like と一致するのですが、coffee と cocoa は一致しないので失敗します。
(hanako like tea)
↑ ↑ ↑
○ ○ ○
↓ ↓ ↓
(taro ?x ?y) ?x = like, ?y = tea
図 : パターン変数の動作 (その３)
また、パターン変数は複数使ってもかまいません。(hanako ?x ?y) はパターン変数 ?x と ?y がありますね。これと (hanako like tea) をマッチングさせてみます。すると、?x は like と、?y は tea と一致するので、マッチングは成功します。
(hanako like tea)
↑ ↑ ↑
○ ○ ×
↓ ↓ ↓
(taro ?x ?x)
?x = like だか tea と ?x の値 like は一致しない
図 : パターン変数の動作 (その４)
今度は、(hanako ?x ?x) を考えてみます。同じパターン変数 ?x が 2 回使われていますね。データと一致したパターン変数は、その後パターンの中では一致したデータとして扱われます。(hanako like tea) とマッチングさせると、最初の ?x は like と一致します。2 番目の ?x は tea と比較することになりますが、?x は既に like と一致しているので like と tea を比較することになるのです。したがって、マッチングは失敗します。
(hanako ?x ?x) は (hanako like like) とか (hanako tea tea) のようなデータと一致しますが、この場合はデータに意味がありませんね。
関数型言語の用語では、変数に値を与えることを「束縛 (binding)」といいます。また、値が与えられていない、未束縛の変数を「自由変数」と呼びます。パターン変数の場合、最初は自由変数であり、データとマッチングしたときに束縛されます。つまり、自由変数であればどんなデータとも一致しますが、束縛されていれば、その値を取り出してデータと比較することになります。パターンマッチングを実現する場合、この変数束縛の管理方法がポイントになります。
今回はオーソドックスに連想リストを使ってパターンマッチングを実現してみましょう。関数名は match とします。match は再帰を使ってリストを分解し、要素同士を比較していきます。match はマッチングに成功した場合、パターン変数とその値を格納する連想リストを返します。本稿では、この連想リストのことを「束縛リスト」と呼ぶことにします。次の例を見てください。
(match '(taro like ?x) '(taro like coffee) '()) => ((?X . COFFEE)) (match '(taro ?y coffee) '(taro like coffee) '()) => ((?Y . LIKE)) (match '(hanako ?x ?y) '(hanako like tea) '()) => ((?Y . TEA) (?X . LIKE))
関数 match は 1 番目の引数にパターンを、2 番目の引数にデータを、3 番目の引数に束縛リストを受け取ります。データにはパターン変数が含まれていないことに注意してください。
最初はどのパターン変数にも値は入っていないので、引数には空リストを渡します。match はパターン変数がなくても、マッチングが成功したときは空リストを返します。
(match '(taro like coffee) '(taro like coffee) '()) => NIL (match '(hanako like tea) '(hanako like tea) '()) => NIL
マッチングが失敗した場合はシンボル FAIL を返すことにします。
(match '(taro ?y coffee) '(taro like cocoa) '()) => FAIL (match '(hanako ?x ?x) '(hanako like tea) '()) => FAIL
match を作る前に、パターン変数を管理するための関数を作っておきましょう。まず、要素がパターン変数であるかチェックする述語 variablep です。
リスト : 要素はパターン変数か
(defun variablep (pattern)
(and (symbolp pattern)
(char= #\? (char (string pattern) 0))))
最初に、述語 symbolp で pattern がシンボルであることを確認します。次に、関数 string でシンボルを文字列に変換して、関数 char で先頭文字を取り出します。そして、述語 char= で文字が #\? であることをチェックします。
次は、束縛リストにデータを追加する add-binding を作ります。
リスト : 束縛リストに追加する (defun add-binding (var value binding) (cons (cons var value) binding))
これも簡単ですね。引数 var に変数名、value に値、binding に束縛リストを受け取ります。まず cons で var と value をドット対にまとめ、それを cons で binding の先頭に追加します。返り値はパターン変数を追加した束縛リストになります。
それでは match を作ります。リスト操作の基本である car と cdr でリストを分解して要素を比較していきます。ここで肩慣らしに、リストが等しいかチェックする述語 equal-list を作ってみましょう。簡単のため、アトムの判定は述語 eql を使うことにします。再帰定義に慣れていればすぐに作れると思います。
考え方は簡単です。2 つの引数がアトムであれば eql で比較すればいいですね。リスト同士であればリストの car を比較します。このとき、リストの要素がリストの場合もあるので、eql で比較することはできません。ここは再帰の出番ですね。equal-list を呼び出して比較すればいいわけです。
その結果が等しい場合はリストの cdr を比較します。ここでも equal-list を呼び出します。2 つの引数がアトムでもなくリストでもない場合は、不一致と判定すればいいでしょう。プログラムは次のようになります。
リスト : リストが等しいか
(defun equal-list (xs ys)
(cond
((and (atom xs) (atom ys))
(eql xs ys))
((and (consp xs) (consp ys))
(when (equal-list (car xs) (car ys))
(equal-list (cdr xs) (cdr ys))))
(t nil)))
述語 atom でアトムのチェック、述語 consp でリストのチェックを行います。述語 listp は NIL でも真と判定するため、ここでは consp を使っています。引数 XS と YS がリストの場合、リストの先頭要素を car で取り出して equal-list を再帰呼び出しします。その結果が真であれば、残りのリストを equal-list でチェックします。
match の場合も基本的な考え方は equal-list と同じです。ここにパターン変数の処理を付け加えればいいわけです。パターン変数とのマッチングは関数 match-variable で行い、リストの比較は関数 match-pieces で行うことにすると、プログラムは次のようになります。
リスト : パターンマッチング
(defun match (pattern datum binding)
(cond
((variablep pattern)
(match-variable pattern datum binding))
((and (atom pattern) (atom datum))
(match-atoms pattern datum binding))
((and (consp pattern) (consp datum))
(match-pieces pattern datum binding))
(t 'fail)))
パターン変数はシンボルなので atom で判定すると真になってしまいます。このため、最初に variablep で引数 PATTERN がパターン変数かチェックしています。
PATTERN と DATUM がアトムであれば、関数 match-atoms で比較します。PATTERN と DATUM がリストであれば、match-pieces でチェックを行います。ここで match が再帰呼び出しされます。それ以外の場合は FAIL を返します。
まず簡単な match-atoms から見ていきましょう。
リスト : アトム同士のマッチング (defun match-atoms (pattern datum binding) (if (equal pattern datum) binding 'fail))
PATTERN と DATUM を述語 equal で比較します。等しい場合は連想リスト BINDING を返し、そうでなければ FAIL を返します。
次は、パターン変数とのマッチングを調べる match-variable です。
リスト : パターン変数とのマッチング
(defun match-variable (var datum binding)
(let ((value (assoc var binding)))
(if value
;; 値を使ってもう一度チェック
(match (cdr value) datum binding)
;; 変数束縛に追加する
(add-binding var datum binding))))
最初に、引数 BINDING からパターン変数 VAR を assoc で検索します。assoc は VAR を発見したらドット対を返すので、それを VALUE にセットします。パターン変数が見つかれば、その値を使って再度マッチングを試みます。これは match を再帰呼び出しすればいいですね。値は (cdr val) で取り出すことができます。
パターン変数が BINDING に無い場合は、そのパターン変数はまだ束縛されていません。そこで、add-binding を呼び出して BINDING にパターン変数と値を登録します。
次はリストのマッチングを行う match-pieces です。
リスト : リストのマッチング
(defun match-pieces (pattern datum binding)
(let ((result (match (car pattern) (car datum) binding)))
(if (eq result 'fail)
'fail
(match (cdr pattern) (cdr datum) result))))
リストを car と cdr で分解してマッチングしていきます。まず PATTERN と DATUM の要素を car で取り出して、match を再帰呼び出しします。結果は RESULT にセットします。マッチングに失敗したら FAIL を返します。
マッチングに成功したら、残りのリストを match で調べます。このとき、束縛リストは BINDING ではなく RESULT を使うことがポイントです。最初に呼び出した match により、新しいパターン変数が追加されているかもしれないからです。
これでプログラムは完成です。簡単な実行例を示します。
* (match '(taro like coffee) '(taro like coffee) '()) NIL * (match '(taro like tea) '(taro like coffee) '()) FAIL * (match '(taro like ?x) '(taro like coffee) '()) ((?X . COFFEE)) * (match '(taro ?x ?y) '(taro like coffee) '()) ((?Y . COFFEE) (?X . LIKE)) * (match '(taro ?x ?x) '(taro like coffee) '()) FAIL
実際にプログラムを動かして、いろいろ試してみてくださいね。
次はパターンとパターンを照合する「ユニフィケーション (unification)」 [*2] を作ってみましょう。関数名は unify とします。unify はパターン変数とパターン変数を照合する分だけ match よりも処理は複雑になります。次の実行例を見てください。
(unify '(taro like coffee) '(taro like ?x) '()) => ((?X . COFFEE)) (unify '(taro like coffee) '(taro ?y coffee) '()) => ((?Y . LIKE)) (unify '(hanako like tea) '(hanako ?x ?y) '()) => ((?Y . TEA) (?X . LIKE))
match では第 2 引数にパターンを与えることはできませんが、unify はパターンでもかまいません。unify は match と同様に、成功した場合は束縛リストを返し、失敗した場合は FAIL を返します。
次は、ユニフィケーションの特徴的な例を示しましょう。
(unify '(hanako ?x ?y) '(hanako ?a ?b) '()) => ((?Y . ?B) (?X . ?A)) (unify '(hanako ?x ?y) '(hanako ?x ?y) '()) => ((?Y . ?Y) (?X . ?X))
ユニフィケーションでは、パターン変数の値がパターン変数になることもあります。最後の例のように、自分自身が値となる場合もあります。このような場合でもユニフィケーションは成功するのです。
それでは unify を作っていきましょう。処理は match とほぼ同じですが、第 2 引数にもパターン変数が含まれるため、その処理を追加することになります。
リスト : ユニフィケーション
(defun unify (pattern datum binding)
(cond
((variablep pattern)
(unify-variable pattern datum binding))
((variablep datum)
(unify-variable datum pattern binding))
((and (atom pattern) (atom datum))
(unify-atoms pattern datum binding))
((and (consp pattern) (consp datum))
(unify-pieces pattern datum binding))
(t 'fail)))
引数 DATUM がパターン変数かチェックする処理を追加しています。関数 unify-atoms と unify-pieces は match を unify に置き換えただけで、match-atoms と match-pieces と同じです。
リスト : アトムとリストのユニフィケーション
;;; アトムとのユニフィケーション
(defun unify-atoms (pattern datum binding)
(if (equal pattern datum) binding 'fail))
;;; リストのユニフィケーション
(defun unify-pieces (pattern datum binding)
(let ((result (unify (car pattern) (car datum) binding)))
(if (eq result 'fail)
'fail
(unify (cdr pattern) (cdr datum) result))))
次は、パターン変数とのユニフィケーションを行う unify-variable を作ります。unify-variable は match-variable と処理が異なる箇所があります。ユニフィケーションの場合、パターン変数とパターン変数は一致しますが、パターン変数とそれと同じパターン変数を含むパターンとは一致しないからです。次の例を見てください。
(unify '(taro like ?x) '(taro like (coffee black)) '()) => ((?X COFFEE BLACK)) (unify '(taro like (coffee ?x)) '(taro like (coffee black)) '()) => ((?X . BLACK)) (unify '(taro like ?x) '(taro like (coffee ?x)) '()) => FAIL
COFFEE の種類をリストで表すことにしました。最初の例では、?X は (COFFEE BLACK) となります。2 番目の例では、?X は BLACK となり、COFFEE の種類を求めることができます。
それでは、最後の例はどうなるのでしょうか。?X と (COFFEE ?X) を照合させることになります。この場合、最初の ?X は TARO が LIKE なものを表しているのに、次の ?X は COFFEE の種類を表すことになり矛盾してしまいます。したがって、?X と (COFFEE ?X) は不一致と判定しなくてはいけないのです。
それでは unify-variable を作りましょう。パターン変数と値を束縛リストに追加するときに、値の中に同じパターン変数がないことを確認します。この処理を関数 insidep で行います。
リスト : パターン変数とのユニフィケーション
(defun unify-variable (pattern datum binding)
(let ((value (assoc pattern binding)))
(if (and value
(not (eq pattern (cdr value))))
(unify (cdr value) datum binding)
(if (insidep pattern datum binding)
'fail
(add-binding pattern datum binding)))))
実は、match-varibale との違いがもうひとつあります。ユニフィケーションの場合、同じパターン変数同士の照合は成功するので、束縛リストの中には、たとえば (?X . ?X) というドット対が含まれることがあります。このため、束縛リストから変数の値を探し、それを使って単純に unify を再帰呼び出しすると困ることが起こるのです。
?X の値は ?X ですから、同じことをずっと繰り返すことになり、再帰呼び出しが停止しないのです。これを回避するために、最初の if でパターン変数とその値が異なることを確認しています。
そして、束縛リストにパターン変数と値を追加する前に関数 insidep を呼び出して、同じパターン変数が値の中で使われていないかチェックします。それでは insidep を作りましょう。
リスト : 同じパターン変数が含まれているか
(defun insidep (var datum binding)
(unless (eq var datum)
(inside-sub-p var datum binding)))
insidep は引数 datum (パターン変数の値) に引数 var (パターン変数) が含まれていれば T を返し、そうでなければ NIL を返します。実際の処理は関数 inside-sub-p で行います。ユニフィケーションは同じパターン変数の照合であれば成功するので、var と datum が同じパターン変数であれば NIL を返します。
リスト : insidep 本体
(defun inside-sub-p (var datum binding)
(cond
((eq var datum) t)
((atom datum) nil)
((variablep datum)
(let ((value (assoc datum binding)))
(when value
(inside-sub-p var (cdr value) binding))))
(t
(or (inside-sub-p var (car datum) binding)
(inside-sub-p var (cdr datum) binding)))))
inside-sub-p はリストを car と cdr で分解しながら、パターン変数 VAR が含まれているかチェックします。最初に VAR と DATUM が等しいか eq でチェックします。結果が真であればデータの中に同じパターン変数を見つけたので T を返します。
次に、DATUM がアトムであれば、これ以上分解できないので NIL を返します。DATUM がパターン変数の場合は、その値に VAR が含まれているかチェックします。assoc で束縛リストから DATUM を探索し、値が見つかれば inside-sub-p を再帰呼び出しします。そうでなければ NIL を返します。
それ以外の場合は DATUM はリストなので、car と cdr でリストを分解して inside-sub-p を再帰呼び出しします。変数 VAR が見つかったら探索を中断して T を返せばいいので、or を使っていることに注意してください。つまり、CAR 部を調べてた結果が T ならば or は T を返しますし、NIL であれば次の CDR 部の探索が行われます。
これでプログラムは完成です。簡単な実行例を示します。
* (unify '(taro like coffee) '(taro like coffee) '()) NIL * (unify '(taro like coffee) '(taro like ?x) '()) ((?X . COFFEE)) * (unify '(taro like coffee) '(taro ?y coffee) '()) ((?Y . LIKE)) * (unify '(taro like coffee) '(taro ?y x) '()) FAIL * (unify '(taro like coffee) '(taro ?y ?x) '()) ((?X . COFFEE) (?Y . LIKE)) * (unify '(hanako ?x ?y) '(hanako a b) '()) ((?Y . B) (?X . A)) * (unify '(hanako ?x ?y) '(hanako ?a ?b) '()) ((?Y . ?B) (?X . ?A)) * (unify '(hanako ?x ?y) '(hanako ?x ?y) '()) ((?Y . ?Y) (?X . ?X)) * (unify '(taro like ?x) '(tario like (coffee black)) '()) FAIL * (unify '(taro like ?x) '(taro like (coffee black)) '()) ((?X COFFEE BLACK)) * (unify '(taro like (coffee ?x)) '(taro like (coffee black)) '()) ((?X . BLACK)) * (unify '(taro like ?x) '(taro like (coffee ?x)) '()) FAIL
実際にプログラムを動かして、いろいろ試してみてくださいね。
関数型言語のパターンマッチング、とくに Erlang でのリストのマッチングは Prolog とよく似ています。そうはいっても、パターンマッチングと Prolog の「ユニフィケーション (unification)」は異なります。Erlang のパターンマッチングは右辺式に未束縛変数 (自由変数) があるとエラーになりますが、Prolog のユニフィケーションは右辺式に自由変数があってもかまいません。Prolog の場合、自由変数同士のマッチングは成功しますし、右辺式 (たとえばリストなど) の中に自由変数が含まれていてもかまいません。
Prolog のユニフィケーションは本稿で作成した unify の動作と少し異なります。unify の場合も自由変数同士の照合は成功します。ところが、自由変数とリストを照合する場合、リストの中に同じ自由変数が含まれていると照合は失敗します。簡単な例を示しましょう。
(unify '?x '(a . ?y) '()) => ((?X A . ?Y)) (unify '?x '(a . ?x) '()) => FAIL
最初の例は ?X と (A . ?Y) を照合します。リストの中には同じ変数 ?X がないので照合は成功します。次の例はリストの中に同じ自由変数 ?X があるので照合は失敗します。Prolog ではどちらの場合も照合に成功します。SWI-Prolog での実行例を示します。
?- X = [a | Y]. X = [a|Y] ; No ?- X = [a | X]. X = [a, a, a, a, a, a, a, a, a|...] ; No
結果を見ればおわかりのように、X = [a | X] は「循環リスト」になります。右辺のリストにある X は自由変数ですが、Prolog はこのようなリストでも扱うことができます。また、右辺と左辺で同じ自由変数 X がありますが、このようなユニフィケーションでも Prolog では実行することができます。X は自由変数なので、X の値はリスト (セルの先頭アドレス) になります。セルの終端は X なので、先頭のセルとつながって循環リストになるわけです。
unify でも Prolog のようなユニフィケーションを行わせることは可能です。次のリストを見てください。
リスト : パターン変数とのユニフィケーション
(defun unify-variable (pattern datum binding)
(let ((value (assoc pattern binding)))
(if (and value
(not (eq pattern (cdr value))))
(unify (cdr value) datum binding)
(if (insidep pattern datum binding)
'fail
(add-binding pattern datum binding)))))
関数 unify-variable で PATTERN が自由変数のとき、それが DATUM の中に含まれているか insidep でチェックしています。このチェックを外せば unify でも循環リストを作ることができます。
それでは実際に試してみましょう。
* (unify '?x '(a . ?x) '()) ((?X A . ?X)) * (unify '?x '(a . ?x) '()) => 無限ループ
確かに ?X と (A . ?X) の照合には成功しますが、そのあとに ?X と ?X を照合すると無限ループに陥ります。このとき、関数の呼び出しは次のようになります。
1. (unify '?x '?x '((?x a . ?x))) 2. (unify-variable '?x '?x '((?x a . ?x))) 3. (unify '(a . ?x) ?x '((?x a . ?x))) 4. (unify-variable '?x '(a , ?x) '((?x a . ?x))) 5. (unify '(a . ?x) '(a . ?x) '((?x a . ?x))) 6. a の照合に成功したあと 1 に戻る
このように循環的なデータがあると正常に動作しないのです。そこで、循環データをチェックする処理を追加します。次のリストを見てください。
リスト : パターン変数とのユニフィケーション (2)
(defun unify-variable (pattern datum binding)
(let ((val (assoc pattern binding)))
(cond
((and val (eq datum (cdr val)))
;; pattern の値と datum が等しい (循環データ)
binding)
((and val
(not (eq pattern (cdr val))))
(unify (cdr val) datum binding))
(t
(add-binding pattern datum binding)))))
束縛リスト binding から求めた値 VAL が DATUM と eq で等しい場合、PATTERN は束縛されていて、かつデータが循環していることがわかります。BINDING をそのまま返します。これで循環データにも対応することができます。
それでは実行してみましょう。
* (setq *print-circle* t) T * (unify '(?x ?x) '((a . ?x) ?x) '()) ((?X A . ?X)) * (unify '(?x ?x) '((a . ?x) (?a . ?z)) '()) ((?Z . #1=(A . ?X)) (?A . A) (?X . #1#)) * (unify '(?x ?x) '((a . ?x) (?a ?b . ?z)) '()) ((?Z . #1=(A . ?X)) (?B . A) (?A . A) (?X . #1#)) * (unify '(?x ?x) '((a . ?x) (?a ?b ?c . ?z)) '()) ((?Z . #1=(A . ?X)) (?C . A) (?B . A) (?A . A) (?X . #1#)) * (unify '(?x ?x) '((a . ?x) (?a ?b ?c ?d . ?z)) '()) ((?Z . #1=(A . ?X)) (?D . A) (?C . A) (?B . A) (?A . A) (?X . #1#))
?X と (A . ?X) を照合したあと、?X の値は確かに循環リストとして機能しています。このように、unify でも Prolog のようなユニフィケーションを行わせることができます。
;;;
;;; match.lisp : 記号のパターンマッチング
;;;
;;; Copyright (C) 2003-2020 Makoto Hiroi
;;;
;;; 関数宣言
(declaim (ftype (function (t t list) t) match unify))
;;; 要素はパターン変数か
(defun variablep (pattern)
(and (symbolp pattern)
(char= #\? (char (string pattern) 0))))
;;; 変数束縛に追加する
(defun add-binding (var value binding)
(cons (cons var value) binding))
;;;
;;; マッチング
;;;
;;; 変数とのマッチング
(defun match-variable (var datum binding)
(let ((value (assoc var binding)))
(if value
;; 値を使ってもう一度チェック
(match (cdr value) datum binding)
;; 変数束縛に追加する
(add-binding var datum binding))))
;;; アトム同士のマッチング
(defun match-atoms (pattern datum binding)
(if (equal pattern datum) binding 'fail))
;;; リスト同士のマッチング
(defun match-pieces (pattern datum binding)
(let ((result (match (car pattern) (car datum) binding)))
(if (eq result 'fail)
'fail
(match (cdr pattern) (cdr datum) result))))
;;; パターンマッチング : datum に変数は無し
(defun match (pattern datum binding)
(cond
((variablep pattern)
(match-variable pattern datum binding))
((and (atom pattern) (atom datum))
(match-atoms pattern datum binding))
((and (consp pattern) (consp datum))
(match-pieces pattern datum binding))
(t 'fail)))
;;;
;;; ユニフィケーション
;;;
;;; datum の中に var があるか
(defun inside-sub-p (var datum binding)
(cond
((eq var datum) t)
((atom datum) nil)
((variablep datum)
(let ((value (assoc datum binding)))
(if value
(inside-sub-p var (cdr value) binding))))
(t
(or (inside-sub-p var (car datum) binding)
(inside-sub-p var (cdr datum) binding)))))
(defun insidep (var datum binding)
(unless (eq var datum)
(inside-sub-p var datum binding)))
;;; アトムとのユニフィケーション
(defun unify-atoms (pattern datum binding)
(if (equal pattern datum) binding 'fail))
;;; リストのユニフィケーション
(defun unify-pieces (pattern datum binding)
(let ((result (unify (car pattern) (car datum) binding)))
(if (eq result 'fail)
'fail
(unify (cdr pattern) (cdr datum) result))))
;;; 変数とのユニフィケーション
(defun unify-variable (pattern datum binding)
(let ((value (assoc pattern binding)))
(if (and value
(not (eq pattern (cdr value))))
(unify (cdr value) datum binding)
(if (insidep pattern datum binding)
'fail
(add-binding pattern datum binding)))))
;;; ユニフィケーション
(defun unify (pattern datum binding)
(cond
((variablep pattern)
(unify-variable pattern datum binding))
((variablep datum)
(unify-variable datum pattern binding))
((and (atom pattern) (atom datum))
(unify-atoms pattern datum binding))
((and (consp pattern) (consp datum))
(unify-pieces pattern datum binding))
(t 'fail)))