統一（コンピュータサイエンス）

論理学とコンピュータサイエンス、特に自動推論において、統一とは、それぞれが左辺 = 右辺という形式の記号式間の方程式を解くアルゴリズム的なプロセスです。たとえば、x、y、z を変数として使用し、fを解釈されていない関数とすると、シングルトン方程式セット { f (1, y ) = f ( x ,2) } は、置換 { x ↦ 1, y ↦ 2 } を唯一の解とする構文上の 1 階統一問題です。

変数がとることのできる値や、同等とみなされる式については、慣例が異なります。 一次構文的統一では、変数は一次項にまたがり、同等性は構文上です。 このバージョンの統一には一意の「最良」の答えがあり、論理プログラミングやプログラミング言語型システムの実装、特にHindley–Milnerベースの型推論アルゴリズムで使用されます。 高次統一 (高次パターン統一に限定される場合もあります) では、項にラムダ式を含めることができ、同等性はベータ縮小までです。 このバージョンは、Isabelle、Twelf、lambdaPrologなどの証明支援システムや高次論理プログラミングで使用されます。 最後に、意味的統一または E 統一では、同等性は背景知識に依存し、変数はさまざまなドメインにまたがります。 このバージョンは、 SMT ソルバー、項書き換えアルゴリズム、および暗号プロトコル分析 で使用されます。

統一問題とは、解くべき方程式の有限集合E ={ l ₁ ≐ r ₁ , ..., l _n ≐ r _n }であり、 l _i、r _{i は}項または表現の集合内にあります。方程式セットまたは統一問題でどの表現または項が出現できるか、およびどの表現が等しいと見なされるかによって、統一のいくつかの枠組みが区別されます。高階変数、つまり関数を表す変数が表現で許可されている場合、このプロセスは高階統一と呼ばれ、そうでない場合は第 1 階統一と呼ばれます。各方程式の両辺を文字通り等しくするソリューションが必要な場合、このプロセスは統語的統一または自由統一と呼ばれ、そうでない場合は意味的統一または等式統一、またはE 統一、あるいは理論を法とする統一と呼ばれます。 ${\displaystyle T}$

各方程式の右辺が閉じている（自由変数がない）場合、その問題は（パターン）マッチングと呼ばれます。各方程式の左辺（変数がある）はパターンと呼ばれます。^[1]

形式的には、統一アプローチは以下を前提としている。

• 変数の無限集合。高階統一のためには、ラムダ項境界変数の集合から互いに素な を選択するのが便利です。${\displaystyle V}$${\displaystyle V}$
• となる項の集合。1 階統一の場合、は通常、 1 階項(変数と関数のシンボルから構築された項)の集合です。高階統一の場合、は 1 階項とラムダ項(いくつかの高階変数を含む項) で構成されます。${\displaystyle T}$${\displaystyle V\subseteq T}$${\displaystyle T}$${\displaystyle T}$
• に発生する自由変数の集合を各項に割り当てるマッピング。${\displaystyle {\text{vars}}\colon T\rightarrow }$ ${\displaystyle \mathbb {P} }$${\displaystyle (V)}$${\displaystyle t}$${\displaystyle {\text{vars}}(t)\subsetneq V}$${\displaystyle t}$
• に関する理論または同値関係 であり、どの項が等しいとみなされるかを示します。1 階の E 統一では、特定の関数記号についての背景知識を反映します。たとえば、が可換とみなされる場合、が の引数を一部 (場合によってはすべて) で交換することによってから生じる場合などです。 ^{[注 1]}背景知識がまったくない最も一般的なケースでは、文字通りまたは構文的に、同一の項のみが等しいとみなされます。この場合、≡ は自由理論(自由オブジェクトであるため)、空理論(等式文の集合、つまり背景知識が空であるため)、未解釈関数の理論(統一が未解釈項に対して行われるため)、またはコンストラクタの理論(すべての関数記号はデータ項を構築するだけで、それらに対して演算を行わないため) と呼ばれます。高階統一では、通常、と がアルファ同値である場合に です。${\displaystyle \equiv}$${\displaystyle T}$${\displaystyle \equiv}$${\displaystyle \oplus}$${\displaystyle t\equiv u}$${\displaystyle u}$${\displaystyle t}$${\displaystyle \oplus}$${\displaystyle t\equiv u}$${\displaystyle t}$${\displaystyle u}$

用語と理論の集合が解の集合にどのように影響するかの例として、統語論的一階統一問題 { y = cons (2, y ) } には有限用語の集合上では解がありません。しかし、無限木用語の集合上では単一の解 { y ↦ cons (2, cons (2, cons (2,...))) }があります。同様に、意味論的一階統一問題 { a ⋅ x = x ⋅ a } には、半群、つまり (⋅) が結合的であると考えられる場合、形式 { x ↦ a ⋅...⋅ a } の各置換が解として存在します。しかし、同じ問題をアーベル群で見ると(ここで (⋅) は可換でもあると考えられます) 、置換はすべて解として存在します。

高階統一の例として、シングルトン セット { a = y ( x ) } は、 y が関数変数であるため、構文上の 2 階統一の問題です。1 つの解は { x ↦ a、y ↦ (恒等関数) } です。もう 1 つの解は { y ↦ (各値をaにマッピングする定数関数)、x ↦ ( 任意の値 ) }です。

置換とは、変数から項へのマッピングです。 表記は、の各変数を項 （）に、その他のすべての変数をそれ自体にマッピングする置換を指します。 は、ペアごとに異なる必要があります。項にその置換を適用することは、接尾辞表記法でと書きます。これは、項内の各変数のすべての出現を で（同時に）置き換えることを意味します。項に置換を適用した結果は、その項のインスタンスと呼ばれます。 1次の例として、項に 置換{ x ↦ h ( a , y ), z ↦ b }を適用すると、${\displaystyle \sigma :V\rightarrow T}$${\displaystyle \{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}}$${\displaystyle x_{i}}$${\displaystyle t_{i}}$${\displaystyle i=1,...,k}$${\displaystyle x_{i}}$${\displaystyle t}$${\displaystyle t\{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}}$${\displaystyle x_{i}}$${\displaystyle t}$${\displaystyle t_{i}}$${\displaystyle t\tau}$${\displaystyle \tau}$${\displaystyle t}$${\displaystyle t}$

項に項 と等価なインスタンスがある場合、つまり、何らかの置き換え に対して である場合、 はよりも一般的なものとされ、 はよりも特別な、またはに包含されていると呼ばれます。たとえば、が可換 である場合、 であるため、は よりも一般的なものとなります。 ${\displaystyle t}$${\displaystyle u}$${\displaystyle t\sigma \equiv u}$${\displaystyle \sigma}$${\displaystyle t}$${\displaystyle u}$${\displaystyle u}$${\displaystyle t}$${\displaystyle x\oplus a}$${\displaystyle a\oplus b}$${\displaystyle (x\oplus a)\{x\mapsto b\}=b\oplus a\equiv a\oplus b}$

≡ が項の文字通りの（統語的）同一性である場合、両方の項が構文構造ではなく変数名のみ異なる場合に限り、項は他の項よりも一般的かつ特殊である可能性があります。このような項は、バリアント、または互いの名前変更と呼ばれます。たとえば、 は および であるため 、 のバリアントです 。 ただし、はのバリアント ではありません。後者の項を前者の項に変換する置換はできないためです。したがって、後者の項は前者の項よりも適切に特殊です。 ${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$${\displaystyle f(x_{2},a,g(z_{2}),y_{2})}$$${\displaystyle f(x_{1},a,g(z_{1}),y_{1})\{x_{1}\mapsto x_{2},y_{1}\mapsto y_{2},z_{1}\mapsto z_{2}\}=f(x_{2},a,g(z_{2}),y_{2})}$$$${\displaystyle f(x_{2},a,g(z_{2}),y_{2})\{x_{2}\mapsto x_{1},y_{2}\mapsto y_{1},z_{2}\mapsto z_{1}\}=f(x_{1},a,g(z_{1}),y_{1}).}$$${\displaystyle f(x_{1},a,g(z_{1}),y_{1})}$${\displaystyle f(x_{2},a,g(x_{2}),x_{2})}$

任意の に対して、項は構造的に異なる項よりも一般的かつ特殊である可能性があります。たとえば、がべき等 である場合、つまり常に である場合、項はよりも一般的です^{[注 2]}。またその逆も同様です^{[注 3]} 。ただし、 と は構造が異なります。 ${\displaystyle \equiv }$${\displaystyle x\oplus x\equiv x}$${\displaystyle x\oplus y}$${\displaystyle z}$${\displaystyle x\oplus y}$${\displaystyle z}$

置換が置換よりも特殊、つまり置換に包含されるとは、各項 に対してが に包含される場合です。また、 はよりも一般的であるとも言えます。より正式には、からの変数を含まない、空でない補助変数の無限集合を取ります。このとき、すべての項 に対して となる置換がある場合、置換は別の置換に包含されます。^[2] たとえば、 はを使用してに包含されますが、 には包含されません。また、は のインスタンスではありません 。^[3]${\displaystyle \sigma }$${\displaystyle \tau }$${\displaystyle t\sigma }$${\displaystyle t\tau }$${\displaystyle t}$${\displaystyle \tau }$${\displaystyle \sigma }$${\displaystyle V}$${\displaystyle l_{i}\doteq r_{i}}$${\displaystyle V}$${\displaystyle \sigma }$${\displaystyle \tau }$${\displaystyle \theta }$${\displaystyle X\notin V}$${\displaystyle X\sigma \equiv X\tau \theta }$${\displaystyle \{x\mapsto a,y\mapsto a\}}$${\displaystyle \tau =\{x\mapsto y\}}$${\displaystyle \theta =\{y\mapsto a\}}$${\displaystyle \sigma =\{x\mapsto a\}}$${\displaystyle \tau =\{x\mapsto y\}}$${\displaystyle f(x,y)\sigma =f(a,y)}$${\displaystyle f(x,y)\tau =f(y,y)}$

置換 σ は、l _i σ ≡ r _i σ がに対して成り立つ場合、統一問題Eの解です。このような置換は、Eの統一子とも呼ばれます。たとえば、 ⊕ が結合的である場合、統一問題 { x ⊕ a ≐ a ⊕ x } には、 { x ↦ a }、 { x ↦ a ⊕ a }、 { x ↦ a ⊕ a ⊕ a } などの解がありますが、問題 { x ⊕ a ≐ a } には解がありません。 ${\displaystyle i=1,...,n}$

与えられた統一問題Eについて、統一子の集合S は、各解の置換がS内の何らかの置換に包含される場合、完全であると呼ばれます。完全な置換集合は常に存在します (たとえば、すべての解の集合) が、一部のフレームワーク (無制限の高階統一など) では、解が存在するかどうか (つまり、完全な置換集合が空でないかどうか) を決定する問題は決定不可能です。

集合S は、そのメンバーのいずれも他のメンバーを包含しない場合に極小と呼ばれます。フレームワークに応じて、完全で極小の置換集合は、0、1、有限個、または無限個のメンバーを持つ場合があり、冗長なメンバーの無限チェーンのためにまったく存在しない場合もあります。^[4]したがって、一般に、ユニフィケーション アルゴリズムは完全な集合の有限近似を計算しますが、これは極小である場合もそうでない場合もあります。ただし、ほとんどのアルゴリズムは、可能な限り冗長なユニファイアを回避します。^[2] 1 階の構文ユニフィケーションでは、Martelli と Montanari ^[5]は、解決不可能であることを報告するか、それ自体で完全で極小の置換集合を形成する単一のユニファイアを計算するアルゴリズムを示しました。これは最も一般的なユニファイアと呼ばれます。

第一階項の統語的統一は、最も広く使われている統一フレームワークです。これは、 T が（ある与えられた変数の集合V 、定数のC 、およびn項関数記号のF _n上の）第一階項の集合であり、 ≡ が統語的等式であることに基づいています。このフレームワークでは、解ける各統一問題{ l ₁ ≐ r ₁、...、l _n ≐ r _n }には、完全で明らかに極小のシングルトン解集合{ σ }があります。そのメンバーσは、問題の最も一般的な統一子( mgu )と呼ばれます。 mgu が適用されると、各潜在的な方程式の左側と右側の項は統語的に等しくなります。つまり、l ₁ σ = r ₁ σ ∧ ... ∧ l _n σ = r _n σです。問題の任意の統一子は、mgu σに包含されます^{[注 4]}。 mgu は、変種を除いて一意です。つまり、S ₁とS _{2 が}両方とも同じ構文統一問題の完全かつ最小の解集合である場合、いくつかの置換σ ₁およびσ _{2に対して}S ₁ = { σ ₁ } およびS ₂ = { σ ₂ } となり、問題に出現する 各変数xに対してxσ ₁はxσ _{2の変種となります。}

例えば、統一問題{ x ≐ z , y ≐ f ( x ) }には統一子{ x ↦ z , y ↦ f ( z ) }がある。なぜなら、

これは最も一般的な統合子でもあります。同じ問題に対する他の統合子は、たとえば { x ↦ f ( x ₁ )、y ↦ f ( f ( x ₁ ))、z ↦ f ( x ₁ ) }、 { x ↦ f ( f ( x ₁ ))、y ↦ f ( f ( f ( x ₁ )))、z ↦ f ( f ( x ₁ )) } などであり、同様の統合子は無限に存在します。

別の例として、問題g ( x , x ) ≐ f ( y ) は、 ≡ が文字通りの恒等式であるという点では解が存在しません。これは、左側と右側にどのような置換を適用しても、最も外側のgとfがそれぞれ保持され、最も外側の関数記号が異なる項は構文的に異なるためです。

ジャック・エルブランは1930年に統一の基本概念について議論し、アルゴリズムを概説した。^{[9] [10] [11]}しかし、ほとんどの著者は最初の統一アルゴリズムをジョン・アラン・ロビンソン（ボックス参照）に帰している。^{[12] [13] [注5]}ロビンソンのアルゴリズムは、時間と空間の両方で最悪の場合の指数関数的動作を示した。^{[11] [15]}多くの著者がより効率的な統一アルゴリズムを提案している。^[16]最悪の線形時間動作を伴うアルゴリズムは、Martelli & Montanari (1976) と Paterson & Wegman (1976) によって独立に発見されました^{[注 6]} Baader & Snyder (2001) は Paterson-Wegman と同様の手法を使用しているため線形ですが、^{[17]ほとんどの線形時間統一アルゴリズムと同様に、} DAG表現の構築など、入力の前処理と出力の後処理のオーバーヘッドのため、小さなサイズの入力では Robinson バージョンよりも遅くなります。 de Champeaux (2022) も入力サイズに対して線形の複雑性ですが、小さなサイズの入力では Robinson アルゴリズムと競合します。高速化は、述語計算のオブジェクト指向表現を使用することで実現されます。これにより、前処理と後処理の必要性が回避され、代わりに変数オブジェクトが置換の作成とエイリアシングの処理を担当するようになります。 de Champeauxは、プログラムオブジェクトとして表現された述語計算に機能を追加する能力は、他の論理演算を最適化する機会も提供すると主張している。^[15]

以下のアルゴリズムはよく提示されており、Martelli & Montanari (1982) に由来する。^{[注 7]}有限の潜在的方程式の集合が与えられると、アルゴリズムはそれを { x ₁ ≐ u ₁ , ..., x _m ≐ u _m } の形式の同等の方程式の集合に変換する規則を適用する。ここで、x ₁、 ...、x _{m は}異なる変数であり、u ₁、 ...、u _mはx _iのいずれも含まない項である。この形式の集合は、置換として読み取ることができる。解がない場合、アルゴリズムは ⊥ で終了する。他の著者は、その場合に「Ω」、つまり「fail 」を使用する。問題Gの変数xのすべての出現を項tで置換する操作は、G { x ↦ t } と表記される。簡単にするために、定数記号は引数が 0 個の関数記号とみなされる。 ${\displaystyle G=\{s_{1}\doteq t_{1},...,s_{n}\doteq t_{n}\}}$

変数x を、 x を厳密な部分項x ≐ f (..., x , ...) として含む項と統合しようとすると、 x がそれ自身の部分項として出現するため、xの解として無限項が生じます。上で定義した (有限の) 1 次項の集合では、方程式x ≐ f (..., x , ...) には解がありません。したがって、elimate規則はx ∉ vars ( t )の場合にのみ適用できます。 この追加のチェックは、happens チェックと呼ばれ、アルゴリズムを遅くするため、たとえばほとんどの Prolog システムでは省略されています。理論的な観点からは、チェックを省略することは、無限ツリー上で方程式を解くことに相当します。下記の #無限項の統合 を参照してください。

アルゴリズムの停止性を証明するために、3 つの要素を考えます。 ここで、n _varは方程式セットで複数回出現する変数の数、n _lhsは潜在的な方程式の左辺にある関数記号と定数の数、n _{eqn は}方程式の数です。規則Eliminateを適用すると、n _{var は}減少します。これは、 x がGから削除され、{ x ≐ t }にのみ保持されるためです。その他の規則を適用しても、 n _{var が}再び増加することはありません。規則Decompose、Conflict、またはswap を適用すると、n _{lhs は}減少します。これは、少なくとも左辺の最も外側のf が消えるためです。残りの規則deleteまたはcheck のいずれかを適用すると、 n _{lhs は}増加しませんが、n _{eqn は}減少します。したがって、規則を適用すると、3 つの要素は辞書式順序に関して減少しますが、これは有限回しか起こりません。 ${\displaystyle \langle n_{var},n_{lhs},n_{eqn}\rangle }$${\displaystyle \langle n_{var},n_{lhs},n_{eqn}\rangle }$

コナー・マクブライドは^[18]、エピグラムのような依存型言語で「統一が利用する構造を表現することによって」、ロビンソンの統一アルゴリズムを変数の数だけ再帰的にすることができ、その場合には別の停止証明は不要になると指摘している。

Prolog の構文規則では、大文字で始まるシンボルは変数名、小文字で始まるシンボルは関数シンボル、コンマは論理演算子として使用されます。数学表記では、x、y、z は変数として、 f、g は関数シンボルとして、a、b は定数として使用されます。

サイズ nの構文的一階統一問題の最も一般的な統一子は、サイズが2 ⁿになることがあります。たとえば、問題⁠ ⁠${\displaystyle (((a*z)*y)*x)*w\doteq w*(x*(y*(z*a)))}$には最も一般的な統一子⁠ ⁠${\displaystyle \{z\mapsto a,y\mapsto a*a,x\mapsto (a*a)*(a*a),w\mapsto ((a*a)*(a*a))*((a*a)*(a*a))\}}$があります（図を参照）。このような爆発によって引き起こされる指数関数的な時間計算量を回避するために、高度な統一アルゴリズムは、木ではなく有向非巡回グラフ（DAG）で動作します。 ^[19]

統一の概念は、論理プログラミングの背後にある主要なアイデアの 1 つです。具体的には、統一は、式の充足可能性を決定するための推論規則である解決の基本的な構成要素です。 Prologでは、等号記号は=1 階の構文上の統一を意味します。これは、変数の内容をバインドするメカニズムを表し、一種の 1 回限りの割り当てとして考えることができます。

プロローグでは:

1. 変数は定数、項、または別の変数と統合することができ、その結果、実質的にその別名になります。多くの最新の Prolog 方言および一階述語論理では、変数はそれを含む項と統合できません。これはいわゆる発生チェックです。
2. 2 つの定数は、同一の場合のみ統合できます。
3. 同様に、項の最上位関数シンボルと項の引数が同一であり、パラメータを同時に統合できる場合、項を別の項と統合できます。これは再帰的な動作であることに注意してください。
4. 、、、+などのほとんどの演算は、によって評価されません。したがって、たとえば、は構文的に異なるため満足できません。整数算術制約を使用すると、これらの演算が解釈され評価されるE-統合の形式が導入されます。^[20]-*/=1+2 = 3#=

型推論アルゴリズムは、通常、ユニフィケーション、特に関数型言語HaskellおよびMLで使用されるHindley-Milner型推論に基づいています。たとえば、Haskell 式 の型を推論しようとすると、コンパイラーはリスト構築関数 の型、最初の引数 の型、および2 番目の引数 の型を使用します。多態型変数 はとユニファイドされ、2 番目の引数 はとユニファイドされます。と の両方を同時に 使用することはできないため、この式は正しく型付けされていません。True : ['x']a -> [a] -> [a](:)BoolTrue[Char]['x']aBool[a][Char]aBoolChar

Prolog と同様に、型推論のアルゴリズムは次のようになります。

1. 任意の型変数は任意の型式と統合され、その式にインスタンス化されます。特定の理論では、発生チェックによってこのルールが制限される場合があります。
2. 2 つの型定数は、同じ型である場合にのみ統合されます。
3. 2 つの型構成は、同じ型コンストラクタの適用であり、そのすべてのコンポーネント型が再帰的に統合される場合にのみ統合されます。

統一は計算言語学のさまざまな研究分野で利用されてきた。^{[21] [22]}

順序ソート ロジックを使用すると、各項にソートまたはタイプ を割り当て、あるソートs _{1 を}別のソートs ₂のサブソートとして宣言できます。これは通常、 s ₁ ⊆ s _{2と記述されます。たとえば、生物について推論する場合、ソート}dog をソートanimalのサブソートとして宣言すると便利です。何らかのソートsの項が必要な場合は、代わりにsの任意のサブソートの項を指定できます。たとえば、関数宣言mother : animal → animalと定数宣言lassie : dog があるとすると、項 mother ( lassie ) は完全に有効であり、ソートanimal を持ちます。次に、 dog の母親が dog であるという情報を指定するには、別の宣言mother : dog → dog を発行します。これは、プログラミング言語のオーバーロードに似た関数オーバーロードと呼ばれます。

ワルサーは、順序ソート論理の項の統一アルゴリズムを与え、任意の２つの宣言されたソートs ₁、s ₂について、それらの共通部分s ₁ ∩ s ₂も宣言する必要があることを要求した。つまり、 x ₁とx _{2 がそれぞれソート}s ₁とs ₂の変数である場合、方程式x ₁ ≐ x ₂の解は { x ₁ = x、x ₂ = x } となり、ここでx : s ₁ ∩ s ₂となる。 ^[23] このアルゴリズムを節ベースの自動定理証明器に組み込んだ後、彼はベンチマーク問題を順序ソート論理に変換することで解決することができた。その結果、多くの単項述語がソートに変換されたため、問題を一桁削減することができた。

スモルカは順序ソートの論理を一般化して、パラメトリック多態性を可能にした。 ^[24] 彼のフレームワークでは、サブソート宣言は複合型式に伝播される。プログラミングの例として、パラメトリックソートリスト（X）を宣言することができ（XはC++テンプレートのように型パラメータである）、サブソート宣言int ⊆ floatから関係list ( int ) ⊆ list ( float )が自動的に推論され、整数の各リストは浮動小数点のリストでもあることを意味する。

シュミット・シャウスは、順序ソート論理を一般化して項宣言を可能にした。 ^[25] 例として、サブソート宣言even ⊆ intとodd ⊆ intを想定すると、 ∀ i  : int . ( i + i ) : even のような項宣言により、通常のオーバーロードでは表現できない整数加算の特性を宣言することができる。

無限ツリーの背景:

• B. Courcelle (1983). 「無限木の基本特性」.理論. Comput. Sci . 25 (2): 95–169. doi : 10.1016/0304-3975(83)90059-2 .
• Michael J. Maher (1988 年 7 月)。「有限、有理、無限ツリーの代数の完全な公理化」。IEEE第 3 回コンピュータ サイエンスにおける論理に関する年次シンポジウム Proc.、エディンバラ。pp. 348–357。
• Joxan Jaffar、Peter J. Stuckey (1986)。「無限木論理プログラミングのセマンティクス」。理論計算機科学。46 :141–158。doi : 10.1016 /0304-3975(86)90027-7。

統一アルゴリズム、Prolog II:

• A. Colmerauer (1982)。KL Clark、S.-A. Tarnlund (編)。Prologと無限ツリー。Academic Press。
• Alain Colmerauer (1984)。「有限木と無限木における方程式と不等式」。ICOT (編)。第 5 世代コンピュータ システムに関する国際会議会議議事録。pp . 85–99。

用途:

• Francis Giannesini、Jacques Cohen (1984)。「Prologの無限木を使用したパーサー生成と文法操作」。Journal of Logic Programming。1 ( 3): 253–265。doi : 10.1016/0743-1066(84)90013-X。

E 統一は、方程式の背景知識Eを考慮して、与えられた方程式の集合の解を求める問題です。後者は、普遍的な等式の集合として与えられます。いくつかの特定の集合Eについては、方程式を解くアルゴリズム(別名E 統一アルゴリズム) が考案されていますが、他の集合については、そのようなアルゴリズムは存在できないことが証明されています。

例えば、aとbが異なる定数である場合、方程式 ⁠ ⁠ は、${\displaystyle x*a\doteq y*b}$演算子⁠ ⁠については何も分かっていない純粋に構文的な統一に関して解を持ちません。しかし、 ⁠ ⁠ が可換であることが分かっている場合、置換{ x ↦ b , y ↦ a }は上記の方程式を解きます。 ${\displaystyle *}$${\displaystyle *}$

背景知識E は、普遍的な等式「すべてのu、vに対して⁠ ⁠ 」によって⁠ ⁠${\displaystyle *}$の可換性を述べることができます。 ${\displaystyle u*v=v*u}$

理論の統一は、任意の入力問題に対して終了する統一アルゴリズムが考案されている場合、その理論に対して決定可能であると言われます。 理論の統一は、任意の解決可能な入力問題に対して終了するが、解決不可能な入力問題の解を永遠に探索し続ける可能性がある統一アルゴリズムが考案されている場合、その理論に対して半決定可能であると言われます。

以下の理論については 統一が決定可能です。

• [ ^26]
• A、 C ^[27]
• A、 C、 I ^[28]
• A、 C、 Nl _[^{注9] [28]}
• A、私^[29]
• A , N _l , N _r（モノイド） ^[30]
• C ^[31]
• ブール環^{[32] [33]}
• アーベル群は、署名が任意の追加記号（公理ではない）によって拡張された場合でも、^[34]
• K4 様相代数^[35]

以下の理論については、 統一は半決定可能です。

• A、 Dl、_Dr ^[ ₃₆ ]
• A、 C、 Dl _[^{注9] [37]}
• 可換環^[34]

Eに対して収束項書き換えシステム Rが利用可能な場合、片側パラモジュレーションアルゴリズム^[38] を使用して、与えられた方程式のすべての解を列挙することができます。

G を解決すべき統一問題、S を恒等置換から始めて、空集合が実際のG​​ として現れるまで非決定的に規則を適用します。この場合、実際のSは統一置換です。パラモジュレーション規則を適用する順序、Gからの実際の方程式の選択、およびmutateにおけるRの規則の選択に応じて、異なる計算パスが可能です。一部だけが解決につながり、その他はG ≠ {} で終了し、それ以上の規則は適用できません (例: G = { f (...) ≐ g (...) })。

一例として、項書き換えシステムR は、 consとnilから構築されたリストの追加演算子を定義するために使用されます。ここで、cons ( x、y ) は、簡潔にするために、中置記法でx . yと記述されます。たとえば、app ( a . b . nil、c . d . nil ) → a . app ( b . nil、c . d . nil ) → a . b . app ( nil、c . d . nil ) → a . b . c . d . nil は、書き換え規則 2、2、および 1 を使用して、リストa . b . nilとc . d . nilの連結を示しています。 Rに対応する等式理論E は、 Rの合同閉包であり、どちらも項上の二項関係として見られます。たとえば、app ( a . b . nil , c . d . nil ) ≡ a . b . c . d . nil ≡ app ( a . b . c . d . nil , nil )。パラモジュレーション アルゴリズムは、例Rが入力されると、そのEに関する方程式の解を列挙します。

統一問題 { app ( x , app ( y , x )) ≐ a . a . nil } の成功した計算パスの例を以下に示します。変数名の衝突を避けるために、書き換え規則は、規則mutateによって使用される前に毎回一貫して名前が変更されます。v ₂、v ₃、... は、この目的のためにコンピューターによって生成された変数名です。各行で、Gから選択された方程式は赤で強調表示されています。 mutate規則が適用されるたびに、選択された書き換え規則 ( 1または2 ) が括弧内に示されます。最後の行から、統一置換S = { y ↦ nil、x ↦ a . nil } を取得できます。実際、 app ( x、app ( y、x )) { y ↦ nil、x ↦ a . nil } = app ( a . nil , app ( nil , a . nil )) ≡ app ( a . nil , a . nil ) ≡ a . app ( nil , a . nil ) ≡ a . a . nilは与えられた問題を解決します。「mutate(1), mutate(2), mutate(2), mutate(1)」を選択することで得られる 2 番目の成功計算パスは、置換S = { y ↦ a . a . nil , x ↦ nil } につながりますが、ここには示されていません。他のパスは成功につながりません。

R がEの収束項書き換えシステムである場合、前のセクションに代わるアプローチは、「絞り込みステップ」を連続的に適用することである。これにより、最終的に与えられた方程式のすべての解が列挙される。絞り込みステップ（図参照）は、

• 現在の項の非変数部分項を選択し、
• Rの規則の左辺と構文的に統合し、
• インスタンス化されたルールの右側をインスタンス化された項に置き換えます。

正式には、l → r がRからの書き換え規則の名前を変更したコピーであり、項sと共通の変数を持たず、部分項s | _pが変数ではなく、mgu σを介してlと統一可能である場合、s は項t = sσ [ rσ ] _p、つまり項sσに絞り込まれ、 pの部分項がrσに置き換えられます。 s がtに絞り込まれる状況は、通常s ↝ tと表されます。 直感的には、一連の絞り込みステップt ₁ ↝ t ₂ ↝ ... ↝ t _{n は}、一連の書き換えステップt ₁ → t ₂ → ... → t _nとして考えることができますが、最初の項t ₁は、使用される各規則を適用できるように必要に応じてさらにインスタンス化されます。

上記の例のパラモジュレーション計算は、次の絞り込みシーケンスに対応します (「↓」はここでインスタンス化を示します)。

最後の項v ₂ . v ₂ . nil は、元の右側の項a . a . nilと構文的に統合できます。

狭義の補題[ ^39]は、項sのインスタンスが収束項書き換えシステムによって項tに書き換えられるときはいつでも、 sとtは狭義に項s ′とt ′に書き換えられ、 t ′はs ′のインスタンスとなることを保証する。

正式には：常にsσ →∗ t が何らかの置換 σ に対して成り立つ場合、項s ′ , t ′が存在し、 s ↝∗ s ′とt →∗ t ′およびs ′ τ = t ′（何らかの置換 τ の場合）。

多くのアプリケーションでは、一次項の代わりに型付きラムダ項の統一を考慮する必要があります。このような統一は、しばしば高次統一と呼ばれます。高次統一は決定不能であり、^{[40] [41] [42]}このような統一問題には最も一般的な統一子はありません。たとえば、唯一の変数がfである統一問題 { f ( a , b , a ) ≐ d ( b , a , c ) } には、解 { f ↦ λ x .λ y .λ z . d ( y , x , c ) }、{ f ↦ λ x .λ y .λ z . d ( y , z , c ) }、{ f ↦ λ x .λ y .λ z .高階統一の問題として、{ f ↦ λ x .λ y .λ z . d ( b , x , c ) }、{ f ↦ λ x .λ y .λ z . d ( b , z , c ) }、{ f ↦ λ x .λ y .λ z . d ( b , z , c ) }、{ f ↦ λ x .λ y .λ z . d ( b , a , c ) } などがあります。高階統一の問題でよく研究されているのは、αβη 変換によって決定される等式を法として単純型ラムダ項を統一する問題です。Gérard Huet は、半決定可能(事前) 統一アルゴリズム^[43]を提示しました。これは、統一子の空間を体系的に検索することを可能にします (Martelli-Montanari ^[5]の統一アルゴリズムを、高階変数を含む項の規則で一般化したもの)。これは実際に十分に機能するようです。 Huet ^[44]とGilles Dowek ^[45]は、このテーマを調査した記事を書いています。

高階統一のいくつかのサブセットは、決定可能であり、解決可能な問題に対する最も一般的な統一子を持つという点で、行儀が良い。そのようなサブセットの 1 つが、前述の 1 階項である。Dale Miller による高階パターン統一^[46]もそのようなサブセットの 1 つである。高階論理プログラミング言語λPrologとTwelf は、完全な高階統一からパターン フラグメントのみの実装に切り替えた。驚くべきことに、パターン統一は、パターン統一以外の各問題が、後続の置換によって統一がパターン フラグメントに配置されるまで保留されている場合、ほとんどすべてのプログラムで十分である。パターン統一のスーパーセットである関数構築子統一も行儀が良い。^[47] Zipperposition 定理証明器には、これらの行儀の良いサブセットを完全な高階統一アルゴリズムに統合するアルゴリズムがある。^[2]

計算言語学において、省略構文の最も影響力のある理論の一つは、省略記号は自由変数で表現され、その値は高階統一法によって決定されるというものである。例えば、「ジョンはメアリーが好きで、ピーターも好きである」の意味表現は like( j , m ) ∧ R( p )であり、R（省略記号の意味表現）の値はlike( j , m ) = R( j ) という式によって決定される。このような式を解くプロセスは高階統一法と呼ばれる。^[48]

ウェイン・スナイダーは、高階統一とE統一の両方の一般化、すなわち方程式理論を法としてラムダ項を統一するアルゴリズムを与えた。^[49]

• 書き直し
• 許容ルール
• ラムダ計算における明示的な置換
• 数式を解く
• 不統一：記号表現間の不等式を解く
• 反統一: 最も一般的なインスタンス (mgu) の計算と双対となる、2 つの項の最小一般化 (lgg) の計算
• 包摂格子、統一を交わり、反統一を結合とする格子
• オントロジーの整合（意味的等価性による統一を使用）