Lecturer	Sean Moss
Degrees	Schedule S1(CS&P)(3rd years) — Computer Science and Philosophy Schedule S1(3rd years) — Computer Science Schedule S1(M&CS)(3rd years) — Mathematics and Computer Science Schedule B — MSc in Advanced Computer Science MSc in Mathematics and Foundations of Computer Science
Term	Hilary Term 2020  (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 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.

 

Learning outcomes

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.

Synopsis

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, the matching problem. Principal Type algorithm and correctness.

Syllabus

Terms, 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, matching, correctness of Principal Type Algorithm

Reading list

Essential

• Andrew Ker, lecture notes. Available in course materials section. Comprehensive notes on the entire course, including practice questions and class exercises.

Useful Background

• 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.
• 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 Lambda-Calculus, Cambridge University Press, 1986.

Taking our courses

This form is not to be used by students studying for a degree in the Department of Computer Science, or for Visiting Students who are registered for Computer Science courses

Other matriculated University of Oxford students who are interested in taking this, or other, courses in the Department of Computer Science, must complete this online form by 17.00 on Friday of 0th week of term in which the course is taught. Late requests, and requests sent by email, will not be considered. All requests must be approved by the relevant Computer Science departmental committee and can only be submitted using this form.