Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
My Menu
Saved Items

On Continuous Normalization

Klaus AehligContact Information and Felix JoachimskiContact Information

(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

Contact Information Klaus Aehlig
Email: aehlig@mathematik.uni-muenchen.de

Contact Information Felix Joachimski
Email: joachski@mathematik.uni-muenchen.de
Fulltext Preview (Small, Large)
Image of the first page of the fulltext

References secured to subscribers.



Export this chapter
Export this chapter as RIS | Text
 
Remote Address: 38.107.191.109 • Server: MPWEB26
HTTP User Agent: CCBot/1.0 (+http://www.commoncrawl.org/bot.html)