In this paper we first study the difference between Weak Normalization (WN) and Strong Normalization (SN), in the framework of first order orthogonal rewriting systems. With the help of the Erasure Lemma we establish a Pumping Lemma, yielding information about exceptional terms, defined as terms that are WN but not SN. A corollary is that if an orthogonal TRS is WN, there are no cyclic reductions in finite reduction graphs. This is a stepping stone towards the insight that orthogonal TRSs with the property WN, do not admit cyclic reductions at all. © 2005 Elsevier B.V. All rights reserved.
Proceedings title: Proceedings of the 4th International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2004)