The typed lambda-calculus is not elementary recursive

DOI10.1016/0304-3975(79)90007-0zbMath0411.03050OpenAlexW1988983596WikidataQ56050817 ScholiaQ56050817MaRDI QIDQ1259590

Richard Statman

Publication date: 1979

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(79)90007-0

zbMATH Keywords

proof theorylower boundstyped lambda calculuselementary recursive calculuslength of derivations

Mathematics Subject Classification ID

Computability and recursion theory (03D99) Combinatory logic and lambda calculus (03B40) Complexity of proofs (03F20)

Related Items (42)

Upper bounds for standardizations and an application ⋮ The role of polymorphism in the characterisation of complexity by soft types ⋮ (Optimal) duplication is not elementary recursive ⋮ Word operation definable in the typed \(\lambda\)-calculus ⋮ Fully abstract translations between functional languages ⋮ The most nonelementary theory ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Many more predecessors: A representation workout ⋮ On session types and polynomial time ⋮ A characterization of lambda-terms transforming numerals ⋮ A characterization of lambda definable tree operations ⋮ On the existence of closed terms in the typed lambda calculus II: Transformations of unification problems ⋮ On Higher-Order Probabilistic Subrecursion ⋮ Unnamed Item ⋮ Finitely stratified polymorphism ⋮ The Impact of the Lambda Calculus in Logic and Computer Science ⋮ An analysis of the Core-ML language: Expressive power and type reconstruction ⋮ Decidability of bounded higher-order unification ⋮ The complexity of higher-order queries ⋮ Least Upper Bounds on the Size of Church-Rosser Diagrams in Term Rewriting and λ-Calculus ⋮ A formal system of reduction paths for parallel reduction ⋮ Functional interpretations of feasibly constructive arithmetic ⋮ A simple proof of a theorem of Statman ⋮ λ-definable functionals andβη conversion ⋮ Functional programs as compressed data ⋮ On the membership problem for non-linear abstract categorial grammars ⋮ Ensuring termination by typability ⋮ Unnamed Item ⋮ Intuitionistic propositional logic is polynomial-space complete ⋮ The semantics of second-order lambda calculus ⋮ Complexity Hierarchies beyond Elementary ⋮ Is the Optimal Implementation Inefficient? Elementarily Not ⋮ Ramified recurrence and computational complexity. III: Higher type recurrence and elementary complexity ⋮ LAMBDA-REPRESENTABLE FUNCTIONS OVER TERM ALGEBRAS ⋮ Ordinals and ordinal functions representable in the simply typed lambda calculus ⋮ Parallel beta reduction is not elementary recursive ⋮ An abstract approach to stratification in linear logic ⋮ Completeness, invariance and λ-definability ⋮ Functions over free algebras definable in the simply typed lambda calculus ⋮ The complexity of type inference for higher-order typed lambda calculi ⋮ A Logical Framework with Explicit Conversions ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction

Cites Work

• A unification algorithm for typed \(\overline\lambda\)-calculus
• The polynomial-time hierarchy
• Fully abstract models of typed \(\lambda\)-calculi
• Intuitionistic propositional logic is polynomial-space complete
• On the computational power of pushdown automata
• Godel's interpretation of intuitionism
• Completeness, invariance and λ-definability
• The Connection between Equivalence of Proofs and Cartesian Closed Categories
• Definierbare Funktionen imλ-Kalkül mit Typen
• A theory of prepositional types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: The typed lambda-calculus is not elementary recursive