On Continuous Normalization
Klaus Aehlig5
and Felix Joachimski5 
| (5) |
Mathematisches Institut, Ludwig-Maximilians-Universität München, Theresienstrasse 39, 80333 München, Germany |
Abstract
This work aims at explaining the syntactical properties of continuous normalization, as introduced in proof theory by Mints,
and further studied by Ruckert, Buchholz and Schwichtenberg. In an extension of the untyped coinductive λ-calculus by void
construcors (so-called repetition rules), a primitive recursive normalization function is defined. Compared with other formulations
of continuous normalization, this definition is much simpler and therefore suitable for analysis in a coalgebraic setting.
It is shown to be continuous w.r.t. the natural topology on non-wellfounded terms with the identity as modulus of continuity.
The number of repetition rules is locally related to the number of β-reductions necessary to reach the normal form (as represented
by the Böhm tree) and the number of applications appearing in this normal form.
Supported by the “Graduiertenkolleg Logik in der Informatik” of the Deutsche Forschungsgemeinschaft
References secured to subscribers.