Critical pair (logic)

From Wikipedia, the free encyclopedia
Triangle diagram of a critical pair obtained from two rewrite rules s→t (upper row, left) and l→r (right). The substitution σ unifies the subterm sp with l. The resulting overlay term sσ[lσ]p (lower row, middle) can be rewritten to the term tσ and sσ[rσ]p (lower row, left and right), respectively. The latter two terms form the critical pair. They can be eventually rewritten to a common term, if the rewrite rule set is confluent.

In mathematical logic, 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

f(g(x,y),z) → g(x,z)
g(x,y) → x,

the only critical pair is ⟨g(x,z), f(x,z)⟩.

When both sides of the critical pair can reduce to the same term, the critical pair is called convergent. Where one side of the critical pair is identical to the other, the critical pair is called trivial.

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, the critical pair lemma states that a term rewriting system is weakly (a.k.a. locally) confluent if all critical pairs are convergent. Thus, to find out if a term rewriting system is weakly confluent, it suffices to test all critical pairs and see if they are convergent. This makes it possible to find out algorithmically if a term rewriting system is weakly confluent or not.

Weak confluence clearly implies convergent critical pairs: if any critical pair ⟨a, b⟩ arises, then a and b have common reduct and thus the critical pair is convergent.

See also

  • Knuth-Bendix completion, an algorithm based on critical pairs to compute a confluent and terminating term rewriting system equivalent to a given one

External links

References

  • Franz Baader and Tobias Nipkow, Term Rewriting and All That, Cambridge University Press, 1998 (book weblink)
  • Terese, Term Rewriting Systems, Cambridge Tracts in Theoretical Computer Science, 2003. (book weblink)
This article is issued from Wikipedia. The text is available under the Creative Commons Attribution/Share Alike; additional terms may apply for the media files.