Critical pair

From Wikipedia, the free encyclopedia

A critical pair arises in term rewriting systems where rewrite rules overlap to yield two different terms.

For example, in the term rewriting system with rules

,

consider the term f(g(x,x), x). Applying ρ₁ yields the term g(x,x), while applying ρ₂ yields the term f(x,x). The critical pair is then (g(x,x), f(x,x)).

When one side of the critical pair reduces to the other, we say that the critical pair is convergent. Where one side of the critical pair is identical to the other, we say that the critical pair is trivial.

Note that if the term rewriting system is not confluent, the critical pair may not converge, so critical pairs are potential sources where confluence will fail. In fact, we have the critical pair lemma, which states that a term rewriting system is weakly confluent if all critical pairs are convergent. Weak confluence implies convergent critical pairs clearly as if any critical pair, say (a, b) arises, then a and b have common reduct and thus the critical pair is convergent.

[edit] External links

• Weisstein, Eric W., Critical Pair at MathWorld.