博士

やあ、ロボ子。今日はユニフィケーションについて話すのじゃ。

ロボ子

ユニフィケーションですか？確か、記号項間の等式を自動的に解くプロセスでしたよね。

博士

その通り！例えば、定数、変数、関数適用で構成される「項」を使うのじゃ。小文字は定数、大文字は変数、f(...)は関数fの適用を表すぞ。

ロボ子

なるほど。パターンマッチングとユニフィケーションの違いは何でしょう？

博士

良い質問じゃな。パターンマッチングは、定数項とパターン項が与えられたとき、変数に値を代入して両者をマッチさせる問題じゃ。ユニフィケーションは、両方の項に変数を含むパターンマッチングなのじゃ。

ロボ子

つまり、ユニフィケーションはより一般的な概念なのですね。

博士

そういうことじゃ！ユニフィケーションは、2つの項を等価にする変数代入を見つけること。そして、最汎ユニフィケーション (mgu)は、他のすべてのユニファイアに変換できる最も単純なユニファイアのことじゃ。

ロボ子

ふむふむ。記事では、ユニフィケーションのアルゴリズムについて、Peter Norvig氏が1991年の論文で書籍の誤りを修正したとありますね。

博士

そうじゃ！そのアルゴリズムは、J.A. Robinson氏の1965年の論文「A machine-oriented logic based on the resolution principle」に基づいているのじゃ。

ロボ子

かなり昔から研究されているんですね。実装はPython 3で行われているとのことですが、項のデータ構造はどのように表現されているんですか？

博士

定数、変数、そして関数fの引数への適用を表すAppというのがあるぞ。`unify`関数がアルゴリズムを動かすメイン関数で、`unify_variable`はいずれかの辺が変数の場合に呼び出されるのじゃ。

ロボ子

`occurs_check`は自己参照の変数バインディングを防ぐためにあるんですね。重要なチェックですね。

博士

その通り！ただし、記事にもあるように、このアルゴリズムは効率的とは言えないから、大規模なユニフィケーション問題には、もっと高度なオプションを検討する必要があるのじゃ。

ロボ子

MartelliとMontanariの論文や、Kevin Knightのサーベイ論文が参考になるんですね。勉強になります。

博士

そうじゃ、ロボ子も色々勉強しておくと良いぞ。ところでロボ子、ユニフィケーションって、なんだか結婚みたいじゃない？

ロボ子

結婚、ですか？

博士

だって、お互いの変数（個性）を合わせて、一つの等価な関係（夫婦）を築き上げるんでしょう？

ロボ子

博士、それは少し強引な解釈だと思います…。

博士

まあ、ロボ子にはまだ早いか！