### Exact Bounds for Lengths of Reductions in Typed $\lambda$-Calculus

Arnold Beckmann
Source: J. Symbolic Logic Volume 66, Issue 3 (2001), 1277-1285.

#### Abstract

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.

Full-text: Remote access
If you are a member of the ASL, log in to Euclid for access.
Full-text is available via JSTOR, for JSTOR subscribers. Go to this article in JSTOR.

Permanent link to this document: http://projecteuclid.org/euclid.jsl/1183746559
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 4, "mathjax_display_tex": 0, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": true, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.8298137187957764, "perplexity_flag": "middle"}