Based on the course taught by Hugo Paquet in Hilary Term 2021 and lecture notes by Andrew Ker.
Lambda calculus is a way to reason about functions, and is also a model of computation. Its most basic form consists of variables, \(\lambda\)-abstractions and applications.
- Syntax (\(\lambda\)-terms, free/bound variables and capture, contexts)
- Equational theories (equalities, theories, fixed points, consistency, Bohm’s thm)
- Reductions (reductions, \(\lambda I\)/affine/linear terms)
- Normal forms (NFs, normalizing, diamond/CR/unique-NF, \(\beta\)/\(\eta\)/\(\beta\eta\) CR)
- Reduction strategies (strategies, red. sequences, standard red. sequences)
- Solvability (solvability, genericity, theories \(\mathcal H\), \(\mathcal H^*\), sensible, semi-sensible)
- Computation (bools/\(\mathbb N\)/lists, recursive functions, \(\lambda\)-definable, undecidability)
- Combinatory logic (CL, translations, CAs, \(\lambda\)-algebras, comb. completeness)
- Simple types (\(\text{TA}_\lambda\), typing, typability, strongly normalizability)
- Principal typing (principal types/deductions, unification, Hindley’s algo)