統一（コンピュータ科学）

形式的には、統一アプローチは

• 無限集合${\displaystyle V}$変数の。高階統一には、選択するのが便利です。${\displaystyle V}$ラムダ項で束縛された変数の集合とは互いに素である。
• セット${\displaystyle T}$条件の​${\displaystyle V\subseteq T}$一次統一の場合、${\displaystyle T}$通常は、 1 階項(変数と関数の記号から構成される項)の集合です。高階の統一については、${\displaystyle T}$一次項とラムダ項（高階変数を含む項）から構成される。
• マッピング${\displaystyle {\text{vars}}\colon T\rightarrow }$${\displaystyle \mathbb {P} }$${\displaystyle (V)}$各項に割り当て${\displaystyle t}$セット${\displaystyle {\text{vars}}(t)\subsetneq V}$自由変数の出現${\displaystyle t}$。
• 理論または同値関係${\displaystyle \equiv }$の上${\displaystyle T}$、どの項が等しいとみなされるかを示します。一次E統一の場合、${\displaystyle \equiv }$特定の関数記号に関する背景知識を反映しています。たとえば、${\displaystyle \oplus }$可換であると考えられている。${\displaystyle t\equiv u}$もし${\displaystyle u}$結果${\displaystyle t}$引数を交換することで${\displaystyle \oplus }$いくつかの（おそらくすべての）事例において。^{[注1 ]}背景知識がまったくない最も典型的なケースでは、文字通り、または構文的に同一の用語のみが等しいとみなされます。この場合、≡ は自由理論（自由オブジェクトであるため）、空理論（等式文の集合、つまり背景知識が空であるため）、未解釈関数の理論（単一化は未解釈の用語に対して行われるため）、またはコンストラクタの理論（すべての関数記号はデータ項に対して操作するのではなく、データ項を構築するだけであるため）と呼ばれます。高階単一化の場合、通常は${\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 が関数変数であるため、構文上の二次単一化問題です。一つの解決策は { x ↦ a , y ↦ (恒等関数) } であり、もう一つの解決策は { y ↦ (各値をaにマッピングする定数関数), x ↦ (任意の値) } です。

置換とは写像のことである${\displaystyle \sigma :V\rightarrow T}$変数から項へ。表記法${\displaystyle \{x_{1}\mapsto t_{1},...,x_{k}\mapsto t_{k}\}}$各変数の置換マッピングを指します${\displaystyle x_{i}}$その用語に$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}$による$t_i$。 結果${\displaystyle t\tau }$置換を適用する$\displaystyle \tau }$期間に${\displaystyle t}$それはその用語のインスタンスと呼ばれます${\displaystyle t}$1 次例として、項に置換{ x ↦ h ( a , y ), z ↦ b }を適用すると、

用語${\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})}$なぜなら、いかなる置換によっても後者の項を前者の項に変換することはできないからである。したがって、後者の項は前者の項よりも本質的に特別なものである。

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

代替品${\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 }$[ ^{2 ]} 例えば^​${\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)}$[ ^{3 ]​}

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

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

集合Sは、そのどの要素も他の要素を包含しない場合に最小であると呼ばれます。フレームワークによっては、完全かつ最小の置換集合は、0 個、1 個、有限個、または無限個の要素を持つ場合があり、冗長な要素の無限連鎖のためにまったく存在しない場合もあります。 ^{[ 4 ]}したがって、一般に、統合アルゴリズムは、完全な集合の有限近似を計算します。これは最小である場合もそうでない場合もありますが、ほとんどのアルゴリズムは可能な限り冗長な統合子を回避します。^{[ 2 ]} 1 階構文統合については、Martelli と Montanari ^{[ 5 ]}は、解決不可能性を報告するか、それ自体で完全かつ最小の置換集合を形成する単一の統合子を計算するアルゴリズムを提供しました。これは最も一般的な統合子と呼ばれます。

ジャック・エルブランは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 アルゴリズムと同等の性能を発揮します。高速化は、前処理と後処理を不要にする述語計算のオブジェクト指向表現を使用することで実現され、代わりに変数オブジェクトが置換の作成とエイリアシングの処理を担当します。ド・シャンポーは、プログラムオブジェクトとして表現された述語論理に機能を追加できる能力は、他の論理演算を最適化する機会も提供すると主張している。^{[ 15 ]}

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

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 ]}

単一化の概念は、論理プログラミングの根幹をなす考え方の一つです。具体的には、単一化は、論理式の充足可能性を判定するための推論規則である解決の基本的な構成要素です。Prologでは、等号は=一階述語論理の単一化を意味します。これは変数の内容を束縛するメカニズムを表し、一種の一回限りの代入と見なすことができます。

プロローグ：

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 ]}

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

以下の理論については、統一性が決定可能である。

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

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

• A、 D _l、D _r ^{[ 35 ]}
• A、 C、 D _l ^{[注9 ] [ 36 ]}
• 可換環^{[ 33 ]}

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

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 2 _、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と構文的に統一できます。

狭窄補題[ ^{38 ]は}、項sのインスタンスが収束項書き換えシステムによって項tに書き換えられる場合、 sとtはそれぞれ項s ′とt ′に狭窄および書き換えられ、t ′はs ′のインスタンスとなることを保証する。

形式的には、ある置換 σ に対してsσ → ∗ tが成り立つ場合、ある置換 τ に対してs ↝ ∗ s ′およびt → ∗ t ′およびs ′ τ = t ′となる項s ′、t ′が存在する。