Jump to content

Overlap (term rewriting)

From Wikipedia, the free encyclopedia

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

[edit]

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

The term can be reduced via ρ1 to yield y, but it can also be reduced via ρ2 to yield . Note how the redex is contained in the redex . 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 .

Overlap may occur with fewer than two reduction rules.

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

The term has overlapping redexes, which can be either applied to the innermost occurrence or to the outermost occurrence of the term.

References

[edit]
  1. ^ Marc Bezem; Jan Willem Klop; Roel de Vrijer (2003). Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge, UK: Cambridge University Press. p. 48. ISBN 0-521-39115-6.