Analyzing Godel's T Via Expanded Head Reduction Trees

&
Mathematical Logic Quarterly 46 (4):517-536 (2000)
  Copy   BIBTEX

Abstract

Inspired from Buchholz' ordinal analysis of ID1 and Beckmann's analysis of the simple typed λ-calculus we classify the derivation lengths for Gödel's system T in the λ-formulation

Categories

Keywords

Reprint years

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 93,774

External links

  • This entry has no external links. Add one.
Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Continuous normalization for the lambda-calculus and Gödel’s T.Klaus Aehlig & Felix Joachimski - 2005 - Annals of Pure and Applied Logic 133 (1-3):39-71.
Short proofs of normalization for the simply- typed λ-calculus, permutative conversions and Gödel's T.Felix Joachimski & Ralph Matthes - 2003 - Archive for Mathematical Logic 42 (1):59-87.
How to assign ordinal numbers to combinatory terms with polymorphic types.William R. Stirton - 2012 - Archive for Mathematical Logic 51 (5):475-501.
How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study.Andreas Weiermann - 1998 - Journal of Symbolic Logic 63 (4):1348-1370.
How is It That Infinitary Methods can be Applied to Finitary Mathematics? Godel's T: A Case Study.Andreas Weiermann - 1998 - Journal of Symbolic Logic 63 (4):1348-1370.
Andreas Weiermann. How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study. The journal of symbolic logic, vol. 63 (1998), pp. 1348–1370. [REVIEW]Thomas Strahm - 2002 - Bulletin of Symbolic Logic 8 (3):435-436.
Andreas Weiermann. How is it that infinitary methods can be applied to finitary mathematics? Gödel's T: a case study. The journal of symbolic logic, vol. 63 (1998), pp. 1348–1370. [REVIEW]Thomas Strahm - 2002 - Bulletin of Symbolic Logic 8 (3):435-435.
Strong Normalization via Natural Ordinal.Daniel Durante Pereira Alves - 1999 - Dissertation,
Characterizing the elementary recursive functions by a fragment of Gödel's T.Arnold Beckmann & Andreas Weiermann - 2000 - Archive for Mathematical Logic 39 (7):475-491.
Polymorphic extensions of simple type structures. With an application to a bar recursive minimization.Erik Barendsen & Marc Bezem - 1996 - Annals of Pure and Applied Logic 79 (3):221-280.

Analytics

Added to PP
2013-12-01

Downloads
36 (#119,765)

6 months
36 (#429,500)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Add more citations

References found in this work

Exact Bounds for lengths of reductions in typed λ-calculus.Arnold Beckmann - 2001 - Journal of Symbolic Logic 66 (3):1277-1285.
An upper bound for reduction sequences in the typed λ-calculus.Helmut Schwichtenberg - 1991 - Archive for Mathematical Logic 30 (5-6):405-408.

Add more references