Misplaced Pages

Critical pair (term rewriting)

Article snapshot taken from Wikipedia with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.
(Redirected from Critical pair lemma) This article is about terms resulting from overlaps in term rewriting systems. For other uses, see Critical pair.
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 s|p with l. The resulting overlay term sσp (lower row, middle) can be rewritten to the term tσ and sσ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. (For notation details, see Term (logic) § Operations with terms.)

A critical pair arises in a term rewriting system when two rewrite rules overlap to yield two different terms. In more detail, (t1, t2) is a critical pair if there is a term t for which two different applications of a rewrite rule (either the same rule applied differently, or two different rules) yield the terms t1 and t2.

Definitions

The actual definition of a critical pair is slightly more involved as it excludes pairs that can be obtained from critical pairs by substitution and orients the pair based on the overlap. Specifically, for a pair of overlapping rules ρ 0 : l 0 → r 0 {\displaystyle \rho _{0}:l_{0}\to r_{0}} and ρ 1 : l 1 → r 1 {\displaystyle \rho _{1}:l_{1}\to r_{1}} , with the overlap being that l 0 = D [ s ] {\displaystyle l_{0}=D} for some non-empty context D [ ] {\displaystyle D} , and the term s {\displaystyle s} (that is not a variable) matches l 1 {\displaystyle l_{1}} under some substitutions s σ = l 1 τ {\displaystyle s\sigma =l_{1}\tau } that are most general, the critical pair is ( D σ [ r 1 τ ] , r 0 σ ) {\displaystyle (D\sigma ,r_{0}\sigma )} .

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.

Examples

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)⟩. Both of these terms can be derived from the term f(g(x,y),z) by applying a single rewrite rule.

As another example, consider the term rewriting system with the single rule

f(x,y) → x.

By applying this rule in two different ways to the term f(f(x,x),x), we see that (f(x,x), f(x,x)) is a (trivial) critical pair.

Critical pair lemma

Confluence clearly implies convergent critical pairs: if any critical pair ⟨a, b⟩ arises, then a and b have a common reduct and thus the critical pair is convergent. If the term rewriting system is not confluent, the critical pair may not converge, so critical pairs are potential sources where confluence will fail.

The critical pair lemma states that a term rewriting system is weakly (a.k.a. locally) confluent if and only 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, given that one can algorithmically check if two terms converge.

See also

External links

References

  1. Terese (2003). Term rewriting systems. Cambridge, UK: Cambridge University Press. p. 53. ISBN 0-521-39115-6.
Category: