Overlap (term rewriting)

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.

Examples

Consider the term rewriting system defined by the following reduction rules:

${\displaystyle \rho _{1}\$ :\ f(g(x),y)\rightarrow y}

${\displaystyle \rho _{2}\$ :\ g(x)\rightarrow f(x,x)}

The term ${\displaystyle f(g(x),y)}$ can be reduced via ρ₁ to yield y, but it can also be reduced via ρ₂ to yield ${\displaystyle f(f(x,x),y).}$. Note how the redex ${\displaystyle g(x)}$ is contained in the redex ${\displaystyle f(g(x),y)}$. 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 ${\displaystyle (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:

${\displaystyle \rho _{1}\$ :\ g(g(x))\rightarrow x}

The term ${\displaystyle g(g(g(x)))}$ has overlapping redexes, which can be either applied to the innermost occurrence or to the outermost occurrence of the ${\displaystyle g(g(x))}$ term.