Extra material

• Freek Wiedijk's λ- and CL-tool.
  Elegant tool, programmed in OCaml, to demonstrate reduction in lambda calculus and CL and to experiment with various reduction strategies. Also provides translations between combinators and lambda terms.
  
• CKI-A voordracht over herschrijven.
  Slides of an introductory talk on rewriting by Vincent van Oostrom (in Dutch).
  
• Vicious circles in term rewriting.
  Slides of a talk by Jan Willem Klop at WRS'04 Aachen.

  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