Path ordering (term rewriting)
In theoretical computer science, in particular in term rewriting, a path ordering is a strict 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 less function symbols and less variables than the latter, respectively. 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.[1]
The latter variations include:
- the multiset path ordering (mpo), originally called recursive path ordering (rpo)[2]
- the lexicographic path ordering (lpo)[3]
- a combination of mpo and lpo, called recursive path ordering by Dershowitz, Jouannaud (1990)[4][5][6]
Dershowitz, Okada (1988) list more variants, and relate them to Ackermann's system of ordinals.
References
- ^ N. Dershowitz, J.-P. 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
- ^ N. Dershowitz (1982). "Orderings for Term-Rewriting Systems" (PDF). Theoret. Comput. Sci. 17 (3): 279–301.
- ^ S. Kamin, J.-J. Levy (1980). Two Generalizations of the Recursive Path Ordering (Technical report). Univ. of Illinois, Urbana/IL.
- ^ Kamin, Levy (1980)
- ^ 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.
 | This computer science article is a stub. You can help Wikipedia by expanding it. |