Exact Bounds for lengths of reductions in typed λ-calculus

Journal of Symbolic Logic 66 (3):1277-1285 (2001)
  Copy   BIBTEX


We determine the exact bounds for the length of an arbitrary reduction sequence of a term in the typed λ-calculus with β-, ξ- and η-conversion. There will be two essentially different classifications, one depending on the height and the degree of the term and the other depending on the length and the degree of the term



    Upload a copy of this work     Papers currently archived: 76,199

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library


Added to PP

55 (#216,118)

6 months
1 (#448,894)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Herbrand's theorem as higher order recursion.Bahareh Afshari, Stefan Hetzl & Graham E. Leigh - 2020 - Annals of Pure and Applied Logic 171 (6):102792.
Elementary Proof of Strong Normalization for Atomic F.Fernando Ferreira & Gilda Ferreira - 2016 - Bulletin of the Section of Logic 45 (1):1-15.
A decidable theory of type assignment.William R. Stirton - 2013 - Archive for Mathematical Logic 52 (5-6):631-658.

View all 9 citations / Add more citations

References found in this work

The Lambda Calculus. Its Syntax and Semantics.E. Engeler - 1984 - Journal of Symbolic Logic 49 (1):301-303.
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