Rewrite order

In theoretical computer science, in particular in automated reasoning about formal equations, reduction orderings are used to prevent endless loops.

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

Formally, a binary relation (→) on the set of terms is called a rewrite relation if it is closed under contextual embedding and under instantiation; formally: if l→r implies u[lσ]p→u[rσ]p for all terms l, r, u, each path p of u, and each substitution σ.