Overlap (term rewriting)

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.