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.[1]
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.
Consider the term rewriting system defined by the following reduction rules:
\rho1 : f(g(x),y) → y
\rho2 : g(x) → f(x,x)
The term
f(g(x),y)
f(f(x,x),y).
g(x)
f(g(x),y)
(f(f(x,x),y),y)
Overlap may occur with fewer than two reduction rules.
Consider the term rewriting system defined by the following reduction rule:
\rho1 : g(g(x)) → x
g(g(g(x)))
g(g(x))