ユニフィケーション（）は数理論理学や計算機科学の用語であり、問題を解く際のアルゴリズム的プロセスである。ユニフィケーションは、見た目の異なる2つのが同一または同等であることを示すを求めるのが目的である。ユニフィケーションは自動推論、論理プログラミング、プログラミング言語の型システムの実装などに幅広く用いられている。なお、ユニフィケーションを単一化あるいは統一化とも呼ぶ。主なユニフィケーションは数種類ある。等号を持たない論理（理論）において、2つの項が同一であることを示すためのユニフィケーションは統語論的ユニフィケーションと呼ばれる。空でない等号を持つ論理（理論）で2つの項の同等性を示す場合、それを意味論的ユニフィケーションと呼ぶ。置換は順序集合として順序付けられるので、ユニフィケーションは束におけるを求める手続きとして解釈できる。ユニフィケーションを初めて形式的に研究したのはで、一階述語論理の導出手続きを構築する際に一階のユニフィケーションを基盤として使い、組合せ爆発の原因の1つ（項を例化したものの探索）を排除することで自動推論技術への大きな一歩とした。変数記号の集合 X = {x,y,z...}、個別定数記号の集合 C = {a,b,c...}、個別関数記号の集合 F = {f,g,h...} が与えられたとき、「項」は以下のような有限個の規則を適用して得られる式として定義される。例えば、x、y、a、b は基本規則から項であることが明らかである。f(a,x) や g(b,y,x) は基本規則で項とされたものに帰納規則を一回適用することで得られる。f(a,f(a,x)) は帰納規則を2回適用することで得られる。このように様々な項が生成できる。簡単にするため、定数記号は引数（アリティ）がゼロ個の関数記号とみなすことが多く、帰納規則でゼロ引数の項も許容されるようにする。その場合、a() は a と統語論的に同等である。証明を行う目的では、基本規則と帰納規則を明確に区別するため、定数（ゼロアリティ関数）とアリティがゼロより大きい関数記号とを区別する。数学では関数記号ごとに引数の個数（アリティ）を固定することが多いが、統語論的ユニフィケーション問題では一般に関数記号は（有限の）任意個の引数を持ち、同じ関数記号であっても文脈によって異なる個数の引数をとりうる。例えば、f(f(a),f(x,y,z)) はユニフィケーション問題においては正しい項である。置換は、変数から項へのマッピングの有限集合 formula_5 と定義され、1つの変数を2つの異なる項にマッピングすると曖昧さが生じるため、個々のマッピングは一意的でなければならない。項 u への置換の「適用」を formula_6 と記述し、項 formula_7 に出現する各変数 formula_8 を項 formula_9 で置き換えることを意味する。このとき、formula_10 である。例えば、formula_11 となる。一階の項における統語論的ユニフィケーション問題は、同等である可能性のある有限個の式の連言 formula_12 で表される。この問題を解くには、それぞれの潜在的等式の左辺と右辺が統語論的に等価となるような置換 formula_13 を求める必要があり、formula_14 となるようにしなければならない。そのような置換 formula_13 を「単一子」（ユニフィケーション作用素）と呼ぶ。ユニフィケーション問題には解がない場合もある。例えば、formula_16 の単一子は formula_17 である。この場合、となる。変数 "x" を "x" が部分として出現する関数 "x=f(...,x...)" とユニフィケーションしようとする場合、"x" は無限個の項を持たなければならなくなる。これは有限であるとした項の定義と矛盾するため、ユニフィケーションは失敗する。そのためユニフィケーション問題を解くアルゴリズムでは、まず "x" がユニフィケーションしようとする項の中に出現しないかチェックする。これをなどと呼ぶ。2つの項 s と t があるとき、（統語論的）ユニフィケーションは s と t を構造的に等価にする置換を求めるプロセスである。そのような置換が存在する場合、それを s と t の単一子と呼ぶ。理論上、入力された2つの項は無数の単一子を持ちうる。しかし一般的用途では1つの最大汎用単一子を考慮すれば十分である。他の単一子は最大汎用単一子のインスタンスである。一階のユニフィケーションは、一階の項（変数記号や関数記号で構築される項）の統語論的ユニフィケーションである。一方高階ユニフィケーションは、高階の項（何らかの高階の変数を含む項）のユニフィケーションを指す。特定のユニフィケーションアルゴリズムの理論的属性は、入力される項の多様性に依存する。たとえば一階のユニフィケーションは決定可能であり、単一化可能な項群は必ず最大汎用単一子を持つ。しかし高階ユニフィケーションは一般に決定不能であり、最大汎用単一子を持たないことが多い。統語論的ユニフィケーションとは別に、意味論的ユニフィケーションも広く使われている。この2つは、項を「等しい」とみなす方法が異なる。統語論的ユニフィケーションでは、置換によって項が構造的に等価になるようにする。意味論的ユニフィケーションでは、2つの項が何らかの理論において合同であるかで判定する。例えば、交換性と結合性において合同な項を「等しい」とするユニフィケーションをAC-ユニフィケーションと呼ぶ。ユニフィケーションは計算機科学の重要なツールである。特に一階のユニフィケーションは論理プログラミング、プログラミング言語の型システム設計、自動推論などに用いられている。高階ユニフィケーションは定理証明支援で使われている。高階ユニフィケーションに制約を加えたものを実装に採用したプログラミング言語もある。意味論的ユニフィケーションは、背景理論付きSAT (SMT) を解くアルゴリズムや項書き換えアルゴリズムでよく使われている。p と q が一階述語論理の文とする。subst(U,p) は置換 U を文 p に適用した結果を意味する。したがって U は p と q にとっての単一子である。p と q のユニフィケーションは両者に U を適用した結果である。例えば L = {p,q} のような文の集合 L があるとする。L についての全単一子を U' としたとき、L に U を適用したものにある置換 s を適用した結果が L に U' を適用した結果と同じなら、単一子 U は L の最大汎用単一子と呼ばれる。単一化(ユニフィケーション)の考え方は に代表される論理プログラミングの根底を支える重要な概念である。それは変数の内容の束縛であり、項の構成要素の全体の形式から細部までその同一性を検査する機構である。他のプログラム言語とは異なり、 では = という記号はこの意味を表す。 は、質問としての副目標と、これによって呼び出される述語定義の頭部の単一化が試みられ、頭部の単一化の成功した節のみ選択され、その本体が次の質問になる導出と呼ばれるダイナミックで再帰的な機構によって実行される。一般に型推論アルゴリズムは上記単一化に基づいている。(注1) 最近の や一階述語論理では、変数（変項）はそれ自身を含む項と単一化することはできない。それをすると無限の単一化が発生するためである。ユニフィケーションは型推論でも使われており、例えば関数型言語 で使われている。型推論を行う言語では型に関する情報をいちいち記述する必要がなく、ユニフィケーションはデータ型の誤り検出に使われる。Haskellの式 1:['a','b','c'] は型付けが正しくない。なぜならリスト構築関数 codice_1 の型は codice_2 だが、第一引数 codice_3 からポリモルフィックな型変数 codice_4 はInt型となるのに対して、codice_5 の型はcodice_6であり、codice_4 は同時に codice_8 と codice_9 になることはできないからである。型推論のアルゴリズムは次のようになる:宣言的特徴から、ユニフィケーションが行われる順序は通常重要ではない。多くの用途で、一階の項ではなく型付きラムダ項のユニフィケーションを考慮する必要がある。そのようなユニフィケーションを「高階ユニフィケーション」と呼ぶことが多い。高階ユニフィケーションで特に研究が進んでいる領域は、αβη変換により単純な型付きラムダ項の等価性を判定する問題である。そのようなユニフィケーション問題は最大汎用単一子を持たない。高階ユニフィケーションは決定不能だが、 は単一子空間の体系的探索を可能にする半決定可能なユニフィケーションアルゴリズム（Martelli-Montanari のユニフィケーションアルゴリズムに高階の変数を含む項についての規則を加えて一般化したもの）を示した。Huet と Gilles Dowek はこれに関する論文を書いている。デール・ミラーは高階パターン・ユニフィケーションと呼ばれるものを提案した。この高階ユニフィケーションのサブセットは決定可能であり、これで解けるユニフィケーション問題には最大汎用単一子が存在する。やといった高階の論理プログラミング言語は、完全な高階ユニフィケーションではなくパターン・ユニフィケーションを実装しているものが多い。計算言語学では、省略法について最も有力な理論として、省略された要素を自由変数で表し高階ユニフィケーション (HOU) を使ってその値を決定するというものがある。例えば、ジョンはメアリーが好きで、ピーターも同様であるという文を like(j; m)R(p) のように意味論表現したとき、R（省略の意味論的表現）の値は like(j; m) = R(j) という等式で決定される。このような式を解くプロセスを高階ユニフィケーションと呼ぶ。 では、大文字で始まるシンボルは変数名、小文字で始まるシンボルは関数名を表し、カンマは論理積として使われる。数学の慣習では小文字だけを使い、アルファベットの最後の方（たとえば codice_10）は変数名、codice_11 といった文字は関数記号、codice_12 といった文字は定数を意味し、定数は引数を持たない関数とみなされる。論理積は codice_13 または formula_20 で表される。項 formula_21 についてのユニフィケーション問題 formula_22 が formula_23 という潜在的等式の多重集合で表されるとき、そのアルゴリズムはそれらの式に以下に示す項書き換え規則を適用し、等価な形式である formula_24 に変形しようとする。ここで、formula_25 は一意な変数である（1つの式の左辺に一度だけ現れ、他の部分には出現しない）。この形式の多重集合は置換を表しているとみなすことができる。解がない場合、アルゴリズムは formula_26 とともに停止する。項 formula_27 に含まれる変数群を formula_28 と表記し、問題 formula_22 内の式の左辺と右辺の全ての項に含まれる変数の集合は formula_30 と表記する。問題 formula_22 内での変数 formula_32 の出現を全て項 formula_27 に置換することを formula_34 と表記する。簡単にするため、定数記号は引数ゼロ個の関数記号とみなす。formula_35formula_36formula_37formula_38formula_39formula_40停止性の証明においては という3タプルを考察する。NVUN は一意でない変数の数、NLHS は潜在的等式の左辺にある関数記号と定数の数、EQN は等式の数である。書き換え規則をどのような順序で適用しても、書き換えの度にNUVNは減るか、減らずに現状維持するかのどちらかなので、最終的に停止する。NUVNが現状維持した場合、NLHSが書き換えによって減るか、減らずに現状維持するかのどちらかである。NUVNとNLHSがどちらも現状維持した場合、EQNが書き換えによって減る。は、のような言語で「ユニフィケーションが利用している構造を表現することにより」、ジョン・アラン・ロビンソンのアルゴリズムを再帰的にすることができ、証明の複数の停止条件は不要になることを示した。

出典:wikipedia