LAMBDA-CALCULUS MODELS OF PROGRAMMING LANGUAGES.
MASSACHUSETTS INST OF TECH CAMBRIDGE PROJECT MAC
Pagination or Media Count:
Two aspects of programming languages, recursive definitions and type declarations are analyzed in detail, using Churchs lambda-calculus as the programming language model. The main result on recursion is an analogue to Kleenes 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 EYF, any expression containing YF, has a normal form then EYF EA. Y is Currys 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
- Computer Programming and Software
- Computer Systems