Beckmann, Arnold Exact bounds for lengths of reductions in typed \(\lambda\)-calculus. (English) Zbl 1159.03305 J. Symb. Log. 66, No. 3, 1277-1285 (2001). Summary: We determine the exact bounds for the length of an arbitrary reduction sequence of a term in the typed \(\lambda\)-calculus with \(\beta\)-, \(\xi\)- and \(\eta\)-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. Reviewer: Reviewer (Berlin) Cited in 15 Documents MSC: 03B40 Combinatory logic and lambda calculus PDF BibTeX XML Cite \textit{A. Beckmann}, J. Symb. Log. 66, No. 3, 1277--1285 (2001; Zbl 1159.03305) Full Text: DOI References: [1] Computer Science Report CS-R9545 (1995) [2] DOI: 10.1007/BF01621476 · Zbl 0719.03007 · doi:10.1007/BF01621476 [3] The lambda calculus 103 (1984) [4] Technical Report ECS-LFCS-98-381 [5] The L. E. J. Brouwer centenary symposium pp 453– (1982) This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.