Lambda Calculus and Types: 20112012
Lecturer 

Degrees 
Schedule B2 — Computer Science Schedule B2 — Mathematics and Computer Science 
Term 
Michaelmas Term 2011 (16 lectures) 
Overview
As 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 selfcontained 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.
Learning outcomes
The course is an introductory overview of the foundations of computer science with particular reference to the lambdacalculus. Students will
 understand the syntax and equational theory of the untyped lambdacalculus, 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 betareduction;
 see the connections between lambdacalculus and computabilty, and an example of how an undecidability proof can be constructed;
 see the connections and distinctions between lambdacalculus and combinatory logic;
 learn about simple type systems for the lambdacalculus, and how to prove a strong normalization result;
 understand how to deduce types for terms, and prove correctness of a principal type algorithm.
Synopsis
Chapter 0 (1 lecture)
Introductory lecture. Preparation for use of inductive definitions and proofs.
Chapters 13 (5 lectures)
Terms, free and bound variables, alphaconversion, substitution, variable
convention, contexts, the formal theory lambda beta, the eta rule, fixed point combinators, lambdatheories. Reduction.
Compatible closure, reflexive transitive closure, diamond and ChurchRosser properties for general notions of reduction. betareduction,
proof of the ChurchRosser property (via parallel reduction), connection between betareduction and lambda beta, consistency
of lambda beta. Inconsistency of equating all terms without betanormal 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, ScottCurry 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 lambdacalculus, mismatches between combinary logic and lambdacalculus, basis. Term algebras.
Chapters 68 (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, the matching problem. Principal Type algorithm and correctness.
Syllabus
Terms, formal theories lambda beta and lambda beta eta, fixed point combinators; reduction, ChurchRosser property of betareduction 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 lambdacalculus, 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, matching, correctness of Principal Type AlgorithmReading list
Essential
 Andrew Ker, lecture notes. Available online and handed out in the lectures. Comprehensive notes on the entire course, including practice questions and class exercises.
 H. P. Barendregt, The Lambda Calculus. NorthHolland, revised edition, 1984.
 J. R. Hindley, Basic Simple Type Theory, CUP Cambridge Tracts in Theoretical Computer Science 42, 1997.
 J.Y. Girard, Y. Lafont, & P. Taylor, Proofs and Types, CUP Cambridge Tracts in Theoretical Computer Science 7, 1989.
 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 LambdaCalculus, Cambridge University Press, 1986.