Overlap (term rewriting) explained

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:

\rho1 :f(g(x),y)y

\rho2 :g(x)f(x,x)

The term

f(g(x),y)

can be reduced via ρ1 to yield, 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:

\rho1 :g(g(x))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.

Notes and References

  1. Book: Term Rewriting Systems . Marc Bezem . Jan Willem Klop . Roel de Vrijer . Cambridge Tracts in Theoretical Computer Science . . 2003 . 0-521-39115-6 . 48. Cambridge, UK .