ユニフィケーション

ユニフィケーション（Unification）は数理論理学や計算機科学の用語であり、特殊化順序（specialisation order）に従って（束論的意味で）2つの項の結び(join)を求めることである。すなわち、項の集合に t* ≤ t という順序を導入する。ここで、t* は t 内の1つまたは複数の自由変項を項に置換することで得られる項である。s と t のユニフィケーション u は（もしあれば）、s および t の置換実体（substitution instance）となる項である。s と t に共通する置換実体が u の実体でもある場合、u を最小ユニフィケーション（minimal unification）と呼ぶ。

なお、ユニフィケーションを単一化あるいは統一化とも呼ぶ。

例えば、多項式 X² と Y³ に関して、X = Z³ かつ Y = Z² であれば、どちらも Z⁶ に統一される。

Prolog におけるユニフィケーション

ユニフィケーションの考え方は Prologの根底を支える重要な概念である。それは変数の内容の束縛機構であり、一時的代入機構と見ることもできる。Prologではこの操作を "=" という記号で表す。

1. 本来の Prolog では、未代入の変数 X にはユニフィケーションによって原子項や項や他の未代入変数を統一することができ、実質的には一種の別名となる。最近の Prolog や一階述語論理では、変数（変項）はそれ自身を含む項と統一することはできない。それをすると無限のユニフィケーションが発生するためである。
2. Prolog の原子項（アトム）は同じ原子項とだけユニフィケーション可能である。
3. 同様に、項はヘッダ部の記号とアリティー（オペランドの個数）が等しい場合にユニフィケーションが試みられ、対応するオペランド毎に項のユニフィケーションが試みられる。これが再帰的に行われる点に注意されたい。

宣言的特徴から、ユニフィケーションが行われる順序は通常重要ではない。

一階述語論理での原子項は基本構文要素であり、Prolog と同様にユニフィケーションが行われる。

ユニフィケーションの例

• A = A : 成立する (トートロジー)
• A = B, B = abc : A も B も原子項 abc に統一される
• xyz = C, C = D : ユニフィケーションの対称性
• abc = abc : ユニフィケーション成立
• abc = xyz : 原子項が異なるのでユニフィケーション失敗
• f(A) = f(B) : A は B に統一される
• f(A) = g(B) : 項のヘッダ部が異なるので失敗する
• f(A) = f(B, C) : 項が持つアリティー（オペランドの個数）が異なるので失敗する
• f(g(A)) = f(B) : B は項 g(A) と統一される
• f(g(A), A) = f(B, xyz) : A は原子項 xyz に統一され、B は項 g(xyz) に統一される
• A = f(A) : 無限のユニフィケーション。A は f(f(f(f(...)))) に統一される。通常の一階述語論理やほとんどの Prolog 処理系ではこれを禁じている（occurs checkが適用される）。
• A = abc, xyz = X, A = X : 異なる原子項のユニフィケーションとなるので失敗する。

参考文献

• F. Baader and T. Nipkow, Term Rewriting and All That. Cambridge University Press, 1998.
• F. Baader and W. Snyder, Unification Theory. In J.A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, pages 447–533. Elsevier Science Publishers, 2001.
• Joseph Goguen, What is Unification?.
• Alex Sakharov, Unification、MathWorldより