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
Reduction Order
Cite this as:
Sakharov, Alex. "Reduction Order." From MathWorld--A Wolfram Web Resource, created by Eric
W. Weisstein. https://mathworld.wolfram.com/ReductionOrder.html
Subject classifications
