LAMBDA-CALCULUS MODELS OF PROGRAMMING LANGUAGES.
Abstract
Two aspects of programming languages, recursive definitions and type declarations are analyzed in detail, using Church's lambda-calculus as the programming language model. The main result on recursion is an analogue to Kleene's first recursion theorem: If A = FA for any lambda-expressions A and F, then A is an extension of YF in the sense that if E(YF), any expression containing YF, has a normal form then E(YF) = E(A). Y is Curry's paradoxical combinator. The result is shown to be invariant for many different versions of Y. A system of types and type declarations is developed for the lambda-calculus and its semantic assumptions are identified. The system is shown to be adequate in the sense that it permits a preprocessor to check formulae prior to evaluation to prevent type errors. It is shown that any formula with a valid assignment of types to all its subexpressions must have a normal form. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Dec 01, 1968
- Accession Number
- AD0683394
Entities
People
- James H. Morris
Organizations
- Massachusetts Institute of Technology