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*(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.