Critical Pair

Let  and  be two rules of a term rewriting system, and suppose these rules have no variables in common. If they do, rename the variables. If  is a subterm of  (or the term  itself) such that it is not a variable, and the pair  is unifiable with the most general unifier , then  and the result of replacing  in  by  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  and , then  and  would form a critical pair because they can both be derived from .

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.

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.