Situation in which there are contradictory ways of reducing a mathematical expression
In mathematics, computer science and logic, overlap, as a property of the reduction rules in term rewriting system, describes a situation where a number of different reduction rules specify potentially contradictory ways of reducing a reducible expression, also known as a redex, within a term.
More precisely, if a number of different reduction rules share function symbols on the left-hand side, overlap can occur. Often we do not consider trivial overlap with a redex and itself.
Examples.
Consider the term rewriting system defined by the following reduction rules:
 formula_1
 formula_2
The term formula_3 can be reduced via ρ1 to yield "y", but it can also be reduced via ρ2 to yield formula_4. Note how the redex formula_5 is contained in the redex formula_3. The result of reducing different redexes is described in a what is known as a critical pair; the critical pair arising out of this term rewriting system is formula_7.
Overlap may occur with fewer than two reduction rules.
Consider the term rewriting system defined by the following reduction rule:
 formula_8
The term formula_9 has overlapping redexes, which can be either applied to the innermost occurrence or to the outermost occurrence of the formula_10 term.
References.
 ;templatestyles src="Reflist/styles.css" / ;