Exact bounds for lengths of reductions in typed λ-calculus

DOI10.2307/2695106zbMath1159.03305OpenAlexW2086316626MaRDI QIDQ2758058

Arnold Beckmann

Publication date: 6 December 2001

Published in: Journal of Symbolic Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.2307/2695106

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Related Items

The Church-Rosser theorem and quantitative analysis of witnesses ⋮ A By-Level Analysis of Multiplicative Exponential Linear Logic ⋮ A decidable theory of type assignment ⋮ Elementary Proof of Strong Normalization for Atomic F ⋮ On the computational complexity of cut-reduction ⋮ Almost Every Simply Typed $$\lambda $$-Term Has a Long $$\beta $$-Reduction Sequence ⋮ Decidability of bounded higher-order unification ⋮ Herbrand's theorem as higher order recursion ⋮ A formal system of reduction paths for parallel reduction ⋮ Extracting Herbrand disjunctions by functional interpretation ⋮ Continuous normalization for the lambda-calculus and Gödel's T ⋮ GAME SEMANTICS AND THE GEOMETRY OF BACKTRACKING: A NEW COMPLEXITY ANALYSIS OF INTERACTION ⋮ Complexity Hierarchies beyond Elementary ⋮ The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type ⋮ Unnamed Item ⋮ Exact bounds for acyclic higher-order recursion schemes ⋮ A quantitative model for simply typed λ-calculus

Cites Work

• An upper bound for reduction sequences in the typed \(\lambda\)-calculus