A strict order 
on the set of terms of a term
rewriting system is called a reduction order if
1. The set of terms is well ordered with respect to 
,
that is, all its nonempty subsets contain their least elements,
2. This order is compatible with functions (operations) of the system, i.e.,
and
3. For any substitution 
(cf. unification), 
.
If 
holds for every rewriting rule 
, then this term rewriting system is finitely
terminating.
See also
Church-Rosser Property, Confluent, Critical Pair, Knuth-Bendix Completion Algorithm, Term Rewriting System
This entry contributed by Alex Sakharov (author's link)
Explore with Wolfram|Alpha
References
Baader, F. and Nipkow, T. Term Rewriting and All That. Cambridge, England: Cambridge University Press, 1999.Wolfram, S. A New Kind of Science. Champaign, IL: Wolfram Media, p. 1037, 2002.
Referenced on Wolfram|Alpha
Cite this as:
Sakharov, Alex. "Reduction Order." From MathWorld--A Wolfram Resource, created by Eric W. Weisstein. https://mathworld.wolfram.com/ReductionOrder.html