Skip to content
The Lumenary
Advanced undergraduateComputationPlanned

The λ-calculus

The untyped λ-calculus (terms, β-reduction, Church encodings, fixed-point combinators, confluence) and the simply typed λ-calculus with normalisation.

math.comp.lambda-calculus

Show everything needed to reach this topic

The lesson for this topic has not been written yet. The outline below is part of the curriculum map and has not been reviewed.

Builds on

Programming for mathematicsProof: direct, contrapositive, contradiction and induction

Required prerequisites, all the way down: 15

You will learn to

  • Reduce λ-terms and encode booleans, pairs and natural numbers (Church numerals).
  • Use a fixed-point combinator to define recursive functions, and explain why untyped terms need not terminate.
  • State the Church–Rosser theorem and explain why every simply typed term has a normal form.

Definition

  • λ-terms are built from variables by application (M N) and abstraction (λx. M).
  • β-reduction rewrites (λx. M) N to M[N/x], using capture-avoiding substitution.
  • A term is in normal form if no β-reduction applies to it.

Theorem

  • Church–Rosser: β-reduction is confluent, so a term has at most one normal form.
  • The untyped λ-calculus computes exactly the partial recursive functions.
  • Every simply typed λ-term has a normal form; in fact the simply typed λ-calculus is strongly normalising.

Common misconceptions

  • Substituting without renaming bound variables (variable capture).
  • Thinking every λ-term has a normal form; (λx. x x)(λx. x x) does not.

Leads to

Type theory and propositions as typesFormal methods

Optional discoveries

Learning pathways

Further reading

  • H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics (1981)
  • J. Roger Hindley and Jonathan P. Seldin, Lambda-Calculus and Combinators: An Introduction (2008)
  • Benjamin C. Pierce, Types and Programming Languages (2002)