Path ordering (term rewriting)


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
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* → + . In order to prove termination, a reduction ordering must be found with respect to which the term x* is greater than the term +. 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* > x*y and x* > 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 list more variants, and relate them to Ackermann's system of ordinals.

Formal definitions

The multiset path ordering can be defined as follows:
where
More generally, an order functional is a function O mapping an ordering to another one, and satisfying the following properties:
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.