title: Overlap (term rewriting)
text: # 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.
  
  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:
  
      $\rho _{1}\ :\ f(g(x),y)\rightarrow y$
      $\rho _{2}\ :\ g(x)\rightarrow f(x,x)$
  
  The term $f(g(x),y)$ can be reduced via $ρ_1$ to yield y, but it can also be reduced via $ρ_2$ to yield $f(f(x,x),y).$. Note how the redex $g(x)$ is contained in the redex $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 $(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:
  
      $\rho _{1}\ :\ g(g(x))\rightarrow x$
  
  The term $g(g(g(x)))$ has overlapping redexes, which can be either applied to the innermost occurrence or to the outermost occurrence of the $g(g(x))$ term.
  
  