クリティカルペア（用語の書き換え）

項書き換えシステムにおいて、2 つの書き換え規則が重なり合って 2 つの異なる項を生成する場合、クリティカル ペアが発生します。より詳細には、( t 1 , _t 2 )_は、項tに対して 2 つの異なる書き換え規則の適用 (同じ規則を異なる方法で適用するか、2 つの異なる規則を適用する) によって項t ₁とt ₂が生成される場合にクリティカル ペアとなります。

クリティカルペアの実際の定義は、置換によってクリティカルペアから得られるペアを除外し、重複に基づいてペアの向きを決定するため、もう少し複雑です。具体的には、重複するルールのペアの場合、${\displaystyle \rho _{0}:l_{0}\to r_{0}}$そして$\displaystyle \rho _{1}:l_{1}\to r_{1}}$重複する部分は${\displaystyle l_{0}=D[s]}$空でないコンテキストの場合${\displaystyle D[\;]}$、そしてその用語${\displaystyle s}$（変数ではない）が一致します${\displaystyle l_{1}}$いくつかの代替案の下で$\displaystyle s\sigma =l_{1}\tau }$最も一般的なもの、重要なペアは${\displaystyle (D\sigma [r_{1}\tau ],r_{0}\sigma )}$[ ^{1 ]​}

臨界対の両辺が同じ項に簡約できる場合、その臨界対は収束的であると呼ばれます。臨界対の一方の辺がもう一方の辺と同一である場合、その臨界対は自明であると呼ばれます。

例えば、ルールによる用語書き換えシステムでは

唯一の重要なペアは⟨g ( x , z ) , f ( x , z )⟩です。これらの2つの項は、1つの書き換え規則を適用することで、項f ( g ( x , y ), z )から導出できます。

別の例として、単一のルールを持つ用語書き換えシステムを考えてみましょう。

この規則を項f ( f ( x , x ), x ) に 2 つの異なる方法で適用すると、( f ( x , x ), f ( x , x )) が (自明な) 臨界ペアであることがわかります。

合流性は明らかに収束する臨界対を意味します。臨界対⟨a, b⟩が生じた場合、 aとbは共通の縮約を持ち、したがって臨界対は収束します。項書き換えシステムが合流性でない場合、臨界対は収束しない可能性があり、したがって臨界対は合流性が失敗する可能性のある原因となります。

クリティカルペア補題によれば、項書き換えシステムが弱合流性（局所合流性）であるのは、すべてのクリティカルペアが収束する場合に限る。したがって、項書き換えシステムが弱合流性であるかどうかを判断するには、すべてのクリティカルペアをテストして、それらが収束するかどうかを確認すればよい。2つの項が収束するかどうかをアルゴリズム的にチェックできれば、項書き換えシステムが弱合流性であるかどうかをアルゴリズム的に判断することが可能となる。

• Knuth–Bendix補完とは、与えられたものと同等の合流的かつ終端的な項書き換えシステムを計算するために、クリティカルペアに基づくアルゴリズムである。

• ワイススタイン、エリック W. 「臨界ペア」 . MathWorld .

• フランツ・バーダー、トビアス・ニプコウ著、『用語の書き換えとその他すべて』、ケンブリッジ大学出版局、1998年（書籍ウェブリンク）