Rewrite order

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 x₁ R x₂ R x₃ 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 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]}^[7]
A ground-total and well-founded rewrite ordering^{[note 6]} necessarily contains the proper subterm relation on ground terms.^[9]
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 1 ::= r 1,..., l n ::= r n, ...}$ is terminating if its rules are subset of the strict part of a simplification ordering.^[4]^[10]

^ 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
^ i.e. a simplification ordering
^ The proof of this property is based on Higman's lemma, or, more generally, Kruskal's tree theorem.

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

^ Dershowitz, Jouannaud (1990), sect.2.1, p.251
^ ^a ^b ^c Dershowitz, Jouannaud (1990), sect.5.1, p.270
^ Dershowitz, Jouannaud (1990), sect.2.2, p.252
^ ^a ^b Dershowitz, Jouannaud (1990), sect.5.2, p.274
^ Dershowitz, Jouannaud (1990), sect.2.1, p.251
^ ^a ^b Dershowitz, Jouannaud (1990), sect.5.1, p.272
^ ^a ^b 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.
^ 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]^[8]
^ 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.

This computer science article is a stub. You can help Wikipedia by expanding it.