ユニフィケーション

ユニフィケーション（英: unification）は数理論理学や計算機科学の用語であり、充足性問題を解く際のアルゴリズム的プロセスである。ユニフィケーションは、見た目の異なる2つの項が同一または同等であることを示す置換を求めるのが目的である。ユニフィケーションは自動推論、論理プログラミング、プログラミング言語の型システムの実装などに幅広く用いられている。
なお、ユニフィケーションを単一化あるいは統一化とも呼ぶ。
主なユニフィケーションは数種類ある。等号を持たない論理（理論）において、2つの項が同一であることを示すためのユニフィケーションは統語論的ユニフィケーションと呼ばれる。空でない等号を持つ論理（理論）で2つの項の同等性を示す場合、それを意味論的ユニフィケーションと呼ぶ。置換は順序集合として順序付けられるので、ユニフィケーションは束における結びを求める手続きとして解釈できる。
ユニフィケーションを初めて形式的に研究したのはジョン・アラン・ロビンソンで、一階述語論理の導出手続きを構築する際に一階のユニフィケーションを基盤として使い、組合せ爆発の原因の1つ（項を例化したものの探索）を排除することで自動推論技術への大きな一歩とした。

置換

置換は、変数から項へのマッピングの有限集合  と定義され、1つの変数を2つの異なる項にマッピングすると曖昧さが生じるため、個々のマッピングは一意的でなければならない。項 u への置換の「適用」を  と記述し、項  に出現する各変数  を項  で置き換えることを意味する。このとき、 である。例えば、 となる。

出現検査

変数 x を x が部分として出現する関数 x=f(...,x,...) とユニフィケーションしようとする場合、x は無限個の項を持たなければならなくなる。これは有限であるとした項の定義と矛盾するため、ユニフィケーションは失敗する。そのためユニフィケーション問題を解くアルゴリズムでは、まず x がユニフィケーションしようとする項の中に出現しないかチェックする。これを出現検査などと呼ぶ。

非形式的概要

2つの項 s と t があるとき、（統語論的）ユニフィケーションは s と t を構造的に等価にする置換を求めるプロセスである。そのような置換が存在する場合、それを s と t の単一子と呼ぶ。
理論上、入力された2つの項は無数の単一子を持ちうる。しかし一般的用途では1つの最大汎用単一子を考慮すれば十分である。他の単一子は最大汎用単一子のインスタンスである。
一階のユニフィケーションは、一階の項（変数記号や関数記号で構築される項）の統語論的ユニフィケーションである。一方高階ユニフィケーションは、高階の項（何らかの高階の変数を含む項）のユニフィケーションを指す。
特定のユニフィケーションアルゴリズムの理論的属性は、入力される項の多様性に依存する。たとえば一階のユニフィケーションは決定可能であり、単一化可能な項群は必ず最大汎用単一子を持つ。しかし高階ユニフィケーションは一般に決定不能であり、最大汎用単一子を持たないことが多い。
統語論的ユニフィケーションとは別に、意味論的ユニフィケーションも広く使われている。この2つは、項を「等しい」とみなす方法が異なる。統語論的ユニフィケーションでは、置換によって項が構造的に等価になるようにする。意味論的ユニフィケーションでは、2つの項が何らかの理論において合同であるかで判定する。例えば、交換性と結合性において合同な項を「等しい」とするユニフィケーションをAC-ユニフィケーションと呼ぶ。
ユニフィケーションは計算機科学の重要なツールである。特に一階のユニフィケーションは論理プログラミング、プログラミング言語の型システム設計、自動推論などに用いられている。高階ユニフィケーションは定理証明支援で使われている。高階ユニフィケーションに制約を加えたものを実装に採用したプログラミング言語もある。意味論的ユニフィケーションは、背景理論付きSAT (SMT) を解くアルゴリズムや項書き換えアルゴリズムでよく使われている。

高階ユニフィケーション

多くの用途で、一階の項ではなく型付きラムダ項のユニフィケーションを考慮する必要がある。そのようなユニフィケーションを「高階ユニフィケーション」と呼ぶことが多い。高階ユニフィケーションで特に研究が進んでいる領域は、αβη変換により単純な型付きラムダ項の等価性を判定する問題である。そのようなユニフィケーション問題は最大汎用単一子を持たない。高階ユニフィケーションは決定不能だが、Gérard Huet は単一子空間の体系的探索を可能にする半決定可能なユニフィケーションアルゴリズム（Martelli-Montanari のユニフィケーションアルゴリズムに高階の変数を含む項についての規則を加えて一般化したもの）を示した。Huet と Gilles Dowek はこれに関する論文を書いている。
デール・ミラーは高階パターン・ユニフィケーションと呼ばれるものを提案した。この高階ユニフィケーションのサブセットは決定可能であり、これで解けるユニフィケーション問題には最大汎用単一子が存在する。λPrologやTwelfといった高階の論理プログラミング言語は、完全な高階ユニフィケーションではなくパターン・ユニフィケーションを実装しているものが多い。
計算言語学では、省略法について最も有力な理論として、省略された要素を自由変数で表し高階ユニフィケーション (HOU) を使ってその値を決定するというものがある。例えば、ジョンはメアリーが好きで、ピーターも同様であるという文を like(j; m)R(p) のように意味論表現したとき、R（省略の意味論的表現）の値は like(j; m) = R(j) という等式で決定される。このような式を解くプロセスを高階ユニフィケーションと呼ぶ。

アルゴリズム

項  についてのユニフィケーション問題  が  という潜在的等式の多重集合で表されるとき、そのアルゴリズムはそれらの式に以下に示す項書き換え規則を適用し、等価な形式である  に変形しようとする。ここで、 は一意な変数である（1つの式の左辺に一度だけ現れ、他の部分には出現しない）。この形式の多重集合は置換を表しているとみなすことができる。解がない場合、アルゴリズムは  とともに停止する。項  に含まれる変数群を  と表記し、問題  内の式の左辺と右辺の全ての項に含まれる変数の集合は  と表記する。問題  内での変数  の出現を全て項  に置換することを  と表記する。簡単にするため、定数記号は引数ゼロ個の関数記号とみなす。

停止することの証明

停止性の証明においては <NUVN,NLHS,EQN> という3タプルを考察する。NVUN は一意でない変数の数、NLHS は潜在的等式の左辺にある関数記号と定数の数、EQN は等式の数である。書き換え規則をどのような順序で適用しても、書き換えの度にNUVNは減るか、減らずに現状維持するかのどちらかなので、最終的に停止する。NUVNが現状維持した場合、NLHSが書き換えによって減るか、減らずに現状維持するかのどちらかである。NUVNとNLHSがどちらも現状維持した場合、EQNが書き換えによって減る。

構造上再帰的なユニフィケーション

コナー・マクブリッジは、Epigramのような依存型言語で「ユニフィケーションが利用している構造を表現することにより」、ジョン・アラン・ロビンソンのアルゴリズムを再帰的にすることができ、証明の複数の停止条件は不要になることを示した。