A term is in _normal form_ if no [[rewrite rule]] applies anywhere within the term.

This implies that [[rewrite rules]] are applied everywhere in a term. This is not always appropriate. 

In rewriting with [[rewriting strategies]] the application of rewrite rules is under control of a user-defined strategy. In this setting the notion of normal form depends on the strategy used, and
can no longer be related only to the set of rules.

-----
CategoryGlossary | StrategoGlossary