overlap (term rewriting)

{{short description|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.{{cite book | title=Term Rewriting Systems | author1=Marc Bezem |author2=Jan Willem Klop |author3=Roel de Vrijer | series=Cambridge Tracts in Theoretical Computer Science | publisher=Cambridge University Press | year=2003 | isbn=0-521-39115-6 | page=48|url=https://books.google.com/books?id=7QQ5u-4tRUkC |location=Cambridge, UK }}

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 ρ₁ to yield {{math|y}}, but it can also be reduced via ρ₂ 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.

References

Category:Rewriting systems