Path ordering (term rewriting)

"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 (>) on the set of all terms such that

f(...) > g(s1,...,sn)   if   f .> g   and   f(...) > si 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 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 less function symbols and less 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.

The latter variations include:

Dershowitz, Okada (1988) list more variants, and relate them to Ackermann's system of ordinals.

Formal definitions

The multiset path ordering (>) can be defined as follows:[8]

s = f(s1,...,sm) > t = g(t1,...,tn) if
f .> g and s > tj for each j∈{1,...,n},     or
si t for some i∈{1,...,m}, or
f = g and { s1,...,sm } >> { t1,...,tn }

where

More generally, an order functional is a function O mapping an ordering to another one, and satisfying the following properties:[10]

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

  1. Nachum Dershowitz, Jean-Pierre Jouannaud (1990). Jan van Leeuwen, ed. Rewrite Systems. Handbook of Theoretical Computer Science B. Elsevier. pp. 243–320. Here: sect.5.3, p.275
  2. Gerard Huet (May 1986). Formal Structures for Computation and Deduction. International Summer School on Logic of Programming and Calculi of Discrete Design. Here: chapter 4, p.55-64
  3. N. Dershowitz (1982). "Orderings for Term-Rewriting Systems" (PDF). Theoret. Comput. Sci. 17 (3): 279–301.
  4. S. Kamin, J.-J. Levy (1980). Two Generalizations of the Recursive Path Ordering (Technical report). Univ. of Illinois, Urbana/IL.
  5. Kamin, Levy (1980)
  6. 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.
  7. Mitsuhiro Okada, Adam Steele (1988). "Ordering Structures and the Knuth–Bendix Completion Algorithm". Proc. of the Allerton Conf. on Communication, Control, and Computing.
  8. Huet (1986), sect.4.3, def.1, p.57
  9. Huet (1986), sect.4.1.3, p.56
  10. Huet (1986), sect.4.3, p. 58
This article is issued from Wikipedia - version of the Thursday, September 25, 2014. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.