Overlap (term rewriting)
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 (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
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
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.
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
, computer science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
and logic
Logic
In philosophy, Logic is the formal systematic study of the principles of valid inference and correct reasoning. Logic is used in most intellectual activities, but is studied primarily in the disciplines of philosophy, mathematics, semantics, and computer science...
, 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
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
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 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
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.