This course is a prerequisite for Types (Part II).

Aims

This course aims (a) to show how lambda-calculus and related
theories can provide a foundation for a large part of practical
programming,
(b) to present students with one particular type analysis algorithm
so that they will be better able to appreciate the Part II Types
course, and (c) to provide a bridge between the Part IA Foundations of Computer Science course and the theory options in Part II.

Lectures

Part A. The theory

Introduction. Combinators. Constants and Free Variables. Reduction.
Equality. the Church-Rosser theorem. Normal forms.

The Lambda calculus. Lambda-terms, alpha and beta conversions.
Free and bound variables. Abbreviations in the notation.
Pure and applied lambda calculi. Relationship
between combinators, lambda calculus and typical programming languages.

Encoding of data: booleans, tuples, lists and trees, numbers.
The treatment of recursion: the Y combinator and its use.

Modelling imperative programming styles: handling state information
and the continuation-passing style.

Relationship between this and Turing computability, the halting problem etc.

Part B. Implementation techniques

Combinator reduction as tree-rewrites. Conversion from lambda-calculus to
combinators. The treatment of lambda-bindings
in an interpreter: the environment. Closures. ML implementation of
lambda-calculus. SECD machine. Brief survey of performance issues.

Part C. Type reconstruction

Let-polymorphism reviewed following the Part IA coverage
of ML. Unification. A type-reconstruction algorithm. Decidability and
potential costs.

Objectives

At the end of the course students should

understand the rules for the construction and processing
of terms in the lambda calculus and of Combinators

know how to model all major aspects of general-purpose
computation in terms of these primitives

be able to derive ML-style type judgements
for languages based upon the lambda-calculus

Recommended reading

Hindley, J.R. & Seldin, J.P. (1986). Introduction to combinators and
lambda-calculus. Cambridge University Press (now out of print but try a
library).
Revesz, G.E. (1988). Lambda calculus, combinators and functional
programming. Cambridge University Press (now out of print but try a library).