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

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

臨界ペアの実際の定義は、置換によって臨界ペアから得られるペアを除外し、重複に基づいてペアを方向付けるため、やや複雑です。具体的には、重複する規則のペア と の場合、重複は、空でないコンテキストと項(変数ではない) が最も一般的ないくつかの置換で一致する場合、臨界ペアは です。^[1]${\displaystyle \rho_{0}:l_{0}\tor_{0}}$${\displaystyle \rho_{1}:l_{1}\tor_{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 )}$

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

例えば、ルール付き書き換えシステムという用語では

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

別の例として、次の単一ルールを持つ項書き換えシステムを考える。

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

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

臨界対補題は、すべての臨界対が収束する場合に限り、項書き換えシステムが弱合流性（つまり局所的合流性）を持つことを規定しています。したがって、項書き換えシステムが弱合流性であるかどうかを調べるには、すべての臨界対をテストし、それらが収束するかどうかを確認すれば十分です。これにより、2 つの項が収束するかどうかをアルゴリズム的に確認できることを前提として、項書き換えシステムが弱合流性であるかどうかをアルゴリズム的に調べることができます。

• クヌース・ベンディックス完備化、与えられたものと同等の合流性があり停止性のある項書き換えシステムを計算するための臨界対に基づくアルゴリズム

• Weisstein、Eric W.「Critical Pair」。MathWorld。

• フランツ・バーダーとトビアス・ニプコウ著『 Term Rewriting and All That』、ケンブリッジ大学出版局、1998年（書籍のウェブリンク）