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).
