Intuitively, a term f(...) is bigger than any term g(...) built from terms si 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.
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.[2][3]
The latter variations include:
the multiset path ordering (mpo), originally called recursive path ordering (rpo)[4]
a combination of mpo and lpo, called recursive path ordering by Dershowitz, Jouannaud (1990)[6][7][8]
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.[7]
Formal definitionsedit
The multiset path ordering (>) can be defined as follows:[9]
O is continuous on relations, i.e. if R0, R1, R2, R3, ... is an infinite sequence of relations, then O(∪∞ i=0Ri) = ∪∞ i=0O(Ri).
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.
^Gerard Huet (May 1986). . 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
^ abN. Dershowitz, M. Okada (1988). "Proof-Theoretic Techniques for Term Rewriting Theory". Proc. 3rd IEEE Symp. on Logic in Computer Science(PDF). pp. 104–111.
^Mitsuhiro Okada, Adam Steele (1988). "Ordering Structures and the Knuth–Bendix Completion Algorithm". Proc. of the Allerton Conf. on Communication, Control, and Computing.
path, ordering, term, rewriting, lexicographic, path, ordering, redirects, here, dictionary, order, lexicographic, ordering, theoretical, computer, science, particular, term, rewriting, path, ordering, well, founded, strict, total, order, terms, such, that, wh. Lexicographic path ordering redirects here For the dictionary order see Lexicographic ordering In theoretical computer science in particular in term rewriting a path ordering is a well founded strict total order gt on the set of all terms such that f gt g s1 sn if f gt g and f gt si for i 1 n where gt 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 si 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 gt 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 gt a path ordering can be used since both x y z gt x y and x y z gt 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 1 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 lt g then s can dominate t only if one of s s subterms does If f gt 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 2 3 The latter variations include the multiset path ordering mpo originally called recursive path ordering rpo 4 the lexicographic path ordering lpo 5 a combination of mpo and lpo called recursive path ordering by Dershowitz Jouannaud 1990 6 7 8 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 f n 0 using Veblen s function for large countable ordinals 7 Formal definitions editThe multiset path ordering gt can be defined as follows 9 s f s1 sm gt t g t1 tn iff gt g and s gt tj for each j 1 n orsi t for some i 1 m orf g and s1 sm gt gt t1 tn where denotes the reflexive closure of the mpo gt s1 sm denotes the multiset of s s subterms similar for t and gt gt denotes the multiset extension of gt defined by s1 sm gt gt t1 tn if t1 tn can be obtained from s1 sm by deleting at least one element or by replacing an element by a multiset of strictly smaller w r t the mpo elements 10 More generally an order functional is a function O mapping an ordering to another one and satisfying the following properties 11 If gt is transitive then so is O gt If gt is irreflexive then so is O gt If s gt t then f s O gt f t O is continuous on relations i e if R0 R1 R2 R3 is an infinite sequence of relations then O i 0 Ri i 0 O Ri The multiset extension mapping gt above to gt gt above is one example of an order functional gt gt O gt Another order functional is the lexicographic extension leading to the lexicographic path ordering References edit N Dershowitz Termination 1995 p 207 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 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 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 S Kamin J J Levy 1980 Two Generalizations of the Recursive Path Ordering Technical report Univ of Illinois Urbana IL Kamin Levy 1980 a b 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 Mitsuhiro Okada Adam Steele 1988 Ordering Structures and the Knuth Bendix Completion Algorithm Proc of the Allerton Conf on Communication Control and Computing Huet 1986 sect 4 3 def 1 p 57 Huet 1986 sect 4 1 3 p 56 Huet 1986 sect 4 3 p 58 Retrieved from https en wikipedia org w index php title Path ordering term rewriting amp oldid 1167028707, wikipedia, wiki, book, books, library,
