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 lr implies u[lσ]pu[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

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 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

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. 1 2 3 Dershowitz, Jouannaud (1990), sect.5.1, p.270
  3. Dershowitz, Jouannaud (1990), sect.2.2, p.252
  4. 1 2 Dershowitz, Jouannaud (1990), sect.5.2, p.274
  5. Dershowitz, Jouannaud (1990), sect.2.1, p.251
  6. 1 2 Dershowitz, Jouannaud (1990), sect.5.1, p.272
  7. 1 2 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.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.