Path ordering (term rewriting)

In <a href="/facts/Theoretical_computer_science/jSkGGuvy">theoretical computer science</a>, in particular in <a href="/facts/Term_rewriting/9PHlnnnJ">term rewriting</a>, a path ordering is a <a href="/facts/Well-founded/zyRRyJ4M">well-founded</a> <a href="/facts/Strict_total_order/xnTtmuYJ">strict total order</a> (>) on the set of all <a href="/facts/Term_(logic)/M0nXp7dH">terms</a> such that 

f(...) > g(s1,...,sn)   if   f .> g   and   f(...) > si for i=1,...,n,
where (.>) is a user-given <a href="/facts/Strict_total_order/xnTtmuYJ">total precedence order</a> on the set of all <a href="/facts/Term_(logic)/M0nXp7dH">function symbols</a>.
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 <a href="/facts/Structural_induction/cn6XIAAd">structural induction</a>, a term f(...) is bigger than any term containing only symbols smaller than f.
A path ordering is often used as <a href="/facts/Reduction_ordering/joLs3AYv">reduction ordering</a> in term rewriting, in particular in the <a href="/facts/Knuth%E2%80%93Bendix_completion_algorithm/cH66W8Rr">Knuth–Bendix completion algorithm</a>.
As an example, a term rewriting system for "<a href="/facts/Elementary_algebra/973nufT7">multiplying out</a>" mathematical expressions could contain a rule x*(y+z) → (x*y) + (x*z). In order to prove <a href="/facts/Termination_(term_rewriting)/9PHlnnnJ">termination</a>, a <a href="/facts/Reduction_ordering/joLs3AYv">reduction ordering</a> (>) 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 <a href="/facts/General_recursive_function/pQezUupS">general recursive functions</a>, for example a system for the <a href="/facts/Ackermann_function/WQNpCWHn">Ackermann function</a> may contain the rule A(a+, b+) → A(a, A(a+, b)), where b+ denotes the <a href="/facts/Successor_function/R1hhkSEG">successor</a> 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.

<ul><li>If f <. g, then s can dominate t only if one of s's subterms does.</li>
<li>If f .> g, then s dominates t if s dominates each of t's subterms.</li>
<li>If f = g, then the immediate <a href="/facts/Term_(logic)/M0nXp7dH">subterms</a> of s and t need to be compared recursively. Depending on the particular method, different variations of path orderings exist.</li></ul>
The latter variations include:

<ul><li>the multiset path ordering (mpo), originally called recursive path ordering (rpo)</li>
<li>the lexicographic path ordering (lpo)</li>
<li>a combination of mpo and lpo, called recursive path ordering by Dershowitz, Jouannaud (1990)</li></ul>
Dershowitz, Okada (1988) list more variants, and relate them to <a href="/facts/Wilhelm_Ackermann/8bPlUHSE">Ackermann</a>'s system of <a href="/facts/Ackermann_ordinal/QSxRdozk">ordinal notations</a>. In particular, an upper bound given on the order types of recursive path orderings with n function symbols is φ(n,0), using <a href="/facts/Veblen_function/XzaRJyjr">Veblen's function</a> for large countable ordinals.

Path ordering (term rewriting) open-in-new

Path ordering (term rewriting)