Rewrite order

From Wikipedia, the free encyclopedia
Jump to navigation Jump to search
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[edit]

  • 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 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 {l1::=r1,...,ln::=rn, ...} is terminating if its rules are subset of the strict part of a simplification ordering.[4][10]

Notes[edit]

  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 xi 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 li > ri 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[edit]

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. ^ a b c Dershowitz, Jouannaud (1990), sect.5.1, p.270
  3. ^ Dershowitz, Jouannaud (1990), sect.2.2, p.252
  4. ^ a b Dershowitz, Jouannaud (1990), sect.5.2, p.274
  5. ^ Dershowitz, Jouannaud (1990), sect.2.1, p.251
  6. ^ a b Dershowitz, Jouannaud (1990), sect.5.1, p.272
  7. ^ a b Dershowitz, Jouannaud (1990), sect.5.1, p.271
  8. ^ 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.
  9. ^ 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]
  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.
Retrieved from "https://en.wikipedia.org/w/index.php?title=Rewrite_order&oldid=779912705"