Lambda Calculus

Why This Matters

Lambda calculus is one of the two foundational models of computation (the other being Turing machines). It strips computation down to three operations: naming a variable, defining a function, and applying a function to an argument. Despite this simplicity, it can express any computable function.

Lambda calculus matters for three reasons. First, it is the theoretical foundation of functional programming (Haskell, ML, Lisp). Second, when you add types, it becomes the foundation of type theory and proof assistants like Lean and Coq. Third, the Curry-Howard correspondence says that typed lambda terms are proofs: programming and proving are the same activity in different notation.

Core Definitions

Definition

Lambda Term (Untyped)

The set of lambda terms $\Lambda$ is defined inductively:

Variable: $x \in \Lambda$ for any variable $x$ .
Abstraction: if $M \in \Lambda$ and $x$ is a variable, then $(\lambda x.\, M) \in \Lambda$ . This denotes a function with parameter $x$ and body $M$ .
Application: if $M, N \in \Lambda$ , then $(M\, N) \in \Lambda$ . This denotes applying function $M$ to argument $N$ .

Nothing else is a lambda term. There are no numbers, no booleans, no data structures. Everything is built from these three forms.

Definition

Free and Bound Variables

In $\lambda x.\, M$ , the variable $x$ is bound. An occurrence of $x$ in $M$ that is not inside another $\lambda x.\, \ldots$ is bound by this abstraction. A variable occurrence is free if it is not bound by any enclosing $\lambda$ .

Example: in $\lambda x.\, (x\, y)$ , $x$ is bound and $y$ is free.

Definition

Beta-Reduction

Beta-reduction is the computation rule of lambda calculus:

$(\lambda x.\, M)\, N \to_\beta M[x := N]$

where $M[x := N]$ means "substitute $N$ for every free occurrence of $x$ in $M$ " (with appropriate renaming to avoid variable capture). This is function application: apply the function $\lambda x.\, M$ to the argument $N$ by substituting $N$ for $x$ in the body $M$ .

Definition

Normal Form

A lambda term is in normal form if no beta-reduction can be applied to it or any of its subterms. A term in normal form is "fully computed." Not every lambda term has a normal form; for example, $\Omega = (\lambda x.\, x\, x)(\lambda x.\, x\, x)$ reduces to itself forever.

Definition

Alpha-Equivalence

Two terms are alpha-equivalent if they differ only by a consistent renaming of bound variables: $\lambda x.\, M \equiv_\alpha \lambda y.\, M[x := y]$ provided $y$ does not occur free in $M$ . For example, $\lambda x.\, x \equiv_\alpha \lambda y.\, y$ . Lambda terms are formally identified up to alpha-equivalence; the choice of bound-variable name is irrelevant.

Definition

Eta-Reduction

Eta-reduction identifies a function with its pointwise application:

$\lambda x.\, (M\, x) \to_\eta M \quad \text{if } x \text{ is not free in } M$

Eta says "if a function just hands its argument to $M$ , it is $M$ ." Beta-eta equivalence ( $\equiv_{\beta\eta}$ ) is the standard equational theory of the lambda calculus and corresponds to extensional equality of functions.

Church Encodings

Lambda calculus has no built-in data types, but you can encode them as lambda terms.

Church booleans:

$\text{true} = \lambda t.\, \lambda f.\, t$ $\text{false} = \lambda t.\, \lambda f.\, f$

A boolean is a function that takes two arguments and returns one of them. Conditionals come for free: $\text{if}\, b\, \text{then}\, M\, \text{else}\, N$ is just $b\, M\, N$ .

Church numerals:

$\bar{0} = \lambda f.\, \lambda x.\, x$ $\bar{1} = \lambda f.\, \lambda x.\, f\, x$ $\bar{2} = \lambda f.\, \lambda x.\, f\, (f\, x)$ $\bar{n} = \lambda f.\, \lambda x.\, f^n\, x$

A numeral $\bar{n}$ is a function that takes $f$ and $x$ and applies $f$ to $x$ exactly $n$ times. Addition is $\lambda m.\, \lambda n.\, \lambda f.\, \lambda x.\, m\, f\, (n\, f\, x)$ . Multiplication is $\lambda m.\, \lambda n.\, \lambda f.\, m\, (n\, f)$ .

Recursion via Fixpoint Combinators

The untyped lambda calculus has no built-in recursion, yet it is Turing-complete. The trick is the Y combinator, due to Curry:

$Y = \lambda f.\, (\lambda x.\, f\, (x\, x))\, (\lambda x.\, f\, (x\, x))$

Applying $Y$ to a function $F$ produces a fixed point of $F$ :

$Y\, F \to_\beta F\, (Y\, F)$

Verification: $Y\, F = (\lambda x.\, F\, (x\, x))\, (\lambda x.\, F\, (x\, x)) \to_\beta F\, ((\lambda x.\, F\, (x\, x))\, (\lambda x.\, F\, (x\, x))) = F\, (Y\, F)$ .

To define a recursive function such as factorial, write the body as a function of a "self" parameter and pass it to $Y$ :

$\text{fact} = Y\, (\lambda f.\, \lambda n.\, \text{if}\ (\text{iszero}\ n)\ \text{then}\ \bar{1}\ \text{else}\ \text{mult}\ n\ (f\ (\text{pred}\ n)))$

The Y combinator does not type-check in the simply typed lambda calculus (it relies on self-application $x\, x$ ). This is why total functional languages (Coq, Agda) require the recursion principle of inductive types instead of an explicit fixpoint combinator. Other fixpoint combinators exist (Turing's $\Theta = (\lambda x.\, \lambda y.\, y\, (x\, x\, y))\, (\lambda x.\, \lambda y.\, y\, (x\, x\, y))$ is the call-by-value-friendly variant), but $Y$ is canonical.

Reduction Strategies

Confluence guarantees that if a normal form exists, it is unique. But not every reduction strategy reaches it. Two are standard:

Normal-order (leftmost-outermost): always reduce the leftmost outermost redex. If a normal form exists, normal-order reduction finds it. Corresponds to call-by-name evaluation in programming languages.
Applicative-order (leftmost-innermost): always reduce arguments before applying functions. Corresponds to call-by-value. Faster in practice but may diverge when normal-order would terminate (e.g., $(\lambda x.\, \bar{0})\, \Omega$ has normal form $\bar{0}$ under normal-order but loops under applicative-order).

Plotkin's "Call-by-name, call-by-value and the lambda-calculus" (Theoretical Computer Science 1975) gave the standard semantic comparison and introduced the call-by-value lambda calculus $\lambda_v$ as a separate formal system. Real-world languages mix strategies: ML and OCaml are call-by-value, Haskell is call-by-need (lazy, a memoized form of call-by-name).

Main Theorems

Theorem

Church-Rosser Theorem (Confluence)

Statement

If a lambda term $M$ reduces to both $N_1$ and $N_2$ (by possibly different sequences of beta-reductions), then there exists a term $N_3$ such that both $N_1$ and $N_2$ reduce to $N_3$ .

$\text{If } M \twoheadrightarrow_\beta N_1 \text{ and } M \twoheadrightarrow_\beta N_2, \text{ then } \exists N_3 \text{ such that } N_1 \twoheadrightarrow_\beta N_3 \text{ and } N_2 \twoheadrightarrow_\beta N_3.$

Intuition

It does not matter which reduction you perform first. All paths eventually converge. If a normal form exists, it is unique. This means that the "answer" a lambda term computes (if it terminates) does not depend on the evaluation strategy.

Proof Sketch

The standard proof uses the Tait-Martin-Lof method of parallel reductions. Define a relation $\Rightarrow$ (parallel reduction) that reduces all redexes simultaneously. Show that $\Rightarrow$ has the diamond property: if $M \Rightarrow N_1$ and $M \Rightarrow N_2$ , then there exists $N_3$ with $N_1 \Rightarrow N_3$ and $N_2 \Rightarrow N_3$ . Then $\twoheadrightarrow_\beta$ is the transitive closure of $\Rightarrow$ , and the diamond property extends to the transitive closure.

Why It Matters

Confluence guarantees that lambda calculus is a well-defined computational model. The result of a computation does not depend on the order of evaluation. This is why pure functional programs are deterministic (in the absence of side effects) and why equational reasoning about programs is sound.

Failure Mode

Confluence holds for the full untyped pure lambda calculus, including terms with fixpoint combinators like $Y$ and non-terminating terms such as $\Omega$ . What fixpoint/recursion combinators break is strong normalization (the property that every reduction reaches a normal form), not confluence: $\Omega$ has no normal form but it also has no diverging pair of reducts. Confluence is genuinely lost when you add non-deterministic features such as mutable state, I/O, or non-confluent rewrite rules. In simply typed and most other typed lambda calculi, both confluence and normalization hold.

report a correction →

The Church-Turing Thesis

Alonzo Church and Alan Turing independently defined computability in the 1930s: Church via lambda calculus, Turing via Turing machines. They proved that the two models compute exactly the same class of functions.

The Church-Turing thesis (not a theorem, but a widely accepted principle) states: every effectively computable function is computable by a Turing machine (equivalently, expressible in lambda calculus). No physically realizable computational model has been shown to exceed this boundary.

Simply Typed Lambda Calculus

The untyped lambda calculus allows self-application ( $x\, x$ ), which leads to non-termination. The simply typed lambda calculus (STLC) restricts terms with types to guarantee termination.

Definition

Simple Types

Types are built from base types ( $\alpha, \beta, \ldots$ ) using the function type constructor:

$\tau ::= \alpha \mid \tau_1 \to \tau_2$

A term $M : \tau_1 \to \tau_2$ is a function taking inputs of type $\tau_1$ and producing outputs of type $\tau_2$ .

In STLC, every well-typed term has a normal form (strong normalization). Self-application $x\, x$ is not typable, because $x$ would need type $\tau \to \sigma$ and type $\tau$ simultaneously, which requires $\tau = \tau \to \sigma$ , an infinite type.

The trade-off: STLC is not Turing-complete. It can only express total (terminating) functions. To recover full computational power, you add recursion (a fixpoint combinator), but then you lose guaranteed termination.

Curry-Howard Correspondence

The Curry-Howard correspondence is the observation that types correspond to propositions and terms correspond to proofs:

Lambda calculus	Logic
Type $A \to B$	Proposition $A \implies B$
Term of type $A \to B$	Proof that $A$ implies $B$
Function application	Modus ponens
Lambda abstraction	Implication introduction

A type is "inhabited" (has a term of that type) if and only if the corresponding proposition is provable. This correspondence is the foundation of proof assistants: to prove a theorem, you construct a term of the corresponding type.

Common Confusions

Watch Out

Lambda calculus is not about Greek letters

The $\lambda$ is just notation for function definition. $\lambda x.\, x + 1$ is the function that adds 1 to its input. In Python, this is lambda x: x + 1. The theoretical significance is that function definition is the only primitive; everything else is derived.

Watch Out

Not every lambda term terminates

$\Omega = (\lambda x.\, x\, x)(\lambda x.\, x\, x)$ beta-reduces to itself, looping forever. The untyped lambda calculus is Turing-complete, which means non-termination is possible. Simply typed lambda calculus guarantees termination but is weaker.

Exercises

ExerciseCore

Problem

Reduce the following lambda term to normal form: $(\lambda x.\, \lambda y.\, x)\, a\, b$ .

ExerciseCore

Problem

Write the Church encoding of the successor function $\text{succ}$ , which takes a Church numeral $\bar{n}$ and returns $\overline{n+1}$ .

ExerciseAdvanced

Problem

Explain why the self-application term $\lambda x.\, x\, x$ cannot be typed in the simply typed lambda calculus.

References

Canonical:

Barendregt, The Lambda Calculus: Its Syntax and Semantics (1984)
Church, "An Unsolvable Problem of Elementary Number Theory" (1936)
Plotkin, "Call-by-name, call-by-value and the lambda-calculus" (Theoretical Computer Science 1975) — call-by-name vs call-by-value semantics
de Bruijn, "Lambda calculus notation with nameless dummies" (1972) — de Bruijn indices

Accessible:

Pierce, Types and Programming Languages (2002), Chapters 5-9
Hindley & Seldin, Lambda-Calculus and Combinators (2008)
Selinger, Lecture Notes on the Lambda Calculus (2013) — open-access modern lecture notes
Krivine, Lambda Calculus: Types and Models (1993)

Next Topics

Dependent type theory: extending STLC so types can depend on values, enabling the Curry-Howard correspondence for full logic
Proof theory and cut-elimination: the structure of proofs as computational objects