TOPICS
Search

Critical Pair


Let x->y and u->v be two rules of a term rewriting system, and suppose these rules have no variables in common. If they do, rename the variables. If x_1 is a subterm of x (or the term x itself) such that it is not a variable, and the pair (x_1,u) is unifiable with the most general unifier theta, then ytheta and the result of replacing x_1theta in xtheta by vtheta are called a critical pair.

The fact that all critical pairs of a term rewriting system are joinable, i.e., can be reduced to the same expression, implies that the system is locally confluent.

For instance, if f(x,x)->x and g(f(x,y),x)->h(x), then g(x,x) and h(x) would form a critical pair because they can both be derived from g(f(x,x),x).

Note that it is possible for a critical pair to be produced by one rule, used in two different ways. For instance, in the string rewrite "AA" -> "B", the critical pair ("BA", "AB") results from applying the one rule to "AAA" in two different ways.


See also

Church-Rosser Property, Confluent, Finitely Terminating, Knuth-Bendix Completion Algorithm, Reduction Order, Term Rewriting System

Portions of this entry contributed by Todd Rowland

Portions of this entry contributed by Alex Sakharov (author's link)

Explore with Wolfram|Alpha

References

Baader, F. and Nipkow, T. Term Rewriting and All That. Cambridge, England: Cambridge University Press, 1999.Wolfram, S. A New Kind of Science. Champaign, IL: Wolfram Media, p. 1037, 2002.

Referenced on Wolfram|Alpha

Critical Pair

Cite this as:

Rowland, Todd; Sakharov, Alex; and Weisstein, Eric W. "Critical Pair." From MathWorld--A Wolfram Web Resource. https://mathworld.wolfram.com/CriticalPair.html

Subject classifications