Reduction Order

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.

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.