Login
Login

Rewrite order

File:Triangle diagram of rewrite rule application svg.svg

In theoretical computer science, in particular in automated reasoning about formal equations, reduction orderings are used to prevent endless loops. Rewrite orders, and, in turn, rewrite relations, are generalizations of this concept that have turned out to be useful in theoretical investigations.

Motivation

Intuitively, a reduction order R relates two terms s and t if t is properly "simpler" than s in some sense.

For example, simplification of terms may be a part of a computer algebra program, and may be using the rule set { x+0 → x , 0+x → x , x*0 → 0, 0*x → 0, x*1 → x , 1*x → x }. In order to prove impossibility of endless loops when simplifying a term using these rules, the reduction order defined by "sRt if term t is properly shorter than term s" can be used; applying any rule from the set will always properly shorten the term.

In contrast, to establish termination of "distributing-out" using the rule x*(y+z) → x*y+x*z, a more elaborate reduction order will be needed, since this rule may blow up the term size due to duplication of x. The theory of rewrite orders aims at helping to provide an appropriate order in such cases.

Formal definitions

Formally,

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, or rewrite preorder. If the latter (→) is moreover well-founded, it is called a reduction ordering,Dershowitz, Jouannaud (1990), sect.5.1, p.270 or a reduction preorder.

Given a binary relation R, its rewrite closure is the smallest rewrite relation containing R.Dershowitz, Jouannaud (1990), sect.2.2, p.252 A transitive and reflexive rewrite relation that contains the subterm ordering is called a simplification ordering.Dershowitz, Jouannaud (1990), sect.5.2, p.274

class="wikitable mw-collapsible mw-collapsed" style="float:right"

|+ {{nowrap|Overview of rewrite relations}}Parenthesized entries indicate inferred properties which are not part of the definition. For example, an irreflexive relation cannot be reflexive (on a nonempty domain set).

! 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

|

| align=center | (No)

| align=center | (No)

| {{yes}}

irreflexive
never x R x

|

| {{yes}}

| {{yes}}

| align=center | (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 ...except all xi are equal for all i beyond some n, for a reflexive relation

|

|

| {{yes}}

| align=center | (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.Dershowitz, Jouannaud (1990), sect.2.1, p.251
  • 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.Since x<y implies y<x, since the latter is an instance of the former, for variables x, y.Dershowitz, Jouannaud (1990), sect.5.1, p.272
  • A term rewriting system {{math|{{mset|1= l1::=r1,...,ln::=rn, ... }}}} is terminating if its rules are a subset of a reduction ordering.i.e. if {{math|li > ri}} for all i, where (>) is a reduction ordering; the system need not have finitely many rules
  • Conversely, for every terminating term rewriting system, the transitive closure of (::=) is a reduction ordering, which need not 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.Since e.g. {{math|a>b}} implied {{math|g(a)>g(b)}}, meaning the second rewrite rule was not decreasing.Dershowitz, Jouannaud (1990), sect.5.1, p.271
  • A ground-total and well-founded rewrite orderingi.e. a ground-total reduction ordering necessarily contains the proper subterm relation on ground terms.{{#tag:ref|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 > ...{{cite tech report| author=David A. Plaisted| title=A Recursively Defined Ordering for Proving Termination of Term Rewriting Systems| year=1978| number=R-78-943| pages=52| institution=Univ. of Illinois, Dept. of Comp. Sc.| url=https://archive.org/details/recursivelydefin943plai}}|group=note}}
  • Conversely, a rewrite ordering that contains the subterm relationi.e. a simplification ordering is necessarily well-founded, when the set of function symbols is finite.The proof of this property is based on Higman's lemma, or, more generally, Kruskal's tree theorem.
  • A finite term rewriting system {{math|{{mset|1= l1::=r1,...,ln::=rn, ... }}}} is terminating if its rules are subset of the strict part of a simplification ordering.{{cite journal | author=N. Dershowitz | title=Orderings for Term-Rewriting Systems | journal=Theoret. Comput. Sci. | volume=17 | number=3 | pages=279–301 | url=http://www.cs.tau.ac.il/~nachum/papers/Orderings4TRS.pdf | year=1982 | doi=10.1016/0304-3975(82)90026-3 | s2cid=6070052 }} Here: p.287; the notions are named slightly different.

Notes

{{Reflist|group=note}}

References

{{cite book| author1=Nachum Dershowitz |author2-link= Jean-Pierre Jouannaud|author2= Jean-Pierre Jouannaud| chapter=Rewrite Systems| title=Formal Models and Semantics| year=1990| volume=B| pages=243–320| publisher=Elsevier| editor=Jan van Leeuwen| editor-link=Jan van Leeuwen| series=Handbook of Theoretical Computer Science |doi=10.1016/B978-0-444-88074-1.50011-1 |author1-link= Nachum Dershowitz|isbn= 9780444880741}}

{{Reflist}}

Category:Rewriting systems

Category:Order theory