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
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.
Eager and Lazy evaluation.
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. Return address seen as an additional
continuation parameter.
Relationship between this and Turing computability, the halting problem etc.
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.
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 combinatory terms and terms in the lambda calculus
know how to model all major aspects of general-purpose
computation in terms of these primitives
know how lambda terms may be efficiently interpreted by machine
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).
