1. Formal definitions

2. References

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

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.

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

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 ss subterms does.
• If f ^.> g, then s dominates t if s dominates each of ts subterms.
• If f = g, then the immediate subterms of s and t need to be compared recursively. Depending on the particular method, different variations of path orderings exist.^[1][2]

The latter variations include:

• the multiset path ordering (mpo), originally called recursive path ordering (rpo)^[3]
• the lexicographic path ordering (lpo)^[4]
• a combination of mpo and lpo, called recursive path ordering by Dershowitz, Jouannaud (1990)^[5][6][7]

Dershowitz, Okada (1988) list more variants, and relate them to Ackermann's system of ordinals.

Formal definitions

The multiset path ordering (>) can be defined as follows:^[8]

where

• (≥) denotes the reflexive closure of the mpo (>),
• { s₁,...,s_m } denotes the multiset of s’s subterms, similar for t, and
• (>>) denotes the multiset extension of (>), defined by { s₁,...,s_m } >> { t₁,...,t_n } if { t₁,...,t_n } can be obtained from { s₁,...,s_m }
  • by deleting at least one element, or
  • by replacing an element by a multiset of strictly smaller (w.r.t. the mpo) elements.^[9]

More generally, an order functional is a function O mapping an ordering to another one, and satisfying the following properties:^[10]

• If (>) is transitive, then so is O(>).
• If (>) is irreflexive, then so is O(>).
• If s > t, then f(...,s,...) O(>) f(...,t,...).
• O is continuous on relations, i.e. if R₀, R₁, R₂, R₃, ... is an infinite sequence of relations, then O(∪{{su|b=i=0|p=∞}} R_i) = ∪{{su|b=i=0|p=∞}} O(R_i).

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.

References

• Northern Amuzgo
• Northern anatolian conifer and deciduous forests
• Northern and eastern railway
• Northern Andes
• Northern and pacific junction railway
• Northern and Shell Media
• Northern and Southern Buddhism
• Northern and southern buddhism
• Northern and southern china
• Northern and Southern Courts period (disambiguation)
• Northern and Southern Courts period (Vietnam)
• Northern and Southern Kwakiutl
• Northern and southern vietnam
• Northern Appalachians Seismic Zone
• Northern Arc (disambiguation)
• Northern Arctic
• Northern Arctic Ecozone (CEC)
• Northern Arc (trade route)
• Northern Areas
• Northern Areas (Jammu and Kashmir)
• Northern Areas (Kashmir)
• Northern Areas Pakistan
• Northern Areas (Pakistan)
• Northern Arizona Food Bank
• Northern Arizona Lumberjacks