Rewrite order

<h2 id="motivation">Motivation</h2>
Intuitively, a reduction order R relates two <a href="/facts/Term_(logic)/M0nXp7dH">terms</a> s and t if t is properly "simpler" than s in some sense.
For example, simplification of terms may be a part of a <a href="/facts/Computer_algebra/hjun1KAX">computer algebra</a> 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.

<h2 id="formal-definitions">Formal definitions</h2>
Formally,
a <a href="/facts/Binary_relation/r9BwGgaK">binary relation</a> (→) on the set of <a href="/facts/Term_(logic)/M0nXp7dH">terms</a> is called a rewrite relation if it is <a href="/facts/Closure_(mathematics)/Ct6r2fJz">closed</a> under <a href="/facts/Context_(term_rewriting)/M0nXp7dH">contextual embedding</a> and under <a href="/facts/Substitution_(logic)/xMGFYd1k">instantiation</a>; formally: if l→r implies u<a href="/facts/Term_(logic)/M0nXp7dH">[</a>l<a href="/facts/Substitution_(logic)/xMGFYd1k">σ</a>]p→u[rσ]p for all terms l, r, u, each path p of u, and each <a href="/facts/Substitution_(logic)/xMGFYd1k">substitution</a> σ. If (→) is also <a href="/facts/Irreflexive_relation/NzTytEg9">irreflexive</a> and <a href="/facts/Transitive_relation/9r90y50r">transitive</a>, then it is called a rewrite ordering,<a class="footnote-ref" id="fnref:1" href="#fn:1">1</a> or rewrite <a href="/facts/Preorder/uubzHSWm">preorder</a>. If the latter (→) is moreover <a href="/facts/Well-founded/zyRRyJ4M">well-founded</a>, it is called a reduction ordering,<a class="footnote-ref" id="fnref:2" href="#fn:2">2</a> or a reduction preorder.
Given a binary relation R, its rewrite <a href="/facts/Closure_(mathematics)/Ct6r2fJz">closure</a> is the smallest rewrite relation containing R.<a class="footnote-ref" id="fnref:3" href="#fn:3">3</a> A transitive and reflexive rewrite relation that contains the <a href="/facts/Term_(logic)/M0nXp7dH">subterm</a> ordering is called a simplification ordering.<a class="footnote-ref" id="fnref:4" href="#fn:4">4</a>

Overview of rewrite relations<a class="footnote-ref" id="fnref:5" href="#fn:5">5</a><table><tbody><tr><th></th><th>rewriterelation</th><th>rewriteorder</th><th>reductionorder</th><th>simplificationorder</th></tr><tr><td>closed under <a href="/facts/Term_(logic)/M0nXp7dH">context</a>x R y implies u<a href="/facts/Term_(logic)/M0nXp7dH">[</a>x]p R u[y]p</td><td>Yes</td><td>Yes</td><td>Yes</td><td>Yes</td></tr><tr><td>closed under <a href="/facts/Substitution_(logic)/xMGFYd1k">instantiation</a>x R y implies x<a href="/facts/Substitution_(logic)/xMGFYd1k">σ</a> R yσ</td><td>Yes</td><td>Yes</td><td>Yes</td><td>Yes</td></tr><tr><td>contains <a href="/facts/Term_(logic)/M0nXp7dH">subterm</a> relationy <a href="/facts/Term_(logic)/M0nXp7dH">subterm</a> of x implies x R y</td><td></td><td></td><td></td><td>Yes</td></tr><tr><td><a href="/facts/Reflexive_relation/NzTytEg9">reflexive</a>always x R x</td><td></td><td>(No)</td><td>(No)</td><td>Yes</td></tr><tr><td><a href="/facts/Irreflexive_relation/NzTytEg9">irreflexive</a>never x R x</td><td></td><td>Yes</td><td>Yes</td><td>(No)</td></tr><tr><td><a href="/facts/Transitive_relation/9r90y50r">transitive</a>x R y and y R z implies x R z</td><td></td><td>Yes</td><td>Yes</td><td>Yes</td></tr><tr><td><a href="/facts/Well-founded/zyRRyJ4M">well-founded</a>no infinite chain x1 R x2 R x3 R ...<a class="footnote-ref" id="fnref:6" href="#fn:6">6</a></td><td></td><td></td><td>Yes</td><td>(Yes)</td></tr></tbody></table>
<h2 id="properties">Properties</h2>
<ul><li>The <a href="/facts/Converse_relation/EVGlRSz7">converse</a>, the <a href="/facts/Symmetric_closure/HLYd9c8W">symmetric closure</a>, the <a href="/facts/Reflexive_closure/wHmreKzK">reflexive closure</a>, and the <a href="/facts/Transitive_closure/HEtgYGM4">transitive closure</a> of a rewrite relation is again a rewrite relation, as are the union and the intersection of two rewrite relations.<a class="footnote-ref" id="fnref:7" href="#fn:7">7</a></li>
<li>The converse of a rewrite order is again a rewrite order.</li>
<li>While rewrite orders exist that are total on the set of <a href="/facts/Term_(logic)/M0nXp7dH">ground terms</a> ("ground-total" for short), no rewrite order can be total on the set of <a href="/facts/Term_(logic)/M0nXp7dH">all terms</a>.<a class="footnote-ref" id="fnref:8" href="#fn:8">8</a><a class="footnote-ref" id="fnref:9" href="#fn:9">9</a></li>
<li>A <a href="/facts/Rewriting/9PHlnnnJ">term rewriting system</a> {l1::=r1,...,ln::=rn, ...} is <a href="/facts/Termination_(rewriting)/9PHlnnnJ">terminating</a> if its rules are a subset of a reduction ordering.<a class="footnote-ref" id="fnref:10" href="#fn:10">10</a><a class="footnote-ref" id="fnref:11" href="#fn:11">11</a></li>
<li>Conversely, for every terminating term rewriting system, the <a href="/facts/Transitive_closure/HEtgYGM4">transitive closure</a> of (::=) is a reduction ordering,<a class="footnote-ref" id="fnref:12" href="#fn:12">12</a> 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.<a class="footnote-ref" id="fnref:13" href="#fn:13">13</a><a class="footnote-ref" id="fnref:14" href="#fn:14">14</a></li>
<li>A ground-total and well-founded rewrite ordering<a class="footnote-ref" id="fnref:15" href="#fn:15">15</a> necessarily contains the <a href="/facts/Term_(logic)/M0nXp7dH">proper subterm</a> relation on ground terms.<a class="footnote-ref" id="fnref:16" href="#fn:16">16</a></li>
<li>Conversely, a rewrite ordering that contains the subterm relation<a class="footnote-ref" id="fnref:17" href="#fn:17">17</a> is necessarily well-founded, when the set of function symbols is finite.<a class="footnote-ref" id="fnref:18" href="#fn:18">18</a><a class="footnote-ref" id="fnref:19" href="#fn:19">19</a></li>
<li>A finite term rewriting system {l1::=r1,...,ln::=rn, ...} is terminating if its rules are subset of the strict part of a simplification ordering.<a class="footnote-ref" id="fnref:20" href="#fn:20">20</a><a class="footnote-ref" id="fnref:21" href="#fn:21">21</a></li></ul>
<h2 id="notes">Notes</h2>

<a href="/facts/Nachum_Dershowitz/WyyUeW3s">Nachum Dershowitz</a>; <a href="/facts/Jean-Pierre_Jouannaud/aF4qbjRu">Jean-Pierre Jouannaud</a> (1990). "Rewrite Systems". In <a href="/facts/Jan_van_Leeuwen/80Kmownr">Jan van Leeuwen</a> (ed.). Formal Models and Semantics. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243–320. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1016%2FB978-0-444-88074-1.50011-1">10.1016/B978-0-444-88074-1.50011-1</a>. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 9780444880741.

<h2 id="references">References</h2>

<ol>
<li id="fn:1">Dershowitz, Jouannaud (1990), sect.2.1, p.251 <a href="#fnref:1" class="footnote-back-ref">↩</a></li>
<li id="fn:2">Dershowitz, Jouannaud (1990), sect.5.1, p.270 <a href="#fnref:2" class="footnote-back-ref">↩</a></li>
<li id="fn:3">Dershowitz, Jouannaud (1990), sect.2.2, p.252 <a href="#fnref:3" class="footnote-back-ref">↩</a></li>
<li id="fn:4">Dershowitz, Jouannaud (1990), sect.5.2, p.274 <a href="#fnref:4" class="footnote-back-ref">↩</a></li>
<li id="fn:5">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). <a href="#fnref:5" class="footnote-back-ref">↩</a></li>
<li id="fn:6">except all xi are equal for all i beyond some n, for a reflexive relation <a href="#fnref:6" class="footnote-back-ref">↩</a></li>
<li id="fn:7">Dershowitz, Jouannaud (1990), sect.2.1, p.251 <a href="#fnref:7" class="footnote-back-ref">↩</a></li>
<li id="fn:8">Since x<y implies y<x, since the latter is an instance of the former, for variables x, y. <a href="#fnref:8" class="footnote-back-ref">↩</a></li>
<li id="fn:9">Dershowitz, Jouannaud (1990), sect.5.1, p.272 <a href="#fnref:9" class="footnote-back-ref">↩</a></li>
<li id="fn:10">i.e. if li > ri for all i, where (>) is a reduction ordering; the system need not have finitely many rules <a href="#fnref:10" class="footnote-back-ref">↩</a></li>
<li id="fn:11">Dershowitz, Jouannaud (1990), sect.5.1, p.270 <a href="#fnref:11" class="footnote-back-ref">↩</a></li>
<li id="fn:12">Dershowitz, Jouannaud (1990), sect.5.1, p.270 <a href="#fnref:12" class="footnote-back-ref">↩</a></li>
<li id="fn:13">Since e.g. a>b implied g(a)>g(b), meaning the second rewrite rule was not decreasing. <a href="#fnref:13" class="footnote-back-ref">↩</a></li>
<li id="fn:14">Dershowitz, Jouannaud (1990), sect.5.1, p.271 <a href="#fnref:14" class="footnote-back-ref">↩</a></li>
<li id="fn:15">i.e. a ground-total reduction ordering <a href="#fnref:15" class="footnote-back-ref">↩</a></li>
<li id="fn:16">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 > ...[6][7] <a href="#fnref:16" class="footnote-back-ref">↩</a></li>
<li id="fn:17">i.e. a simplification ordering <a href="#fnref:17" class="footnote-back-ref">↩</a></li>
<li id="fn:18">Dershowitz, Jouannaud (1990), sect.5.1, p.272 <a href="#fnref:18" class="footnote-back-ref">↩</a></li>
<li id="fn:19">The proof of this property is based on Higman's lemma, or, more generally, Kruskal's tree theorem. <a href="/wiki/Higman%27s_lemma" target="_blank">/wiki/Higman%27s_lemma</a> <a href="#fnref:19" class="footnote-back-ref">↩</a></li>
<li id="fn:20">Dershowitz, Jouannaud (1990), sect.5.2, p.274 <a href="#fnref:20" class="footnote-back-ref">↩</a></li>
<li id="fn:21">N. Dershowitz (1982). "Orderings for Term-Rewriting Systems" (PDF). Theoret. Comput. Sci. 17 (3): 279–301. doi:10.1016/0304-3975(82)90026-3. S2CID 6070052. Here: p.287; the notions are named slightly different. <a href="http://www.cs.tau.ac.il/~nachum/papers/Orderings4TRS.pdf" target="_blank">http://www.cs.tau.ac.il/~nachum/papers/Orderings4TRS.pdf</a> <a href="#fnref:21" class="footnote-back-ref">↩</a></li>
</ol>

Rewrite order open-in-new

Rewrite order