3rd International School on Rewriting
21 – 26 July 2008, Obergurgl, Austria
Program – Track B – An Infinitary Rewriting Primer
Lecturer
Jan Willem KlopIntroduction
The course aims to give an impression of the state of the art in infinitary rewriting. The focus will be on infinitary first order rewriting, infinitary lambda calculus and extensions, and properties of these systems, notably with respect to infinitary confluence and infinitary normalization.
A selection of the following topics will be presented:
- countable ordinals and computing with Cantor normal forms,
- acyclicity in combinatory logic and orthogonal term rewriting,
- enumerators and fixed point combinators in lambda calculus.
- combinatory reduction systems and lambda-phi calculus,
- compression and infinitary normalization in infinitary first order term rewriting,
- productivity of stream definitions, Thue-Morse sequence, Toeplitz sequence,
- tree ordinals,
- infinitary lambda calculus and Böhm trees,
- three applications of infinitary lambda calculus: Berry’s sequentiality theorem, infinitary delta-reduction, relative recursiveness,
- supporting tools: lambda-CL calculator, tree ordinal tool, pebble flow tool, productivity analyzer.