Continuous Normalization

Felix Joachimski

(Munich, visiting Bristol)

Continuous normalization has been introduced to proof theory by Mints and since then studied (amongst others) by Buchholz and Schwichtenberg. The talk will try to illustrate the underlying ideas by applying them to a much simpler setting - the untyped lambda-calculus. This is quite interesting, because the process of continuous normalization can even be applied to non-normalizing terms. It uses so-called repetition rules to coinductively construct the normal form of its input. The algorithm is very intuitive and ensures that the function it models is primitive recursive; being defined on non-wellfounded terms, it has the identity as modulus of continuity. We will explore some further fascinating properties and in particular relate the continuous normal forms of typed to derivations of strong normalizability, which leads to new bounds on the height of these terms' reduction trees. The talk is based on two recent articles by Klaus Aehlig and Felix Joachimski, available on

[1] On continuous normalization. CSL 2002.
[2] Continuous normalization in the untyped lambda-calculus and Godel's T.
Friday 31st January 2003, 14:00
Robert Recorde Room
Department of Computer Science