Exact bounds for lengths of reductions in typed \(\lambda\)-calculus. (English) Zbl 1159.03305

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.


03B40 Combinatory logic and lambda calculus
Full Text: DOI


[1] Computer Science Report CS-R9545 (1995)
[2] DOI: 10.1007/BF01621476 · Zbl 0719.03007
[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.