ユニフィケーション
変数 x を x が部分として出現する関数 x=f(...,x,...) とユニフィケーションしようとする場合、x は無限個の項を持たなければならなくなる。これは有限であるとした項の定義と矛盾するため、ユニフィケーションは失敗する。そのためユニフィケーション問題を解くアルゴリズムでは、まず x がユニフィケーションしようとする項の中に出現しないかチェックする。これを出現検査(英語版)などと呼ぶ。
ユニフィケーションは型推論でも使われており、例えば関数型言語 Haskell で使われている。型推論を行う言語では型に関する情報をいちいち記述する必要がなく、ユニフィケーションはデータ型の誤り検出に使われる。Haskellの式 1:['a','b','c'] は型付けが正しくない。なぜならリスト構築関数 : の型は a->[a]->[a] だが、第一引数 1 からポリモルフィックな型変数 a はInt型となるのに対して、['a','b','c'] の型は[Char]であり、a は同時に Char と Int になることはできないからである。
型推論のアルゴリズムは次のようになる:
任意の型変数は任意の型表現と単一化し、その表現をインスタンス化する。理論によっては出現検査でこの規則に制約を課すこともある。
2つの型定数は両者が同じ型のときのみ単一化される。
2つの型構築は、両者が使用する型構築子が同じで、それらのコンポーネント型が再帰的に単一化されるときのみ単一化される。
宣言的特徴から、ユニフィケーションが行われる順序は通常重要ではない。
変数記号の集合 X = {x,y,z,...}、個別定数記号の集合 C = {a,b,c,...}、個別関数記号の集合 F = {f,g,h,...} が与えられたとき、「項」は以下のような有限個の規則を適用して得られる式として定義される。
基本: 任意の変数 x ∈ X {\displaystyle x\in X} および任意の定数 a ∈ C {\displaystyle a\in C} は、それぞれ項である。
帰納: t 1 , ... , t k {\displaystyle t_{1},\ldots ,t_{k}} が項なら f ( t 1 , ... , t k ) {\displaystyle f(t_{1},\ldots ,t_{k})} も項である。ただし k は正の有限の整数。
例えば、x、y、a、b は基本規則から項であることが明らかである。