Annals of Pure and Applied Logic 133 (1-3):39-71 (2005)

Building on previous work by Mints, Buchholz and Schwichtenberg, a simplified version of continuous normalization for the untyped λ-calculus and Gödel’s is presented and analysed in the coalgebraic framework of non-wellfounded terms with so-called repetition constructors.The primitive recursive normalization function is uniformly continuous w.r.t. the natural metric on non-wellfounded terms. Furthermore, the number of necessary repetition constructors is locally related to the number of reduction steps needed to reach the normal form and its size.It is also shown how continuous normal forms relate to derivations of strong normalizability in the typed λ-calculus and how this leads to new bounds for the sum of the height of the reduction tree and the size of the normal form.Finally, the methods are extended to an infinitary λ-calculus with ω-rule and permutative conversions and this is used to derive a strong form of normalization for an iterative version of Gödel’s system , leading to a value table semantics for number-theoretic functions
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1016/j.apal.2004.10.003
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 54,740
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Notation Systems for Infinitary Derivations.Wilfried Buchholz - 1991 - Archive for Mathematical Logic 30 (5-6):277-296.
Exact Bounds for Lengths of Reductions in Typed Λ-Calculus.Arnold Beckmann - 2001 - Journal of Symbolic Logic 66 (3):1277-1285.

View all 8 references / Add more references

Citations of this work BETA

On the Computational Complexity of Cut-Reduction.Klaus Aehlig & Arnold Beckmann - 2010 - Annals of Pure and Applied Logic 161 (6):711-736.

Add more citations

Similar books and articles

Topological Representation of the Lambda-Calculus.Steve Awodey - 2000 - Mathematical Structures in Computer Science 10 (1):81-96.
Recursion Theory and the Lambda-Calculus.Robert E. Byerly - 1982 - Journal of Symbolic Logic 47 (1):67-83.
Light Affine Lambda Calculus and Polynomial Time Strong Normalization.Kazushige Terui - 2007 - Archive for Mathematical Logic 46 (3-4):253-280.
Strong Normalization of Program-Indexed Lambda Calculus.Norihiro Kamide - 2010 - Bulletin of the Section of Logic 39 (1/2):65-78.
$Lambdamu$-Calculus and Bohm's Theorem.Rene David & Walter Py - 2001 - Journal of Symbolic Logic 66 (1):407-413.
Lambda Calculus with Types.H. P. Barendregt - 2013 - Cambridge University Press.
Typed Lambda-Calculus in Classical Zermelo-Frænkel Set Theory.Jean-Louis Krivine - 2001 - Archive for Mathematical Logic 40 (3):189-205.


Added to PP index

Total views
17 ( #578,365 of 2,386,868 )

Recent downloads (6 months)
1 ( #550,981 of 2,386,868 )

How can I increase my downloads?


My notes