critical pair
In term rewriting, a critical pair is, intuitively, a pair of terms for which there exists a term such that and “in two different ways”.
Let and be (possibly equal) rewrite rules in a TRS such that
- and have no variables in common, and
- (the subterm of at position ) is not a variable.
Let be a most general unifier of and , so that . Then we have both by the first rule and by the second rule. The pair is a critical pair.
The requirement that and have no variables in common is purely technical: any common variables can always be renamed.