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:

1. Variable: $x \in \Lambda$ for any variable $x$.
2. 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$.
3. 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.

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

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 pure lambda calculus. Adding side effects (mutable state, I/O) or unrestricted recursion combinators can break it. In typed lambda calculi, confluence typically still holds, but normalization (every term reaches a normal form) also holds, which is a stronger property.

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

Hint

Reveal Solution

ExerciseCore

Problem

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

Hint

Reveal Solution

ExerciseAdvanced

Problem

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

Hint

Reveal Solution

References

Canonical:

• Barendregt, The Lambda Calculus: Its Syntax and Semantics (1984)
• Church, "An Unsolvable Problem of Elementary Number Theory" (1936)

Accessible:

• Pierce, Types and Programming Languages (2002), Chapters 5-9
• Hindley & Seldin, Lambda-Calculus and Combinators (2008)

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