Path ordering (term rewriting)

{{Short description|Total order in computer science}} {{redirect|Lexicographic path ordering|the dictionary order|Lexicographic ordering}} In theoretical computer science, in particular in term rewriting, a '''path ordering''' is a well-founded strict total order (>) on the set of all terms such that :''f''(...) > ''g''(''s''1,...,''s''''n'')   if   ''f'' .> ''g''   and   ''f''(...) > ''s''''i'' for ''i''=1,...,''n'', where (.>) is a user-given total precedence order on the set of all function symbols.

Intuitively, a term ''f''(...) is bigger than any term ''g''(...) built from terms ''s''''i'' smaller than ''f''(...) using a lower-precedence root symbol ''g''. In particular, by structural induction, a term ''f''(...) is bigger than any term containing only symbols smaller than ''f''.

A path ordering is often used as reduction ordering in term rewriting, in particular in the Knuth–Bendix completion algorithm. As an example, a term rewriting system for "multiplying out" mathematical expressions could contain a rule ''x''*(''y''+''z'') → (''x''*''y'') + (''x''*''z''). In order to prove termination, a reduction ordering (>) must be found with respect to which the term ''x''*(''y''+''z'') is greater than the term (''x''*''y'')+(''x''*''z''). This is not trivial, since the former term contains both fewer function symbols and fewer variables than the latter. However, setting the precedence (*) .> (+), a path ordering can be used, since both ''x''*(''y''+''z'') > ''x''*''y'' and ''x''*(''y''+''z'') > ''x''*''z'' is easy to achieve.

There may also be systems for certain general recursive functions, for example a system for the Ackermann function may contain the rule A(''a''+, ''b''+) → A(''a'', A(''a''+, ''b'')),<ref>N. Dershowitz, "[https://www.semanticscholar.org/paper/T-E-R-M-I-N-a-T-I-O-N-*-Dershowitz/53272b7f1535a9a0f665026393518c0d738a14fe Termination]" (1995). p. 207</ref> where ''b''+ denotes the successor of ''b''.

Given two terms ''s'' and ''t'', with a root symbol ''f'' and ''g'', respectively, to decide their relation their root symbols are compared first. * If ''f'' <. ''g'', then ''s'' can dominate ''t'' only if one of ''s'''s subterms does. * If ''f'' .> ''g'', then ''s'' dominates ''t'' if ''s'' dominates each of ''t'''s subterms. * If ''f'' = ''g'', then the immediate subterms of ''s'' and ''t'' need to be compared recursively. Depending on the particular method, different variations of path orderings exist.<ref>{{cite book| author=Nachum Dershowitz, Jean-Pierre Jouannaud| title=Rewrite Systems| year=1990| volume=B| pages=243–320| publisher=Elsevier| editor=Jan van Leeuwen| series=Handbook of Theoretical Computer Science}} Here: sect.5.3, p.275</ref><ref>{{cite book| author=Gerard Huet| title=Formal Structures for Computation and Deduction| date=May 1986| series=International Summer School on Logic of Programming and Calculi of Discrete Design| url=http://yquem.inria.fr/~huet/PUBLIC/Formal_Structures.ps.gz| url-status=dead| archive-url=https://web.archive.org/web/20140714171331/http://yquem.inria.fr/~huet/PUBLIC/Formal_Structures.ps.gz| archive-date=2014-07-14}} Here: chapter 4, p.55-64</ref> The latter variations include: * the '''multiset path ordering''' ('''mpo'''), originally called '''recursive path ordering''' ('''rpo''')<ref>{{cite journal| author=N. Dershowitz| title=Orderings for Term-Rewriting Systems| journal=Theoret. Comput. Sci.| year=1982| volume=17| number=3| pages=279–301| doi=10.1016/0304-3975(82)90026-3| s2cid=6070052| url=http://www.cs.tau.ac.il/~nachum/papers/Orderings4TRS.pdf}}</ref> * the '''lexicographic path ordering''' ('''lpo''')<ref>{{cite tech report| author=S. Kamin, J.-J. Levy| title=Two Generalizations of the Recursive Path Ordering| year=1980| institution=Univ. of Illinois, Urbana/IL}}</ref> * a combination of mpo and lpo, called '''recursive path ordering''' by Dershowitz, Jouannaud (1990)<ref>Kamin, Levy (1980)</ref><ref name=":0">{{cite book| author=N. Dershowitz, M. Okada| chapter=Proof-Theoretic Techniques for Term Rewriting Theory| title=Proc. 3rd IEEE Symp. on Logic in Computer Science| year=1988| pages=104–111| url=http://www.cs.tau.ac.il/~nachum/papers/ProofTheoretic.pdf}}</ref><ref>{{cite book| author=Mitsuhiro Okada, Adam Steele| chapter=Ordering Structures and the Knuth–Bendix Completion Algorithm| title=Proc. of the Allerton Conf. on Communication, Control, and Computing| year=1988}}</ref> Dershowitz, Okada (1988) list more variants, and relate them to Ackermann's system of ordinal notations. In particular, an upper bound given on the order types of recursive path orderings with ''n'' function symbols is φ(''n'',0), using Veblen's function for large countable ordinals.<ref name=":0" />

==Formal definitions==

The '''multiset path ordering''' (>) can be defined as follows:<ref>Huet (1986), sect.4.3, def.1, p.57</ref>

{| |- | colspan=9 | ''s'' = ''f''(''s''1,...,''s''''m'') > ''t'' = ''g''(''t''1,...,''t''''n'') | if |- | ''f'' | .> | ''g'' | and | ''s'' | > | ''t''''j'' | for each | ''j''∈{1,...,''n''},     | or |- | | | | | ''s''''i'' | ≥ | ''t'' | for some | ''i''∈{1,...,''m''}, | or |- | ''f'' | = | ''g'' | and | colspan=5 | { ''s''1,...,''s''''m'' } >> { ''t''1,...,''t''''n'' } |}

where * (≥) denotes the reflexive closure of the mpo (>), * { ''s''1,...,''s''''m'' } denotes the multiset of ''s''’s subterms, similar for ''t'', and * (>>) denotes the multiset extension of (>), defined by { ''s''1,...,''s''''m'' } >> { ''t''1,...,''t''''n'' } if { ''t''1,...,''t''''n'' } can be obtained from { ''s''1,...,''s''''m'' } ** by deleting at least one element, or ** by replacing an element by a multiset of strictly smaller (w.r.t. the mpo) elements.<ref>Huet (1986), sect.4.1.3, p.56</ref>

More generally, an '''order functional''' is a function ''O'' mapping an ordering to another one, and satisfying the following properties:<ref>Huet (1986), sect.4.3, p. 58</ref> * If (>) is transitive, then so is ''O''(>). * If (>) is irreflexive, then so is ''O''(>). * If ''s'' > ''t'', then ''f''(...,''s'',...) ''O''(>) ''f''(...,''t'',...). * ''O'' is continuous on relations, i.e. if ''R''0, ''R''1, ''R''2, ''R''3, ... is an infinite sequence of relations, then ''O''(∪{{su|b=''i''=0|p=∞}} ''R''''i'') = ∪{{su|b=''i''=0|p=∞}} ''O''(''R''''i'').

The multiset extension, mapping (>) above to (>>) above is one example of an order functional: (>>)=''O''(>). Another order functional is the lexicographic extension, leading to the '''lexicographic path ordering'''.

==References== {{reflist}}

Category:Rewriting systems Category:Order theory