... apply the ...
transforming [the terms] until a 'reduced' or 'normal form' is
reached where no further rules are applicable.
A set of
is said to be 'terminating' if
every sequence of rewrites on ground terms eventually reaches normal
form, and is said to be
if any two rewrite
sequences starting from the same term ... can always be further
rewritten in such a way that they reach equal values .... It is a
basic result of term-rewriting theory that if a system of rewrite
rules is Church-Rosser and terminating, then every term has a
-- Goguen & Meseguer.
Functional, Object-Oriented and Relational Programming with