Lambda Calculus and Types: 2009-2010
OverviewAs a language for describing functions, any literate computer scientist would expect to understand the vocabulary of the lambda calculus. It is folklore that various forms of the lambda calculus are the prototypical functional programming languages, but the pure theory of the lambda calculus is also extremely attractive in its own right. This course introduces the terminology and philosophy of the lambda calculus, and then covers a range of self-contained topics studying the language and some related structures. Topics covered include the equational theory, term rewriting and reduction strategies, combinatory logic, Turing completeness and type systems. As such, the course will also function as a brief introduction to many facets of theoretical computer science, illustrating each (and showing the connections with practical computer science) by its relation to the lambda calculus.
There are no prerequisites, but the course will assume familiarity with construting mathematical proofs. Some basic knowledge of computability would be useful for one of the topics (the Models of Computation course is much more than enough), but is certainly not necessary.
The course is an introductory overview of the foundations of computer science with particular reference to the lambda-calculus. Students will
- understand the syntax and equational theory of the untyped lambda-calculus, and gain familiarity with manipulation of terms;
- be exposed to a variety of inductive proofs over recursive structures;
- learn techniques for analysing term rewriting systems, with particular reference to beta-reduction;
- see the connections between lambda-calculus and computabilty, and an example of how an undecidability proof can be constructed;
- see the connections and distinctions between lambda-calculus and combinatory logic;
- learn about simple type systems for the lambda-calculus, and how to prove a strong normalization result;
- understand how to deduce types for terms, and prove correctness of a principal type algorithm.
Chapter 0 (1 lecture)
Introductory lecture. Preparation for use of inductive definitions and proofs.
Chapters 1-3 (5 lectures)
Terms, free and bound variables, alpha-conversion, substitution, variable convention, contexts, the formal theory lambda beta, the eta rule, fixed point combinators, lambda-theories. Reduction. Compatible closure, reflexive transitive closure, diamond and Church-Rosser properties for general notions of reduction. beta-reduction, proof of the Church-Rosser property (via parallel reduction), connection between beta-reduction and lambda beta, consistency of lambda beta. Inconsistency of equating all terms without beta-normal form. Reduction strategies, head and leftmost reduction. Standard reductions. Proof that leftmost reduction is normalising. Statement, without proof, of Genericity Lemma, and simple applications.
Chapter 4 (2 lectures)
Church numerals, definability of total recursive functions. Second Recursion Theorem, Scott-Curry Theorem, undecideability of equality in lambda beta. Briefly, extension to partial functions.
Chapter 5 (2 lectures)
Untyped combinatory algebras. Abstraction algorithm, combinatory completeness, translations to and from untyped lambda-calculus, mismatches between combinary logic and lambda-calculus, basis. Term algebras.
Chapters 6-8 (6 lectures)
Simple type assignment a la Curry using Hindley's TA lambda system. Contexts and deductions. Subject Construction Lemma, Subject Reduction Theorem and failure of Subject Expansion. Briefly, a system with type invariance under equality. Tait's proof of strong normalisation. Consequences: no fixed point combinators, poor definability power. Pointer to literature on PCF as the obvious extension of simple types to cover all computable functions. Type substitutions and unification, Robinson's algorithm. Principal Type algorithm and correctness.
SyllabusTerms, formal theories lambda beta and lambda beta eta, fixed point combinators; reduction, Church-Rosser property of beta-reduction and consistency of lambda beta; reduction strategies, standard reduction sequences, proof that leftmost reduction is normalising; Church numerals, definability of total recursive functions in the lambda-calculus, Second Recusion Theorem and undecidability results; combinatory algebras, combinatory completeness, basis; simple types a la Curry, type deductions, Subject Reduction Theorem, strong normalisation and consequences; type substitutions, unification, correctness of Principal Type Algorithm
- Andrew Ker, lecture notes. Available from reception at the start of term. Comprehensive notes on the entire course, including practice questions and class exercises.
- H. P. Barendregt, The Lambda Calculus. North-Holland, revised edition, 1984.
- J. R. Hindley, Basic Simple Type Theory, CUP Cambridge Tracts in Theoretical Computer Science 42, 1997.
- C. Hankin, Lambda Calculi, A Guide for Computer Scientists, OUP Graduate Texts in Computer Science, 1994.
- J. R. Hindley & J. P. Seldin, Introduction to Combinators and Lambda-Calculus, Cambridge University Press, 1986.
- J.-Y. Girard, Y. Lafont, & P. Taylor, Proofs and Types, CUP Cambridge Tracts in Theoretical Computer Science 7, 1989.