Reflective λ-Calculus

摘要

We introduce a general purpose typed λ-calculus λ~∞ which contains intuitionistic logic, is capable of internalizing its own derivations as λ-terms and yet enjoys strong normalization with respect to a natural reduction system. In particular, λ~∞ subsumes the typed λ-calculus. The Curry-Howard isomorphism converting intuitionistic proofs into λ-terms is a simple instance of the internalization property of λ~∞. The standard semantics of λ~∞ is given by a proof system with proof checking capacities. The system λ~∞ is a theoretical prototype of reflective extensions of a broad class of type-based systems in programming languages, provers, AI and knowledge representation, etc.