Overlap (term rewriting)

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 (or 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.

For example, consider the term rewriting system defined by the 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 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 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

  • "Terese"; Marc Bezem, J. W. Klop, Roel de Vrijer (2003). Term Rewriting Systems. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press. p. 48. ISBN 0-521-39115-6. 



Wikimedia Foundation. 2010.

Игры ⚽ Поможем написать курсовую

Look at other dictionaries:

  • Orthogonality (term rewriting) — Orthogonality as a property of term rewriting systems describes where the reduction rules of the system are all left linear, that is each variable occurs only once on the left hand side of each reduction rule, and there is no overlap between them …   Wikipedia

  • List of mathematics articles (O) — NOTOC O O minimal theory O Nan group O(n) Obelus Oberwolfach Prize Object of the mind Object theory Oblate spheroid Oblate spheroidal coordinates Oblique projection Oblique reflection Observability Observability Gramian Observable subgroup… …   Wikipedia

  • Knuth-Bendix completion algorithm — The Knuth Bendix completion algorithm is an algorithm for transforming a set of equations (over terms) into a confluent term rewriting system. When the algorithm succeeds, it has effectively solved the word problem for the specified algebra. An… …   Wikipedia

  • Critical pair (logic) — In mathematical logic, a critical pair arises in term rewriting systems where rewrite rules overlap to yield two different terms. For example, in the term rewriting system with rules , the only critical pair is then (g(x,z), f(x,z)). When one… …   Wikipedia

  • Reduction strategy — In code optimization during the translation of computer programs into an executable form, and in mathematical reduction generally, a reduction strategy for a term rewriting system determines which reducible subterms (or reducible expressions,… …   Wikipedia

  • Palestinian people — Palestinians (الفلسطينيون al Filasṭīniyyūn) Tawfiq Canaan • …   Wikipedia

  • logic, history of — Introduction       the history of the discipline from its origins among the ancient Greeks to the present time. Origins of logic in the West Precursors of ancient logic       There was a medieval tradition according to which the Greek philosopher …   Universalium

  • Database — A database is an organized collection of data for one or more purposes, usually in digital form. The data are typically organized to model relevant aspects of reality (for example, the availability of rooms in hotels), in a way that supports… …   Wikipedia

  • Accountability — is the concept in ethics and governance with several meanings. It is often used synonymously with such concepts as responsibility,[1] answerability, blameworthiness, liability, and other terms associated with the expectation of account giving. As …   Wikipedia

  • biblical literature — Introduction       four bodies of written works: the Old Testament writings according to the Hebrew canon; intertestamental works, including the Old Testament Apocrypha; the New Testament writings; and the New Testament Apocrypha.       The Old… …   Universalium

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”