λ-definable functionals andβη conversion

DOI10.1007/BF02023009zbMath0537.03009OpenAlexW2319619459MaRDI QIDQ3322071

Richard Statman

Publication date: 1983

Published in: Archiv für Mathematische Logik und Grundlagenforschung (Search for Journal in Brave)

Full work available at URL: https://eudml.org/doc/138003

zbMATH Keywords

semanticscongruence relationtyped lambda calculustype structuresbeta-eta-conversionlambda definable functionalslambda-free functional equations

Mathematics Subject Classification ID

Functional equations and inequalities (39B99) Combinatory logic and lambda calculus (03B40)

Related Items

Word operation definable in the typed \(\lambda\)-calculus, Weak typed Böhm theorem on IMLL, Provable isomorphisms of types, Böhm theorem and Böhm trees for the \(\varLambda \mu\)-calculus, The relational model is injective for multiplicative exponential linear logic (without weakenings), Unnamed Item, A characterization of lambda definable tree operations, Identity of Proofs Based on Normalization and Generality, The Typed Böhm Theorem, Linear realizability and full completeness for typed lambda-calculi, What is the meaning of proofs?. A Fregean distinction in proof-theoretic semantics, Extensional models for polymorphism, ETA-RULES IN MARTIN-LÖF TYPE THEORY, Prelogical relations

Cites Work

• Unnamed Item
• Unnamed Item
• The typed lambda-calculus is not elementary recursive
• Completeness, invariance and λ-definability