Abstract
In this talk we discuss the difference between Weak Normalization (WN) and
Strong Normalization (SN) in the framework of orthogonal term rewriting.
With the help of the powerful 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 a 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. We consider an extension to infinitary
rewriting, yielding another proof for the acyclicity of S-terms. The talk
contains some reminiscences and photos.
[NB The table at page 47 contains an
erroneous definition, masked by a red blob.]
Last modified: Wed Apr 13 15:15:45 CEST 2005