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 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 { l1::=r1,...,ln::=rn, ... } 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 { l1::=r1,...,ln::=rn } is terminating if its rules are subset of the strict part of a simplification ordering.[4][10]
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 xi 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 li > ri 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.
References
Nachum Dershowitz; Jean-Pierre Jouannaud (1990). Jan van Leeuwen, ed. Rewrite Systems. Handbook of Theoretical Computer Science B. Elsevier. pp. 243–320.
- ↑ Dershowitz, Jouannaud (1990), sect.2.1, p.251
- ↑ 2.0 2.1 2.2 Dershowitz, Jouannaud (1990), sect.5.1, p.270
- ↑ Dershowitz, Jouannaud (1990), sect.2.2, p.252
- ↑ 4.0 4.1 Dershowitz, Jouannaud (1990), sect.5.2, p.274
- ↑ Dershowitz, Jouannaud (1990), sect.2.1, p.251
- ↑ 6.0 6.1 Dershowitz, Jouannaud (1990), sect.5.1, p.272
- ↑ 7.0 7.1 Dershowitz, Jouannaud (1990), sect.5.1, p.271
- ↑ 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]
- ↑ 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". Theoret. Comput. Sci. 17 (3): 279––301. Here: p.287; the notions are named slightly different.