Vicious Circles in Orthogonal Term Rewriting Systems

AbstractIn 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