Rewrite order

Rewriting s to t by a rule l::=r. If l and r are related by a rewrite relation, so are s and t. A simplifcation ordering always relates l and s, and similarly r and t.

In theoretical computer science, in particular in automated theorem proving and term rewriting, 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]p R u[y]p	Yes	Yes	Yes	Yes
closed under instantiation x R y implies xσ R yσ	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 x1 R x2 R x3 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.^[5]
• 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][6]}
• A term rewriting system {l₁::=r₁,...,l_n::=r_n, ...} is terminating if its rules are 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][7]}
• A ground-total and well-founded rewrite ordering^{[note 6]} necessarily contains the proper subterm relation on ground terms.^[8]
• Conversely, a rewrite ordering that contains the subterm relation^{[note 7]} is necessarily well-founded, when the set of function symbols is finite.^{[6][note 8]}
• A finite term rewriting system {l₁::=r₁,...,l_n::=r_n, ...} is terminating if its rules are subset of the strict part of a simplification ordering.^[4][10]

Notes

1. 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).
2. except all x_i are equal for all i beyond some n, for a reflexive relation
3. Since x<y implies y<x, since the latter is an instance of the former, for variables x, y.
4. i.e. if l_i > r_i for all i, where (>) is a reduction ordering; the system needn't have finitely many rules
5. Since e.g. a>b implied g(a)>g(b), meaning the second rewrite rule was not decreasing.
6. i.e. a ground-total reduction ordering
7. i.e. a simplification ordering
8. The proof of this property is based on Higman's lemma, or, more generally, Kruskal's tree theorem.

References

Nachum Dershowitz; Jean-Pierre Jouannaud (1990). Jan van Leeuwen, ed. Rewrite Systems. Handbook of Theoretical Computer Science. B. Elsevier. pp. 243–320.

1. Dershowitz, Jouannaud (1990), sect.2.1, p.251
2. Dershowitz, Jouannaud (1990), sect.5.1, p.270
3. Dershowitz, Jouannaud (1990), sect.2.2, p.252
4. Dershowitz, Jouannaud (1990), sect.5.2, p.274
5. Dershowitz, Jouannaud (1990), sect.2.1, p.251
6. Dershowitz, Jouannaud (1990), sect.5.1, p.272
7. Dershowitz, Jouannaud (1990), sect.5.1, p.271
8. 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 > ... ^[7][9]
9. 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.
10. N. Dershowitz (1982). "Orderings for Term-Rewriting Systems" (PDF). Theoret. Comput. Sci. 17 (3): 279––301. Here: p.287; the notions are named slightly different.