Intuitively, a reduction order
R relates two
terms s and
t if
t is properly "simpler" than
s in some sense. For example, simplification of terms may be a part of a
computer algebra program, and may be using the rule set {
x+0 →
x , 0+
x →
x ,
x*0 → 0, 0*
x → 0,
x*1 →
x , 1*
x →
x }. In order to prove impossibility of endless loops when simplifying a term using these rules, the reduction order defined by "
sRt if term
t is properly shorter than term
s" can be used; applying any rule from the set will always properly shorten the term. In contrast, to establish termination of "distributing-out" using the rule
x*(
y+
z) →
x*
y+
x*
z, a more elaborate reduction order will be needed, since this rule may blow up the term size due to duplication of
x. The theory of rewrite orders aims at helping to provide an appropriate order in such cases. ==Formal definitions==