Lambda Calculus

Sixteen-hour lecture course. Final-year computer science undergraduate / MSc

Nature and aim of the course

Lambda calculus is a theory of functions that is central to (theoretical) computer science. It is well known that all recursive functions are representable as lambda terms: the representation is so compelling that definability in the calculus may as well be regarded as a definition of computability. This forms part of the standard foundations of computer science and mathematics. Less familiar are two separate developments -- one in programming, the other in proof theory -- in which lambda calculus has played a key role:

Lambda calculus is the commonly accepted basis of functional programming languages; and it is folklore that the calculus is the prototypical functional language in purified form.
The idea that there is a close relation between proof theory and a theory of functions is an old one. It underlies the Kolmogorov-Brouwer-Heyting interpretation of intuitionistic logic, and the Curry-Howard isomorphism between natural deduction and typed lambda calculus.

We develop the syntax and semantics of lambda calculus along these two themes. The aim of this course is to provide the foundation for an important aspect of the semantics of programming languages with a view to helping enthusiastic research students appreciate (perhaps even begin to address) some of the open problems in the field. The second theme in particular will be followed up by two new courses Type theory, and Types, Proofs and Categorical Logic in the Hilary term. Familiarity with any of the following will be useful: the basics of computability, first-order predicate logic, functional programming and semantics of programming languages.

Synopsis

History, brief survey, formal theory, fixed point (recursion) theorems, combinatory logic: combinatory completeness, translations between lambda calculus and combinatory logic; reduction: Church-Rosser theorem, normalization, standardization, finite development; Bohm's theorem and applications; basic recursion theory: Church and Scott numerals, strong representability in call-by-value lambda calculus; lambda calculi considered as programming languages: lazy lambda calculus, head reduction, solvability, context lemma; simple type theory and PCF: higher-type sequentiality and full abstraction (brief), (categorical) models of lambda calculus, Curry-Howard isomorphism; current developments.

Selected Reading

[1] S. Abramsky and C.-H. L. Ong. Full abstraction in the lazy lambda calculus. Information and Computation, 105:159-267, 1993.

[2] H. Barendregt. The Lambda Calculus. North-Holland, revised edition, 1984.

[3] R. L. Crole. Categories for Types. Cambridge University Press, 1993.

[4] J.-Y. Girard, Y. Lafont, and P. Taylor. Proofs and Types. Cambridge University Press, 1989.

[5] C. A. Gunter. Semantics of Programming Languages: Structures and Techniques. MIT Press, 1992.

[6] J. R. Hindley and J. P. Seldin. To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, 1980.

[7] J. L. Krivine. Lambda-Calculus, Types and Models. Ellis Horwood, 1990.

[8] G. D. Plotkin. Call-by-name, call-by-value and the lambda calculus. Theoretical Computer Science, 1:125-159, 1975.

[9] G.D. Plotkin. LCF as a programming language. Theoretical Computer Science, 5:223-255, 1977.

[10] D. S. Scott. Lambda calculus: Some models, some philosophy. In J. Barwise, H. J. Keisler, and K. Kunen, editors, The Kleene Symposium, pages 223-265. North-Holland Publishing Company, 1980.

Course material

Course notes are available from the Reception or by clicking here.

[Last updated on 23 Jan 1998 by Luke Ong]