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(s₁,...,s_n)   if   f ^.> g   and   f(...) > s_i 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 s_i 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.

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 methode, different variations of path orderings exist.

A path ordering is often used as reduction ordering in term rewriting, in particular in the Knuth-Bendix completion algorithm.