Lambda Calculus

---

BA in Computer Science, Paper II.1 BA in Mathematics & Computer Science, Paper II.1 MSc in Mathematics and the Foundations of Computer Science

16 lectures HT

---

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 formal theory, term rewriting, 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 by its relation to the lambda calculus. Although some previous knowledge of formal logic and computability (such as provided by the Mathematics course b1) would be an advantage, it is certainly not necessary.

Learning Outcomes

To be familiar with the syntax of the lambda calculus, including alpha conversion to avoid free variable capture.

To understand the formal theories of the untyped lambda calculus; to see fixed point combinators in action; to meet some standard theorems from the literature of the untyped lambda calculus.

To be introduced to the topic of term rewriting, with specific examples in the lambda calculus; by relating reduction to the formal theory, to understand why the standard theory of untyped lambda calculus is consistent.

To be introduced to first order languages, with combinatory algebras as a specific example; to understand the connection between the untyped lambda calculus and combinatory algebras.

To see how numbers and functions, while omitted from the pure untyped lambda calculus, can nonetheless be represented in it.

To understand the concepts of unsolvability and head normal form, and some associated lambda theories.

To understand what it means for a language to be Turing complete, and to see why the pure untyped lambda calculus has this property.

To see how the pure lambda calculus may be given a simple type system, and to understand some of the key differences from the untyped language.

To see how the lambda calculus underpins functional programming, via equational and operational semantics for PCF.

---