Rewrite order

Last updated October 21, 2022

In theoretical computer science, in particular in automated reasoning about formal equations, reduction orderings are used to prevent endless loops. Rewrite orders, and, in turn, rewrite relations, are generalizations of this concept that have turned out to be useful in theoretical investigations.

Motivation

Intuitively, a reduction order R relates two formal expressions s and t if t is properly "simpler" than s in some sense.

For example, simplification of terms may be a part of a computer algebra program, and may be using the rule set { x+0 → x , 0+x → x , x*0 → 0, 0*x → 0, x*1 → x , 1*x → x }. In order to prove impossibility of endless loops when simplifying a term, the reduction order defined by "sRt if expression t is properly shorter than expression s" can be used; applying any rule from the set will always properly shorten the term.

In contrast, to establish termination of "distributing-out" using the rule x*(y+z) → x*y+x*z, a more elaborate reduction order will be needed, since this rule may blow up the term size due to duplication of x. The theory of rewrite orders aims at helping to provide an appropriate order in such cases.

Formal definitions

Formally, a binary relation (→) on the set of terms is called a rewrite relation if it is closed under contextual embedding and under instantiation; formally: if l→r implies u [ l σ]_p→u[rσ]_p for all terms l, r, u, each path p of u, and each substitution σ. If (→) is also irreflexive and transitive, then it is called a rewrite ordering,^[1] or rewrite preorder . If the latter (→) is moreover well-founded, it is called a reduction ordering,^[2] or a reduction preorder. Given a binary relation R, its rewrite closure is the smallest rewrite relation containing R.^[3] A transitive and reflexive rewrite relation that contains the subterm ordering is called a simplification ordering.^[4]

Overview of rewrite relations^{[note 1]}
	rewrite relation	rewrite order	reduction order	simplification order
closed under context x R y implies u [ x]_pRu[y]_p	Yes	Yes	Yes	Yes
closed under instantiation x R y implies x σ Ryσ	Yes	Yes	Yes	Yes
contains subterm relation y subterm of x implies x R y				Yes
reflexive always x R x		(No)	(No)	Yes
irreflexive never x R x		Yes	Yes	(No)
transitive x R y and y R z implies x R z		Yes	Yes	Yes
well-founded no infinite chain x₁Rx₂Rx₃R ...^{[note 2]}			Yes	(Yes)

Properties

The converse, the symmetric closure, the reflexive closure, and the transitive closure of a rewrite relation is again a rewrite relation, as are the union and the intersection of two rewrite relations.^[1]
The converse of a rewrite order is again a rewrite order.
While rewrite orders exist that are total on the set of ground terms ("ground-total" for short), no rewrite order can be total on the set of all terms.^{[note 3]}^[5]
A term rewriting system ${l 1 ::= r 1,..., l n ::= r n, ...}$ is terminating if its rules are a subset of a reduction ordering.^{[note 4]}^[2]
Conversely, for every terminating term rewriting system, the transitive closure of (::=) is a reduction ordering,^[2] which needn't be extendable to a ground-total one, however. For example, the ground term rewriting system { f(a)::=f(b), g(b)::=g(a) } is terminating, but can be shown so using a reduction ordering only if the constants a and b are incomparable.^{[note 5]}^[6]
A ground-total and well-founded rewrite ordering^{[note 6]} necessarily contains the proper subterm relation on ground terms.^{[note 7]}
Conversely, a rewrite ordering that contains the subterm relation^{[note 8]} is necessarily well-founded, when the set of function symbols is finite.^[5]^{[note 9]}
A finite term rewriting system ${l 1 ::= r 1,..., l n ::= r n, ...}$ is terminating if its rules are subset of the strict part of a simplification ordering.^[4]^[8]

Notes

↑ Parenthesized entries indicate inferred properties which are not part of the definition. For example, an irreflexive relation can't be reflexive (on a nonempty domain set).
↑ except all x_i are equal for all i beyond some n, for a reflexive relation
↑ Since x<y implies y<x, since the latter is an instance of the former, for variables x, y.
↑ i.e. if $l i > r i$ for all i, where (>) is a reduction ordering; the system needn't have finitely many rules
↑ Since e.g. $a > b$ implied $g (a)> g (b)$ , meaning the second rewrite rule was not decreasing.
↑ i.e. a ground-total reduction ordering
↑ Else, t|_p > t for some term t and position p, implying an infinite descending chain t > t[t]_p > t[t[t]_p]_p > ...^[6]^[7]
↑ i.e. a simplification ordering
↑ The proof of this property is based on Higman's lemma, or, more generally, Kruskal's tree theorem.

Related Research Articles

In mathematics, a binary relation associates elements of one set, called the domain, with elements of another set, called the codomain. A binary relation over sets $X$ and $Y$ is a new set of ordered pairs $(x, y)$ consisting of elements $x$ in $X$ and $y$ in $Y$ . It is a generalization of the more widely understood idea of a mathematical function, but with fewer restrictions. It encodes the common concept of relation: an element $x$ is related to an element $y$ , if and only if the pair $(x, y)$ belongs to the set of ordered pairs that defines the binary relation. A binary relation is the most studied special case $n = 2$ of an $n$ -ary relation over sets $X 1, ..., X n$ , which is a subset of the Cartesian product

In mathematics, especially order theory, a partially ordered set formalizes and generalizes the intuitive concept of an ordering, sequencing, or arrangement of the elements of a set. A poset consists of a set together with a binary relation indicating that, for certain pairs of elements in the set, one of the elements precedes the other in the ordering. The relation itself is called a "partial order."

In mathematics, especially in order theory, a preorder or quasiorder is a binary relation that is reflexive and transitive. Preorders are more general than equivalence relations and (non-strict) partial orders, both of which are special cases of a preorder: an antisymmetric preorder is a partial order, and a symmetric preorder is an equivalence relation.

<span class="mw-page-title-main">Church–Rosser theorem</span>

In lambda calculus, the Church–Rosser theorem states that, when applying reduction rules to terms, the ordering in which the reductions are chosen does not make a difference to the eventual result.

In mathematics, a binary relation R on a set X is reflexive if it relates every element of X to itself.

In mathematics, a relation $R$ on a set $X$ is transitive if, for all elements $a$ , $b$ , $c$ in $X$ , whenever $R$ relates $a$ to $b$ and $b$ to $c$ , then $R$ also relates $a$ to $c$ . Each partial order as well as each equivalence relation needs to be transitive.

In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems. In their most basic form, they consist of a set of objects, plus relations on how to transform those objects.

This is a glossary of some terms used in various branches of mathematics that are related to the fields of order, lattice, and domain theory. Note that there is a structured list of order topics available as well. Other helpful resources might be the following overview articles:

The Knuth–Bendix completion algorithm is a semi-decision algorithm for transforming a set of equations into a confluent term rewriting system. When the algorithm succeeds, it effectively solves the word problem for the specified algebra.

<span class="mw-page-title-main">Weak ordering</span> Mathematical ranking of a set

In mathematics, especially order theory, a weak ordering is a mathematical formalization of the intuitive notion of a ranking of a set, some of whose members may be tied with each other. Weak orders are a generalization of totally ordered sets and are in turn generalized by partially ordered sets and preorders.

In theoretical computer science and mathematical logic a string rewriting system (SRS), historically called a semi-Thue system, is a rewriting system over strings from a alphabet. Given a binary relation $between fixed strings over the alphabet, called rewrite rules, denoted by, an SRS extends the rewriting relation to all strings in which the left- and right-hand side of the rules appear as substrings, that is, where,,, and are strings.$

In computer science, confluence is a property of rewriting systems, describing which terms in such a system can be rewritten in more than one way, to yield the same result. This article describes the properties in the most abstract setting of an abstract rewriting system.

In abstract rewriting, an object is in normal form if it cannot be rewritten any further, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all. Many properties of rewriting systems relate to normal forms.

In mathematics, a homogeneous relation over a set X is a binary relation over X and itself, i.e. it is a subset of the Cartesian product $X \times X$ . This is commonly phrased as "a relation on X" or "a (binary) relation over X". An example of a homogeneous relation is the relation of kinship, where the relation is over people.

In mathematics, a binary relation is a general concept that defines some relation between the elements of two sets. It is a generalization of the more commonly understood idea of a mathematical function, but with fewer restrictions. A binary relation over sets $X$ and $Y$ is a set of ordered pairs $(x, y)$ consisting of elements $x$ in $X$ and $y$ in $Y$ . It encodes the common concept of relation: an element $x$ is related to an element $y$ , if and only if the pair $(x, y)$ belongs to the set of ordered pairs that defines the binary relation. A binary relation is the most studied special case $n = 2$ of an $n$ -ary relation over sets $X 1, ..., X n$ , which is a subset of the Cartesian product $X 1 \times ... \times X n$ .

In mathematical logic and theoretical computer science, an abstract rewriting system is a formalism that captures the quintessential notion and properties of rewriting systems. In its simplest form, an ARS is simply a set together with a binary relation, traditionally denoted with $; this definition can be further refined if we index (label) subsets of the binary relation. Despite its simplicity, an ARS is sufficient to describe important properties of rewriting systems like normal forms, termination, and various notions of confluence.$

In mathematical logic, a term denotes a mathematical object while a formula denotes a mathematical fact. In particular, terms appear as components of a formula. This is analogous to natural language, where a noun phrase refers to an object and a whole sentence refers to a fact.

In rewriting, a reduction strategy or rewriting strategy is a relation specifying a rewrite for each object or term, compatible with a given reduction relation. Some authors use the term to refer to an evaluation strategy.

In theoretical computer science, in particular in automated theorem proving and term rewriting, the containment, or encompassment, preorder (≤) on the set of terms, is defined by

In theoretical computer science, in particular in term rewriting, a path ordering is a well-founded strict total order (>) on the set of all terms such that

References

Nachum Dershowitz; Jean-Pierre Jouannaud (1990). "Rewrite Systems". In Jan van Leeuwen (ed.). Formal Models and Semantics. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243–320. doi:10.1016/B978-0-444-88074-1.50011-1. ISBN 9780444880741.

1 2 Dershowitz, Jouannaud (1990), sect.2.1, p.251
1 2 3 Dershowitz, Jouannaud (1990), sect.5.1, p.270
↑ Dershowitz, Jouannaud (1990), sect.2.2, p.252
1 2 Dershowitz, Jouannaud (1990), sect.5.2, p.274
1 2 Dershowitz, Jouannaud (1990), sect.5.1, p.272
1 2 Dershowitz, Jouannaud (1990), sect.5.1, p.271
↑ David A. Plaisted (1978). A Recursively Defined Ordering for Proving Termination of Term Rewriting Systems (Technical report). Univ. of Illinois, Dept. of Comp. Sc. p. 52. R-78-943.
↑ N. Dershowitz (1982). "Orderings for Term-Rewriting Systems" (PDF). Theoret. Comput. Sci. 17 (3): 279–301. doi:10.1016/0304-3975(82)90026-3. S2CID 6070052. Here: p.287; the notions are named slightly different.

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.

[5] Parenthesized entries indicate inferred properties which are not part of the definition. For example, an irreflexive relation can't be reflexive (on a nonempty domain set).

[6] xcept all x_i are equal for all i beyond some n, for a reflexive relation

[7] Since x<y implies y<x, since the latter is an instance of the former, for variables x, y.

[9] .e. if $l i > r i$ for all i, where (>) is a reduction ordering; the system needn't have finitely many rules

[10] Since e.g. $a > b$ implied $g (a)> g (b)$ , meaning the second rewrite rule was not decreasing.

[12] .e. a ground-total reduction ordering

[14] Else, t|_p > t for some term t and position p, implying an infinite descending chain t > t[t]_p > t[t[t]_p]_p > ...^[6]^[7]

[15] .e. a simplification ordering

[16] The proof of this property is based on Higman's lemma, or, more generally, Kruskal's tree theorem.

[DJ90:251-1] 1 2 Dershowitz, Jouannaud (1990), sect.2.1, p.251

[DJ90:270-2] 1 2 3 Dershowitz, Jouannaud (1990), sect.5.1, p.270

[DJ90:252-3] Dershowitz, Jouannaud (1990), sect.2.2, p.252

[DJ90:274-4] 1 2 Dershowitz, Jouannaud (1990), sect.5.2, p.274

[DJ90:272-8] 1 2 Dershowitz, Jouannaud (1990), sect.5.1, p.272

[DJ90:271-11] 1 2 Dershowitz, Jouannaud (1990), sect.5.1, p.271

[13] David A. Plaisted (1978). A Recursively Defined Ordering for Proving Termination of Term Rewriting Systems (Technical report). Univ. of Illinois, Dept. of Comp. Sc. p. 52. R-78-943.

[17] N. Dershowitz (1982). "Orderings for Term-Rewriting Systems" (PDF). Theoret. Comput. Sci. 17 (3): 279–301. doi:10.1016/0304-3975(82)90026-3. S2CID 6070052. Here: p.287; the notions are named slightly different.

[1]

[2]

[3]

[4]

[note 1]

[note 2]

[note 3]

[5]

[note 4]

[note 5]

[6]

[note 6]

[note 7]

[note 8]

[note 9]

[8]

[7]