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.
As an example, a term rewriting system for "multiplying out" mathematical expressions could contain a rule x*(y+z) → (x*y) + (x*z).
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.
The latter variations include: 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.