Path ordering (term rewriting)

Short description: Total order in computer science

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 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)),[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 <. 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]
* 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 φ(n,0), using Veblen's function for large countable ordinals.[7]

## Formal definitions

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

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

* (≥) denotes the reflexive closure of the mpo (>),
* { s1,...,sm } denotes the multiset of s’s subterms, similar for t, and
* (>>) denotes the multiset extension of (>), defined by { s1,...,sm } >> { 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 (>) 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 R0, R1, R2, R3, ... is an infinite sequence of relations, then O(∪∞i=0 Ri) = ∪∞i=0 O(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.

## References

1. ↑ N. Dershowitz, "Termination" (1995). p. 207
2. ↑ 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
3. ↑ Gerard Huet (May 1986). Formal Structures for Computation and Deduction. International Summer School on Logic of Programming and Calculi of Discrete Design. http://yquem.inria.fr/~huet/PUBLIC/Formal_Structures.ps.gz. Here: chapter 4, p.55-64
4. ↑ N. Dershowitz (1982). "Orderings for Term-Rewriting Systems". Theoret. Comput. Sci. 17 (3): 279–301. doi:10.1016/0304-3975(82)90026-3. http://www.cs.tau.ac.il/~nachum/papers/Orderings4TRS.pdf.
5. ↑ S. Kamin, J.-J. Levy (1980). Two Generalizations of the Recursive Path Ordering (Technical report). Univ. of Illinois, Urbana/IL.
6. ↑ Kamin, Levy (1980)
7. ↑ 7.0 7.1 N. Dershowitz, M. Okada (1988). "Proof-Theoretic Techniques for Term Rewriting Theory". Proc. 3rd IEEE Symp. on Logic in Computer Science. pp. 104–111. http://www.cs.tau.ac.il/~nachum/papers/ProofTheoretic.pdf.
8. ↑ Mitsuhiro Okada, Adam Steele (1988). "Ordering Structures and the Knuth–Bendix Completion Algorithm". Proc. of the Allerton Conf. on Communication, Control, and Computing.
9. ↑ Huet (1986), sect.4.3, def.1, p.57
10. ↑ Huet (1986), sect.4.1.3, p.56
11. ↑ Huet (1986), sect.4.3, p. 58

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/Path ordering (term rewriting). Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=Path_ordering_(term_rewriting)&oldid=211857"