Menu
Home
People
Places
Arts
History
Plants & Animals
Science
Life & Culture
Technology
Reference.org
Path ordering (term rewriting)
open-in-new
<h2 id="formal-definitions">Formal definitions</h2> <p>The multiset path ordering (>) can be defined as follows:<a class="footnote-ref" id="fnref:10" href="#fn:10"><sup>10</sup></a> </p> <table><tbody><tr><td colspan="9"><i>s</i> = <i>f</i>(<i>s</i>1,...,<i>s</i><i>m</i>) > <i>t</i> = <i>g</i>(<i>t</i>1,...,<i>t</i><i>n</i>)</td><td>if</td></tr><tr><td><i>f</i></td><td>.></td><td><i>g</i></td><td>and</td><td><i>s</i></td><td>></td><td><i>t</i><i>j</i></td><td>for each</td><td><i>j</i>∈{1,...,<i>n</i>}, </td><td>or</td></tr><tr><td></td><td></td><td></td><td></td><td><i>s</i><i>i</i></td><td>≥</td><td><i>t</i></td><td>for some</td><td><i>i</i>∈{1,...,<i>m</i>},</td><td>or</td></tr><tr><td><i>f</i></td><td>=</td><td><i>g</i></td><td>and</td><td colspan="5">{ <i>s</i>1,...,<i>s</i><i>m</i> } >> { <i>t</i>1,...,<i>t</i><i>n</i> }</td></tr></tbody></table> <p>where </p> <ul><li>(≥) denotes the <a href="/facts/Reflexive_closure/wHmreKzK">reflexive closure</a> of the mpo (>),</li> <li>{ <i>s</i>1,...,<i>s</i><i>m</i> } denotes the <a href="/facts/Multiset/bPFJGMDo">multiset</a> of <i>s</i>’s subterms, similar for <i>t</i>, and</li> <li>(>>) denotes the multiset extension of (>), defined by { <i>s</i>1,...,<i>s</i><i>m</i> } >> { <i>t</i>1,...,<i>t</i><i>n</i> } if { <i>t</i>1,...,<i>t</i><i>n</i> } can be obtained from { <i>s</i>1,...,<i>s</i><i>m</i> } <ul><li>by deleting at least one element, or</li> <li>by replacing an element by a multiset of strictly smaller (w.r.t. the mpo) elements.<a class="footnote-ref" id="fnref:11" href="#fn:11"><sup>11</sup></a></li></ul></li></ul> <p>More generally, an order <a href="/facts/Higher-order_function/VjnjGbpt">functional</a> is a function <i>O</i> mapping an ordering to another one, and satisfying the following properties:<a class="footnote-ref" id="fnref:12" href="#fn:12"><sup>12</sup></a> </p> <ul><li>If (>) is <a href="/facts/Transitive_relation/9r90y50r">transitive</a>, then so is <i>O</i>(>).</li> <li>If (>) is <a href="/facts/Irreflexive/NzTytEg9">irreflexive</a>, then so is <i>O</i>(>).</li> <li>If <i>s</i> > <i>t</i>, then <i>f</i>(...,<i>s</i>,...) <i>O</i>(>) <i>f</i>(...,<i>t</i>,...).</li> <li><i>O</i> is <a href="/facts/Continuous_function_(set_theory)/oBwh40rV">continuous</a> on relations, i.e. if <i>R</i>0, <i>R</i>1, <i>R</i>2, <i>R</i>3, ... is an infinite sequence of relations, then <i>O</i>(∪∞<i>i</i>=0 <i>R</i><i>i</i>) = ∪∞<i>i</i>=0 <i>O</i>(<i>R</i><i>i</i>).</li></ul> <p>The multiset extension, mapping (>) above to (>>) above is one example of an order functional: (>>)=<i>O</i>(>). Another order functional is the <a href="/facts/Lexicographical_order/xQANy8Br">lexicographic</a> extension, leading to the lexicographic path ordering. </p> <h2 id="references">References</h2> <ol> <li id="fn:1"><p>N. Dershowitz, "Termination" (1995). p. 207 <a href="https://www.semanticscholar.org/paper/T-E-R-M-I-N-a-T-I-O-N-*-Dershowitz/53272b7f1535a9a0f665026393518c0d738a14fe" target="_blank">https://www.semanticscholar.org/paper/T-E-R-M-I-N-a-T-I-O-N-*-Dershowitz/53272b7f1535a9a0f665026393518c0d738a14fe</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></p></li> <li id="fn:2"><p>Nachum Dershowitz, Jean-Pierre Jouannaud (1990). Jan van Leeuwen (ed.). Rewrite Systems. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243–320. Here: sect.5.3, p.275 <a href="/wiki/Nachum_Dershowitz" target="_blank">/wiki/Nachum_Dershowitz</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></p></li> <li id="fn:3"><p>Gerard Huet (May 1986). Formal Structures for Computation and Deduction. International Summer School on Logic of Programming and Calculi of Discrete Design. Archived from the original on 2014-07-14. Here: chapter 4, p.55-64 <a href="https://web.archive.org/web/20140714171331/http://yquem.inria.fr/~huet/PUBLIC/Formal_Structures.ps.gz" target="_blank">https://web.archive.org/web/20140714171331/http://yquem.inria.fr/~huet/PUBLIC/Formal_Structures.ps.gz</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></p></li> <li id="fn:4"><p>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. <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:4" class="footnote-back-ref">↩</a></p></li> <li id="fn:5"><p>S. Kamin, J.-J. Levy (1980). Two Generalizations of the Recursive Path Ordering (Technical report). Univ. of Illinois, Urbana/IL. <a href="#fnref:5" class="footnote-back-ref">↩</a></p></li> <li id="fn:6"><p>Kamin, Levy (1980) <a href="#fnref:6" class="footnote-back-ref">↩</a></p></li> <li id="fn:7"><p>N. Dershowitz, M. Okada (1988). "Proof-Theoretic Techniques for Term Rewriting Theory". Proc. 3rd IEEE Symp. on Logic in Computer Science (PDF). pp. 104–111. <a href="http://www.cs.tau.ac.il/~nachum/papers/ProofTheoretic.pdf" target="_blank">http://www.cs.tau.ac.il/~nachum/papers/ProofTheoretic.pdf</a> <a href="#fnref:7" class="footnote-back-ref">↩</a></p></li> <li id="fn:8"><p>Mitsuhiro Okada, Adam Steele (1988). "Ordering Structures and the Knuth–Bendix Completion Algorithm". Proc. of the Allerton Conf. on Communication, Control, and Computing. <a href="#fnref:8" class="footnote-back-ref">↩</a></p></li> <li id="fn:9"><p>N. Dershowitz, M. Okada (1988). "Proof-Theoretic Techniques for Term Rewriting Theory". Proc. 3rd IEEE Symp. on Logic in Computer Science (PDF). pp. 104–111. <a href="http://www.cs.tau.ac.il/~nachum/papers/ProofTheoretic.pdf" target="_blank">http://www.cs.tau.ac.il/~nachum/papers/ProofTheoretic.pdf</a> <a href="#fnref:9" class="footnote-back-ref">↩</a></p></li> <li id="fn:10"><p>Huet (1986), sect.4.3, def.1, p.57 <a href="#fnref:10" class="footnote-back-ref">↩</a></p></li> <li id="fn:11"><p>Huet (1986), sect.4.1.3, p.56 <a href="#fnref:11" class="footnote-back-ref">↩</a></p></li> <li id="fn:12"><p>Huet (1986), sect.4.3, p. 58 <a href="#fnref:12" class="footnote-back-ref">↩</a></p></li> </ol>