The λ-calculus · The Lumenary

Lens

MotivationH

Functions as rules

In school a function is often a formula: $x \mapsto x^2 + 1$ . In set theory it becomes a set of ordered pairs. In the early 1930s the American logician Alonzo Church took a third view: a function is a rule that can be applied, and the only things in the world are rules. He wrote $\lambda x.\, x^2 + 1$ for "the function that sends $x$ to $x^2 + 1$ ", and studied what can be done with abstraction ( $\lambda x.\,\dots$ ) and application ( $f\,a$ ) alone.

The answer is: everything that can be computed. Truth values, pairs, natural numbers and arithmetic can be encoded as pure functions; recursion comes from a clever self-application; and the resulting calculus computes exactly the same functions as Turing machines. Python's lambda, JavaScript's arrow functions and every functional programming language descend from it.

It also contains a warning. Type this into Python:

(lambda x: x(x))(lambda x: x(x))

It never finishes (Python gives up with a RecursionError). In the λ-calculus this term is called $\Omega$ , and it reduces to itself forever. So the λ-calculus raises two questions that this lesson answers. If a computation can be carried out in many orders, can different orders give different answers? (No — the Church–Rosser theorem.) And which terms are guaranteed to finish? (Among others, all typed ones.) The lesson assumes induction from proof techniques and some experience of programming.

IntuitionH

Terms as trees, reduction as plugging in

A λ-term is a tree built from variables, applications and abstractions. In $\lambda x.\, x\,y$ the variable $x$ is bound by the $\lambda$ — it is a placeholder, and $\lambda z.\, z\,y$ means the same thing — while $y$ is free. Computing means β-reduction: wherever a function meets an argument, plug the argument in,

(\lambda x.\, M)\, N \;\to\; M[N/x].

The only subtlety is that plugging in must not change the meaning of free variables. Take $K = \lambda x.\, \lambda y.\, x$ , the function that returns a constant function. Applied to a free variable $y$ , naive textual substitution would give

(\lambda x.\, \lambda y.\, x)\, y \;\to\; \lambda y.\, y \qquad \text{(wrong!)}

— the free $y$ has been captured by the inner $\lambda y$ , and a constant function has turned into the identity. The correct answer renames the bound variable first: $\lambda z.\, y$ . Capture-avoiding substitution is easy to state and notoriously easy to get wrong; the Lean formalisation sidesteps it entirely by using de Bruijn indices.

DefinitionsH

Definitions

Definition— λ-terms

Given an infinite set of variables $x, y, z, \dots$ , the λ-terms are generated by

M, N \;::=\; x \;\mid\; (M\, N) \;\mid\; (\lambda x.\, M).

Conventions: application associates to the left ( $M\,N\,L = (M\,N)\,L$ ); the body of a $\lambda$ extends as far right as possible; $\lambda x\, y.\, M$ abbreviates $\lambda x.\, \lambda y.\, M$ .

Definition— free variables and α-equivalence

$\mathrm{FV}(x) = \{x\}$ , $\mathrm{FV}(M\, N) = \mathrm{FV}(M) \cup \mathrm{FV}(N)$ , $\mathrm{FV}(\lambda x.\, M) = \mathrm{FV}(M) \setminus \{x\}$ . A term is closed if it has no free variables. Terms that differ only by renaming bound variables (such as $\lambda x.\, x$ and $\lambda y.\, y$ ) are α-equivalent, and we identify them.

Definition— capture-avoiding substitution

$M[N/x]$ replaces the free occurrences of $x$ in $M$ by $N$ :

$x[N/x] = N$ , and $y[N/x] = y$ for $y \ne x$ ;
$(M_1\, M_2)[N/x] = M_1[N/x]\; M_2[N/x]$ ;
$(\lambda x.\, M)[N/x] = \lambda x.\, M$ ;
$(\lambda y.\, M)[N/x] = \lambda y.\, M[N/x]$ if $y \ne x$ and $y \notin \mathrm{FV}(N)$ ; otherwise first rename $y$ to a variable not free in $M$ or $N$ .

Definition— β-reduction and normal forms

A redex is a term $(\lambda x.\, M)\, N$ ; its contractum is $M[N/x]$ . One-step β-reduction $M \to M'$ contracts one redex anywhere inside $M$ . Write $M \twoheadrightarrow M'$ for zero or more steps, and $M =_\beta M'$ for the equivalence relation generated by $\to$ (β-equality). A term with no redex is in normal form; $M$ has a normal form $N$ if $M \twoheadrightarrow N$ with $N$ normal. $M$ is weakly normalising if it has a normal form, and strongly normalising if every reduction sequence from $M$ is finite.

Definition— de Bruijn indices

Replace each variable occurrence by the number of $\lambda$ 's between it and its binder: $\lambda x.\, \lambda y.\, x$ becomes $\lambda\, \lambda\, 1$ and $\lambda x.\, x\,(\lambda y.\, y\, x)$ becomes $\lambda\, 0\,(\lambda\, 0\, 1)$ . α-equivalent terms become identical, and substitution becomes arithmetic on indices, with no renaming. This is how the Lean formalisation and the Python experiments represent terms.

Worked examplesH

Examples: combinators, data and recursion

Example— Small combinators

$I = \lambda x.\, x$ , $K = \lambda x\, y.\, x$ , $S = \lambda f\, g\, x.\, f\, x\, (g\, x)$ . Then $I\, M \to M$ , $K\, M\, N \twoheadrightarrow M$ , and

S\, K\, K\, M \;\to\; (\lambda g\, x.\, K\, x\, (g\, x))\, K\, M \;\twoheadrightarrow\; K\, M\, (K\, M) \;\twoheadrightarrow\; M,

so $S\,K\,K$ behaves like $I$ . With $\omega = \lambda x.\, x\, x$ and $\Omega = \omega\, \omega$ :

\Omega = (\lambda x.\, x\, x)(\lambda x.\, x\, x) \;\to\; (\lambda x.\, x\, x)(\lambda x.\, x\, x) = \Omega .

Example— Order matters for termination

$K\, I\, \Omega$ has two redexes. Contracting the leftmost-outermost one first: $K\, I\, \Omega \to (\lambda y.\, I)\, \Omega \to I$ , a normal form in two steps. Contracting $\Omega$ first does nothing: $K\, I\, \Omega \to K\, I\, \Omega$ , forever. A term can have a normal form and an infinite reduction. Normal order — always contract the leftmost-outermost redex — finds the normal form whenever there is one (the standardisation theorem, below); applicative order — evaluate arguments first, as most programming languages do — can loop.

Example— Booleans and pairs

A truth value is a choice: $\mathsf{TRUE} = \lambda x\, y.\, x$ picks the first of two arguments, $\mathsf{FALSE} = \lambda x\, y.\, y$ the second. Then "if $b$ then $M$ else $N$ " is just $b\, M\, N$ , and

\mathsf{AND} = \lambda p\, q.\, p\, q\, p, \qquad \mathsf{OR} = \lambda p\, q.\, p\, p\, q, \qquad \mathsf{NOT} = \lambda p.\, p\, \mathsf{FALSE}\, \mathsf{TRUE}.

For instance $\mathsf{AND}\, \mathsf{TRUE}\, \mathsf{FALSE} \twoheadrightarrow \mathsf{TRUE}\, \mathsf{FALSE}\, \mathsf{TRUE} \twoheadrightarrow \mathsf{FALSE}$ . A pair is a function waiting for a selector: $\mathsf{PAIR} = \lambda a\, b\, f.\, f\, a\, b$ , $\mathsf{FST} = \lambda p.\, p\, \mathsf{TRUE}$ , $\mathsf{SND} = \lambda p.\, p\, \mathsf{FALSE}$ .

Example— Church numerals

The number $n$ is "do something $n$ times": $\bar n = \lambda f\, x.\, f^n\, x$ , so $\bar 0 = \lambda f\, x.\, x$ and $\bar 3 = \lambda f\, x.\, f\,(f\,(f\, x))$ . Arithmetic is composition of iterations:

\mathsf{SUCC} = \lambda n\, f\, x.\, f\,(n\, f\, x), \quad \mathsf{PLUS} = \lambda m\, n\, f\, x.\, m\, f\,(n\, f\, x), \quad \mathsf{TIMES} = \lambda m\, n\, f.\, m\,(n\, f), \quad \mathsf{EXP} = \lambda m\, n.\, n\, m .

In normal order, $\mathsf{PLUS}\, \bar 2\, \bar 3 \twoheadrightarrow \bar 5$ takes six steps:

\begin{aligned} \mathsf{PLUS}\, \bar 2\, \bar 3 &\twoheadrightarrow \lambda f\, x.\, \bar 2\, f\,(\bar 3\, f\, x) && \text{(2 steps)}\\ &\to \lambda f\, x.\, (\lambda x'.\, f\,(f\, x'))\,(\bar 3\, f\, x) \to \lambda f\, x.\, f\,(f\,(\bar 3\, f\, x))\\ &\twoheadrightarrow \lambda f\, x.\, f\,(f\,(f\,(f\,(f\, x)))) = \bar 5 && \text{(2 more steps).} \end{aligned}

Testing for zero is $\mathsf{ISZERO} = \lambda n.\, n\, (\lambda z.\, \mathsf{FALSE})\, \mathsf{TRUE}$ . The predecessor is harder — Church at first doubted that it could be defined; Stephen Kleene found it by iterating on pairs, $(0, 0) \mapsto (0, 1) \mapsto (1, 2) \mapsto \cdots \mapsto (n - 1, n)$ , then taking the first component:

\mathsf{PRED} = \lambda n.\, \mathsf{FST}\, \big(n\, (\lambda p.\, \mathsf{PAIR}\, (\mathsf{SND}\, p)\, (\mathsf{SUCC}\, (\mathsf{SND}\, p)))\, (\mathsf{PAIR}\, \bar 0\, \bar 0)\big).

Example— Recursion by self-application

Curry's paradoxical combinator $Y = \lambda f.\, (\lambda x.\, f\,(x\, x))\,(\lambda x.\, f\,(x\, x))$ and Turing's $\Theta = A\, A$ with $A = \lambda x\, y.\, y\,(x\, x\, y)$ produce fixed points (Theorem 1). To define the factorial, solve the recursive equation $\mathsf{fact} = F\, \mathsf{fact}$ for

F = \lambda r\, n.\, \mathsf{ISZERO}\, n\, \bar 1\, \big(\mathsf{TIMES}\, n\, (r\, (\mathsf{PRED}\, n))\big),

by $\mathsf{FACT} = Y\, F$ . Then $\mathsf{FACT}\, \bar 3 \twoheadrightarrow \bar 6$ — after 1477 normal-order steps in the experiment below. The same trick with $F = I$ gives $Y\, I \twoheadrightarrow \omega'\,\omega'$ with $\omega' = \lambda x.\, I\,(x\, x)$ , a term with no normal form: recursion and non-termination are two sides of one coin.

ProofH

The main theorems

Theorem— Theorem 1 (fixed points)

For every term $F$ there is a term $X$ with $F\, X =_\beta X$ . In fact $\Theta\, F \twoheadrightarrow F\,(\Theta\, F)$ , and $Y\, F$ and $F\,(Y\, F)$ have a common reduct.

Proof

With $A = \lambda x\, y.\, y\,(x\, x\, y)$ : $\Theta\, F = A\, A\, F \to (\lambda y.\, y\,(A\, A\, y))\, F \to F\,(A\, A\, F) = F\,(\Theta\, F)$ . For $Y$ , let $W = \lambda x.\, F\,(x\, x)$ . Then $Y\, F \to W\, W \to F\,(W\, W)$ , and also $F\,(Y\, F) \to F\,(W\, W)$ . So $X = \Theta\, F$ (or $Y\, F$ ) works.

∎

Now the central theorem. The naive approach — show that two one-step reducts can be joined in one step each, then tile — fails, because contracting one redex can duplicate another: from $(\lambda x.\, x\, x)(I\, z)$ one step gives $(I\, z)(I\, z)$ and another gives $(\lambda x.\, x\, x)\, z$ , and joining them at $z\, z$ takes two steps on the left. The cure (Tait and Martin-Löf) is to reduce in parallel.

Definition— parallel reduction

$M \Rightarrow M'$ is defined inductively: $x \Rightarrow x$ ; if $M \Rightarrow M'$ then $\lambda x.\, M \Rightarrow \lambda x.\, M'$ ; if $M \Rightarrow M'$ and $N \Rightarrow N'$ then $M\, N \Rightarrow M'\, N'$ and $(\lambda x.\, M)\, N \Rightarrow M'[N'/x]$ . Intuitively: contract any set of redexes already present, all at once.

Theorem— Lemma A

(i) $M \Rightarrow M$ . (ii) If $M \to N$ then $M \Rightarrow N$ . (iii) If $M \Rightarrow N$ then $M \twoheadrightarrow N$ . Hence $\twoheadrightarrow$ is the reflexive–transitive closure of $\Rightarrow$ .

Proof

(i) By induction on $M$ . (ii) By induction on the position of the contracted redex, using (i) for the parts that do not change. (iii) By induction on the derivation of $M \Rightarrow N$ : the congruence cases chain reductions of the parts, and the last case reduces $M \twoheadrightarrow M'$ and $N \twoheadrightarrow N'$ inside $(\lambda x.\, M)\, N$ and then contracts. Finally, (ii) and (iii) give $\to \;\subseteq\; \Rightarrow \;\subseteq\; \twoheadrightarrow$ , and taking reflexive–transitive closures of all three gives $\twoheadrightarrow = \Rightarrow^\ast$ .

∎

We use the substitution lemma: if $x \ne y$ and $x \notin \mathrm{FV}(L)$ , then $M[N/x][L/y] = M[L/y][N[L/y]/x]$ . (Induction on $M$ : for $M = x$ both sides are $N[L/y]$ ; for $M = y$ both are $L$ , using $x \notin \mathrm{FV}(L)$ ; the other cases are immediate, choosing bound variables fresh.)

Theorem— Lemma B (parallel reduction respects substitution)

If $M \Rightarrow M'$ and $N \Rightarrow N'$ , then $M[N/x] \Rightarrow M'[N'/x]$ .

Proof

Induction on the derivation of $M \Rightarrow M'$ , with bound variables chosen different from $x$ and not free in $N, N'$ . Variable case: if $M = x$ the claim is $N \Rightarrow N'$ ; otherwise both sides are the same variable. The abstraction and application cases follow from the induction hypothesis. In the remaining case $M = (\lambda y.\, P)\, Q$ and $M' = P'[Q'/y]$ with $P \Rightarrow P'$ and $Q \Rightarrow Q'$ . Then

M[N/x] = (\lambda y.\, P[N/x])\,(Q[N/x]) \;\Rightarrow\; P'[N'/x]\,\big[Q'[N'/x]/y\big] = P'[Q'/y][N'/x] = M'[N'/x],

using the induction hypothesis for $P$ and $Q$ , then the substitution lemma (valid because $y \notin \mathrm{FV}(N')$ ).

∎

Definition— complete development

$M^\ast$ contracts every redex of $M$ : $x^\ast = x$ ; $(\lambda x.\, M)^\ast = \lambda x.\, M^\ast$ ; $(M\, N)^\ast = M^\ast\, N^\ast$ if $M$ is not an abstraction; $((\lambda x.\, M)\, N)^\ast = M^\ast[N^\ast/x]$ .

Theorem— Lemma C (triangle property; Takahashi)

If $M \Rightarrow N$ then $N \Rightarrow M^\ast$ . Consequently $\Rightarrow$ has the diamond property: if $M \Rightarrow N_1$ and $M \Rightarrow N_2$ , then $N_1 \Rightarrow M^\ast$ and $N_2 \Rightarrow M^\ast$ .

Proof

Induction on the derivation of $M \Rightarrow N$ . Variables and abstractions are immediate. If $M = (\lambda x.\, P)\, Q$ and $N = P'[Q'/x]$ with $P \Rightarrow P'$ , $Q \Rightarrow Q'$ , then by induction $P' \Rightarrow P^\ast$ and $Q' \Rightarrow Q^\ast$ , and Lemma B gives $N \Rightarrow P^\ast[Q^\ast/x] = M^\ast$ . If $M = P\, Q$ and $N = P'\, Q'$ with $P \Rightarrow P'$ , $Q \Rightarrow Q'$ : when $P$ is not an abstraction, $M^\ast = P^\ast\, Q^\ast$ and the induction hypotheses give $N \Rightarrow M^\ast$ . When $P = \lambda x.\, P_0$ , the only rule producing $P \Rightarrow P'$ makes $P' = \lambda x.\, P_0'$ with $P_0 \Rightarrow P_0'$ , and the induction hypothesis $P' \Rightarrow P^\ast = \lambda x.\, P_0^\ast$ gives $P_0' \Rightarrow P_0^\ast$ . So $N = (\lambda x.\, P_0')\, Q' \Rightarrow P_0^\ast[Q^\ast/x] = M^\ast$ by the last rule of $\Rightarrow$ .

∎

Theorem— Lemma D (diamond implies confluence)

If a relation $\triangleright$ has the diamond property, then so does its reflexive–transitive closure $\triangleright^\ast$ : if $a \triangleright^\ast b$ and $a \triangleright^\ast c$ , there is $d$ with $b \triangleright^\ast d$ and $c \triangleright^\ast d$ .

Proof

First the strip lemma: if $a \triangleright b$ and $a \triangleright^\ast c$ , then there is $d$ with $b \triangleright^\ast d$ and $c \triangleright d$ . By induction on the length of $a \triangleright^\ast c$ : for length $0$ take $d = b$ ; if $a \triangleright^\ast c' \triangleright c$ and (by induction) $b \triangleright^\ast d'$ , $c' \triangleright d'$ , the diamond property applied to $c' \triangleright d'$ and $c' \triangleright c$ gives $e$ with $d' \triangleright e$ and $c \triangleright e$ ; then $b \triangleright^\ast e$ . Now induct on the length of $a \triangleright^\ast b$ in the same way, using the strip lemma for each step. Geometrically: the two reductions span a grid, and each square is filled by one diamond.

∎

Theorem— Theorem 2 (Church–Rosser)

β-reduction is confluent: if $M \twoheadrightarrow N_1$ and $M \twoheadrightarrow N_2$ , then there is a term $L$ with $N_1 \twoheadrightarrow L$ and $N_2 \twoheadrightarrow L$ .

Proof

By Lemma A, $\twoheadrightarrow$ equals $\Rightarrow^\ast$ . By Lemma C, $\Rightarrow$ has the diamond property, so by Lemma D, $\Rightarrow^\ast$ is confluent.

∎

Theorem— Corollary 3 (uniqueness of normal forms; consistency)

If $M =_\beta N$ , then $M$ and $N$ have a common reduct.
A term has at most one normal form.
Distinct normal forms are not β-equal. In particular $\mathsf{TRUE} \ne_\beta \mathsf{FALSE}$ and $K \ne_\beta I$ , so β-equality does not identify all terms.

Proof

(1) By induction on a chain $M = M_0, M_1, \dots, M_k = N$ in which each consecutive pair is related by $\to$ or $\leftarrow$ : if $M_0$ and $M_{k-1}$ have a common reduct $L$ , then either $M_k \to M_{k-1}$ , so $L$ is also a reduct of $M_k$ , or $M_{k-1} \to M_k$ , and Church–Rosser applied to $M_{k-1} \twoheadrightarrow L$ and $M_{k-1} \to M_k$ gives a common reduct of $L$ and $M_k$ , hence of $M_0$ and $M_k$ . (2) If $N_1, N_2$ are normal forms of $M$ , Church–Rosser gives $L$ with $N_i \twoheadrightarrow L$ ; a normal form reduces only to itself, so $N_1 = L = N_2$ . (3) follows from (1) in the same way.

∎

So the value of a computation, if it has one, does not depend on the order of evaluation. Two further classical theorems complete the picture; we state them with references.

Theorem— Theorem 4 (standardisation, stated)

If $M$ has a normal form, then normal-order reduction (always contracting the leftmost-outermost redex) reaches it. (Curry and Feys 1958; see Barendregt 1984 or Hindley and Seldin 2008.)

Theorem— Theorem 5 (λ-definability and undecidability, stated)

A partial function $\N^k \rightharpoonup \N$ is λ-definable on Church numerals if and only if it is partial recursive, if and only if it is computable by a Turing machine (Kleene 1936, Turing 1937). Consequently there is no algorithm that decides whether a λ-term has a normal form, or whether two λ-terms are β-equal (Church 1936).

The idea of the first equivalence: primitive recursion is iteration on pairs, exactly as in $\mathsf{PRED}$ , and unbounded search ("the least $n$ with $f(n) = 0$ ") is a recursive definition, solved with $Y$ . Conversely, β-reduction is a mechanical process a Turing machine can simulate. See computability.

Types tame the calculus

The simply typed λ-calculus attaches a type to every variable. Types are built from base types by $A \to B$ ; the rules are: a variable $x{:}A$ has type $A$ ; if $M : A \to B$ and $N : A$ then $M\, N : B$ ; and if $M : B$ assuming $x : A$ , then $\lambda x{:}A.\, M : A \to B$ . So $\lambda x{:}A.\, x : A \to A$ and $\lambda x{:}A.\, \lambda y{:}B.\, x : A \to B \to A$ , but $\omega = \lambda x.\, x\, x$ has no type: $x\, x$ would need $x : A \to B$ and $x : A$ at once, i.e. $A = A \to B$ , impossible since $A \to B$ is strictly bigger than $A$ . Types are preserved by reduction (subject reduction, a consequence of a substitution lemma for typings).

The degree of a redex $(\lambda x{:}A.\, M)\, N$ is the size (number of arrows) of the type $A \to B$ of the function $\lambda x{:}A.\, M$ .

Theorem— Theorem 6 (weak normalisation; Turing)

Every simply typed λ-term has a normal form.

Proof

For a term $M$ let $d$ be the maximum degree of its redexes and $n$ the number of redexes of degree $d$ ; we induct on $(d, n)$ in lexicographic order. If $M$ has no redex we are done. Otherwise choose a redex $R = (\lambda x{:}A.\, P)\, Q$ of degree $d$ that is rightmost among those of degree $d$ (its $\lambda$ comes last in the written term). Every redex inside $Q$ starts to the right of $R$ 's $\lambda$ , so $Q$ contains no redex of degree $d$ . Contract $R$ to $P[Q/x]$ and look at the redexes of the result:

redexes outside $R$ , and redexes inside $P$ , survive exactly once each, with the same degree (substitution does not copy $P$ );
redexes inside $Q$ may be copied many times, but all have degree $< d$ ;
new redexes can be created only in two ways: where $P$ contains $x\, L$ and $Q$ is an abstraction, giving $Q\, L'$ of degree $|A| < d$ ; or where $R$ itself was applied, $R\, L$ , and $P[Q/x]$ is an abstraction, giving a redex of degree $|B| < d$ , where $A \to B$ is the type of $\lambda x{:}A.\, P$ .

So the redex $R$ of degree $d$ is gone and no redex of degree $\ge d$ was created: either $n$ drops by one or, if $n$ was $1$ , the maximal degree $d$ drops. By induction the process reaches a normal form.

∎

Theorem— Theorem 7 (strong normalisation and expressive power, stated)

Every simply typed λ-term is strongly normalising: every reduction sequence is finite (Tait 1967, by "reducibility candidates"; see Girard, Lafont and Taylor 1989). The price is expressive power: on Church numerals of type $(o \to o) \to o \to o$ , the simply typed λ-calculus defines exactly the extended polynomials — functions built from constants, addition, multiplication and a test for zero (Schwichtenberg 1976). Not even subtraction or exponentiation in general is definable at that type.

So typed programs always terminate, but some computable functions cannot be typed this way — an instance of a general trade-off: a total language cannot define all computable total functions. Under the Curry–Howard correspondence, types are propositions and typed terms are proofs; normalisation of terms is normalisation of proofs. That is the subject of type theory and propositions as types.

Formal mathematicsF

The λ-calculus in Lean

The Lean module uses de Bruijn indices, so α-equivalent terms are equal and substitution never captures. Substitutions are simultaneous: subst σ t replaces each free variable n by σ n, and going under a binder uses up σ, which shifts the substituted terms. The β-rule contracts (λ t) s to inst t s.

TermLean 4Formally verified

/-- Untyped λ-terms with **de Bruijn indices**: `var n` refers to the variable bound by the
`n`-th enclosing `lam`, counting outwards from `0`. So `λx. λy. x` is `lam (lam (var 1))`, and
α-equivalent terms such as `λx. x` and `λy. y` are the same term `lam (var 0)`. -/
inductive Term where
  | var : Nat → Term
  | app : Term → Term → Term
  | lam : Term → Term
  deriving DecidableEq, Repr

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

upLean 4Formally verified

/-- Lift a substitution `σ` (a term for each free variable) under one binder: the new bound
variable stays put, and the substituted terms are shifted so that their free variables skip the
new binder. This shift is exactly what makes substitution **capture-avoiding**. -/
def up (σ : Nat → Term) : Nat → Term
  | 0 => var 0
  | n + 1 => rename Nat.succ (σ n)

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

substLean 4Formally verified

/-- Simultaneous capture-avoiding substitution: replace each free variable `n` by `σ n`. -/
def subst (σ : Nat → Term) : Term → Term
  | var n => σ n
  | app s t => app (subst σ s) (subst σ t)
  | lam t => lam (subst (up σ) t)

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

instLean 4Formally verified

/-- `inst t s` is `t[s/x]` for the variable `x` bound by an enclosing `λ`: index `0` becomes
`s`, and the other free indices drop by one because that `λ` has disappeared. -/
def inst (t s : Term) : Term :=
  subst (scons s var) t

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

The algebra of substitution is proved from scratch. Two of the fusion laws, including the substitution lemma used in Lemma B:

subst_substLean 4Proved here from basic factsFormally verified

/-- **Substitution is associative**: substituting `σ` and then `τ` is substituting the
composite `n ↦ subst τ (σ n)`. -/
theorem subst_subst (t : Term) : ∀ (σ τ : Nat → Term),
    subst τ (subst σ t) = subst (subst τ ∘ σ) t := by
  induction t with
  | var n => intro σ τ; rfl
  | app s t ihs iht => intro σ τ; simp [subst, ihs, iht]
  | lam t ih =>
    intro σ τ
    simp only [subst, ih]
    congr 2
    funext n
    cases n with
    | zero => rfl
    | succ k =>
      show subst (up τ) (rename Nat.succ (σ k)) = rename Nat.succ (subst τ (σ k))
      rw [subst_rename, rename_subst]
      rfl

Axioms used: propext, Quot.soundformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

subst_instLean 4Proved here from basic factsFormally verified

/-- **The substitution lemma**: `(t[s/x])σ = (tσ')[sσ/x]`, where `σ'` is `σ` lifted under the
binder of `x`. -/
theorem subst_inst (σ : Nat → Term) (t s : Term) :
    subst σ (inst t s) = inst (subst (up σ) t) (subst σ s) := by
  simp only [inst, subst_subst]
  congr 1
  funext n
  cases n with
  | zero => rfl
  | succ k =>
    show σ k = subst (scons (subst σ s) var) (rename Nat.succ (σ k))
    rw [subst_rename, subst_var]
    intro m
    rfl

Axioms used: propext, Quot.soundformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

β-reduction, normal forms and Ω. $\Omega$ reduces only to itself, so it has no normal form:

StepLean 4Formally verified

/-- One step of **β-reduction**, anywhere in a term: `(λx. t) s → t[s/x]`, also inside
applications and under λ. -/
inductive Step : Term → Term → Prop where
  | beta (t s : Term) : Step (app (lam t) s) (inst t s)
  | appL {s s' : Term} (t : Term) : Step s s' → Step (app s t) (app s' t)
  | appR (s : Term) {t t' : Term} : Step t t' → Step (app s t) (app s t')
  | lam {t t' : Term} : Step t t' → Step (lam t) (lam t')

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

NormalLean 4Formally verified

/-- A term is in **normal form** if no β-step applies to it. -/
def Normal (t : Term) : Prop :=
  ∀ u, ¬ Step t u

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

bigOmegaLean 4Formally verified

/-- `Ω = ω ω = (λx. x x)(λx. x x)`. -/
def bigOmega : Term := app omega omega

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

bigOmega_stepLean 4Proved here from basic factsFormally verified

/-- **Ω reduces to itself and to nothing else.** The only redex is the whole term, and
contracting it substitutes `ω` for `x` in `x x`, giving `ω ω` back. -/
theorem bigOmega_step (u : Term) : Step bigOmega u ↔ u = bigOmega := by
  constructor
  · intro h
    cases h with
    | beta => rfl
    | appL _ h' => exact absurd h' (omega_normal _)
    | appR _ h' => exact absurd h' (omega_normal _)
  · rintro rfl
    exact Step.beta _ _

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

bigOmega_no_normal_formLean 4Proved here from basic factsFormally verified

/-- **Ω has no normal form**: everything it reduces to is Ω, and Ω is not normal. So the untyped
λ-calculus has non-terminating computations. -/
theorem bigOmega_no_normal_form : ¬ ∃ u, ReflTransGen Step bigOmega u ∧ Normal u := by
  rintro ⟨u, hu, hn⟩
  have only : ∀ w, ReflTransGen Step bigOmega w → w = bigOmega := by
    intro w hw
    induction hw with
    | refl => rfl
    | tail _ hstep ih =>
      subst ih
      exact (bigOmega_step _).1 hstep
  have := only u hu
  subst this
  exact hn bigOmega ((bigOmega_step bigOmega).2 rfl)

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

Fixed points (Theorem 1).

thetaLean 4Formally verified

/-- **Turing's fixed-point combinator** `Θ = A A` with `A = λx. λy. y (x x y)`. -/
def theta : Term :=
  app (lam (lam (app (var 0) (app (app (var 1) (var 1)) (var 0)))))
    (lam (lam (app (var 0) (app (app (var 1) (var 1)) (var 0)))))

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

theta_fixed_pointLean 4Proved here from basic factsFormally verified

/-- **`Θ F ↠ F (Θ F)` for every term `F`** — in two β-steps. This is how the untyped calculus
defines recursive functions: a solution of `f = F f`. -/
theorem theta_fixed_point (F : Term) : ReflTransGen Step (app theta F) (app F (app theta F)) := by
  refine ReflTransGen.head (Step.appL F (Step.beta _ _)) ?_
  exact ReflTransGen.single (Step.beta _ _)

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

curryYLean 4Formally verified

/-- **Curry's paradoxical combinator** `Y = λf. (λx. f (x x)) (λx. f (x x))`. -/
def curryY : Term :=
  lam (app (lam (app (var 1) (app (var 0) (var 0))))
    (lam (app (var 1) (app (var 0) (var 0)))))

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

curryY_fixed_pointLean 4Proved here from basic factsFormally verified

/-- **`Y F` and `F (Y F)` reduce to a common term**, so they are β-equal. (Unlike `Θ`, `Y F`
does not reduce to `F (Y F)` itself.) With `W = λx. F (x x)`: `Y F → W W → F (W W)` and
`F (Y F) → F (W W)`. -/
theorem curryY_fixed_point (F : Term) :
    ∃ N, ReflTransGen Step (app curryY F) N ∧ ReflTransGen Step (app F (app curryY F)) N := by
  let W : Term := lam (app (rename Nat.succ F) (app (var 0) (var 0)))
  have h1 : Step (app curryY F) (app W W) := Step.beta _ _
  have h2 : Step (app W W) (app F (app W W)) := by
    have e : inst (app (rename Nat.succ F) (app (var 0) (var 0))) W = app F (app W W) := by
      simp only [inst, subst]
      rw [subst_rename, subst_var]
      · rfl
      · intro n
        rfl
    rw [← e]
    exact Step.beta _ _
  exact ⟨app F (app W W), ReflTransGen.head h1 (ReflTransGen.single h2),
    ReflTransGen.single (Step.appR F h1)⟩

Axioms used: propext, Quot.soundformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

Church numerals, computed by the kernel. A normal-order evaluator is proved sound (each step is a β-step) and complete for normal forms (when it stops, the term is normal). Then decide makes Lean's kernel run it, and soundness turns the run into a proof of $\mathsf{PLUS}\, \bar 2\, \bar 3 \twoheadrightarrow \bar 5$ .

churchLean 4Formally verified

/-- The **Church numeral** `n̄ = λf. λx. fⁿ x`: the number `n` as "do something `n` times". -/
def church (n : Nat) : Term := lam (lam (iterate n))

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

plusLean 4Formally verified

/-- `plus = λm. λn. λf. λx. m f (n f x)`: do `f` `n` times, then `m` more times. -/
def plus : Term :=
  lam (lam (lam (lam (app (app (var 3) (var 1)) (app (app (var 2) (var 1)) (var 0))))))

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

stepNOLean 4Formally verified

/-- One step of **normal-order** (leftmost-outermost) reduction, or `none` if the term is
normal: contract the head redex if there is one, otherwise reduce inside, left to right. -/
def stepNO : Term → Option Term
  | var _ => none
  | lam t => (stepNO t).map lam
  | app (lam t) s => some (inst t s)
  | app (var n) t => (stepNO t).map (app (var n))
  | app (app s₁ s₂) t =>
    match stepNO (app s₁ s₂) with
    | some s' => some (app s' t)
    | none => (stepNO t).map (app (app s₁ s₂))

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

stepNO_soundLean 4Proved here from basic factsFormally verified

/-- **The evaluator is sound**: every step it takes is a β-step. -/
theorem stepNO_sound (t : Term) : ∀ u, stepNO t = some u → Step t u := by
  induction t with
  | var n => intro u h; cases h
  | lam t ih =>
    intro u h
    simp only [stepNO, Option.map_eq_some_iff] at h
    obtain ⟨t', ht', rfl⟩ := h
    exact Step.lam (ih t' ht')
  | app s t ihs iht =>
    intro u h
    cases s with
    | var n =>
      simp only [stepNO, Option.map_eq_some_iff] at h
      obtain ⟨t', ht', rfl⟩ := h
      exact Step.appR _ (iht t' ht')
    | lam s₀ =>
      simp only [stepNO, Option.some.injEq] at h
      subst h
      exact Step.beta _ _
    | app s₁ s₂ =>
      simp only [stepNO] at h
      split at h
      · rename_i s' hs'
        simp only [Option.some.injEq] at h
        subst h
        exact Step.appL _ (ihs s' hs')
      · simp only [Option.map_eq_some_iff] at h
        obtain ⟨t', ht', rfl⟩ := h
        exact Step.appR _ (iht t' ht')

Axioms used: propext, Quot.soundformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

stepNO_noneLean 4Proved here from basic factsFormally verified

/-- **When the evaluator stops, the term is normal**: if normal order finds no redex, there is
no redex at all. -/
theorem stepNO_none (t : Term) : stepNO t = none → Normal t := by
  induction t with
  | var n => intro _ u h; cases h
  | lam t ih =>
    intro h u hu
    simp only [stepNO, Option.map_eq_none_iff] at h
    cases hu with
    | lam h' => exact ih h _ h'
  | app s t ihs iht =>
    intro h u hu
    cases s with
    | var n =>
      simp only [stepNO, Option.map_eq_none_iff] at h
      cases hu with
      | appL _ h' => cases h'
      | appR _ h' => exact iht h _ h'
    | lam s₀ => simp [stepNO] at h
    | app s₁ s₂ =>
      simp only [stepNO] at h
      split at h
      · cases h
      · rename_i hs
        simp only [Option.map_eq_none_iff] at h
        cases hu with
        | appL _ h' => exact ihs hs _ h'
        | appR _ h' => exact iht h _ h'

Axioms used: propextformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

two_plus_threeLean 4Proved here from basic factsFormally verified

/-- **`plus 2̄ 3̄ ↠ 5̄`**. The kernel runs the evaluator (6 normal-order steps) and checks that
the result is the Church numeral `5̄`; soundness turns the run into a β-reduction. -/
theorem two_plus_three : ReflTransGen Step (app (app plus (church 2)) (church 3)) (church 5) := by
  have h : normalize 20 (app (app plus (church 2)) (church 3)) = church 5 := by decide
  rw [← h]
  exact normalize_steps 20 _

Axioms used: propext, Quot.soundformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

two_times_threeLean 4Proved here from basic factsFormally verified

/-- **`times 2̄ 3̄ ↠ 6̄`**, computed the same way. -/
theorem two_times_three : ReflTransGen Step (app (app times (church 2)) (church 3)) (church 6) := by
  have h : normalize 30 (app (app times (church 2)) (church 3)) = church 6 := by decide
  rw [← h]
  exact normalize_steps 30 _

Axioms used: propext, Quot.soundformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

Lemma D, abstractly, proved from scratch and compared with Mathlib's Relation.church_rosser:

DiamondLean 4Formally verified

/-- A relation has the **diamond property** if any two one-step reducts of a term can be
joined by one more step on each side. -/
def Diamond : Prop :=
  ∀ a b c, r a b → r a c → ∃ d, r b d ∧ r c d

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

stripLean 4Proved here from basic factsFormally verified

/-- **The strip lemma**: if `r` has the diamond property, a single `r`-step and a many-step
`r`-reduction from the same term can be joined (one step on the far side, many on the other).
Induction along the many-step reduction, tiling one diamond at a time. -/
theorem strip (hd : Diamond r) {a b c : α} (hab : r a b) (hac : ReflTransGen r a c) :
    ∃ d, ReflTransGen r b d ∧ r c d := by
  induction hac with
  | refl => exact ⟨b, ReflTransGen.refl, hab⟩
  | tail _ hcc' ih =>
    obtain ⟨d, hbd, hcd⟩ := ih
    obtain ⟨e, hde, hc'e⟩ := hd _ _ _ hcd hcc'
    exact ⟨e, hbd.tail hde, hc'e⟩

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

diamond_confluentLean 4Proved here from basic factsFormally verified

/-- **Diamond implies confluence**: if `r` has the diamond property, then any two many-step
reducts of a term have a common many-step reduct. Induction along one reduction, using the
strip lemma for each of its steps. -/
theorem diamond_confluent (hd : Diamond r) {a b c : α} (hab : ReflTransGen r a b)
    (hac : ReflTransGen r a c) : ∃ d, ReflTransGen r b d ∧ ReflTransGen r c d := by
  induction hab with
  | refl => exact ⟨c, hac, ReflTransGen.refl⟩
  | tail _ hbb' ih =>
    obtain ⟨d, hbd, hcd⟩ := ih
    obtain ⟨e, hb'e, hde⟩ := strip hd hbb' hbd
    exact ⟨e, hb'e, hcd.tail hde⟩

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

church_rosser_libraryLean 4Applies a library theoremFormally verified

/-- The same abstract fact from Mathlib, in a slightly stronger form (Mathlib's
`Relation.church_rosser` only needs the joining step on one side to be optional). -/
theorem church_rosser_library (hd : Diamond r) {a b c : α} (hab : ReflTransGen r a b)
    (hac : ReflTransGen r a c) : Join (ReflTransGen r) b c :=
  Relation.church_rosser (fun a b c hab hac =>
    let ⟨d, hbd, hcd⟩ := hd a b c hab hac
    ⟨d, ReflGen.single hbd, ReflTransGen.single hcd⟩) hab hac

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

The Church–Rosser theorem (Theorem 2 and Corollary 3), following Lemmas A–C: parallel reduction, its substitution lemma, complete developments and the triangle property.

ParLean 4Formally verified

/-- **Parallel reduction** `t ⇒ t'` (Tait, Martin-Löf): contract any set of redexes already
present in `t`, all at once. Unlike `→`, it has the diamond property. -/
inductive Par : Term → Term → Prop where
  | var (n : Nat) : Par (var n) (var n)
  | app {s s' t t' : Term} : Par s s' → Par t t' → Par (app s t) (app s' t')
  | lam {t t' : Term} : Par t t' → Par (lam t) (lam t')
  | beta {t t' s s' : Term} : Par t t' → Par s s' → Par (app (lam t) s) (inst t' s')

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

par_substLean 4Proved here from basic factsFormally verified

/-- **Parallel reduction is preserved by substitution**: if `t ⇒ t'` and `σ n ⇒ τ n` for every
variable `n`, then `tσ ⇒ t'τ`. The β case is the substitution lemma `subst_inst`. -/
theorem par_subst {t t' : Term} (h : Par t t') :
    ∀ σ τ, (∀ n, Par (σ n) (τ n)) → Par (subst σ t) (subst τ t') := by
  induction h with
  | var n => intro σ τ hστ; exact hστ n
  | app _ _ ihs iht => intro σ τ hστ; exact Par.app (ihs σ τ hστ) (iht σ τ hστ)
  | lam _ ih =>
    intro σ τ hστ
    refine Par.lam (ih _ _ ?_)
    intro n
    cases n with
    | zero => exact Par.var 0
    | succ k => exact par_rename (hστ k) _
  | beta _ _ iht ihs =>
    intro σ τ hστ
    rw [subst_inst]
    refine Par.beta (iht _ _ ?_) (ihs σ τ hστ)
    intro n
    cases n with
    | zero => exact Par.var 0
    | succ k => exact par_rename (hστ k) _

Axioms used: propext, Quot.soundformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

cdLean 4Formally verified

/-- **The complete development** `t*` (Takahashi): contract *every* redex present in `t`,
innermost information first. -/
def cd : Term → Term
  | var n => var n
  | lam t => lam (cd t)
  | app (lam t) s => inst (cd t) (cd s)
  | app (var n) t => app (var n) (cd t)
  | app (app s₁ s₂) t => app (cd (app s₁ s₂)) (cd t)

Axioms used: No axiomsformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

triangleLean 4Proved here from basic factsFormally verified

/-- **The triangle property**: if `t ⇒ u`, then `u ⇒ t*`. Every parallel reduct of `t` can
catch up with the complete development of `t` in one more parallel step. -/
theorem triangle {t u : Term} (h : Par t u) : Par u (cd t) := by
  induction h with
  | var n => exact Par.var n
  | lam _ ih => exact Par.lam ih
  | beta _ _ iht ihs => exact par_inst iht ihs
  | @app s s' t t' hs _ ihs iht =>
    cases s with
    | var n => exact Par.app ihs iht
    | app s₁ s₂ => exact Par.app ihs iht
    | lam s₀ =>
      cases hs with
      | lam hs₀ =>
        cases ihs with
        | lam ih₀ => exact Par.beta ih₀ iht

Axioms used: propext, Quot.soundformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

par_diamondLean 4Proved here from basic factsFormally verified

/-- Parallel reduction has the **diamond property**: two parallel reducts of `t` both reduce in
one parallel step to the complete development `t*`. -/
theorem par_diamond : Diamond Par :=
  fun t _ _ hu hv => ⟨cd t, triangle hu, triangle hv⟩

Axioms used: propext, Quot.soundformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

church_rosserLean 4Proved here from basic factsFormally verified

/-- **The Church–Rosser theorem** (Church and Rosser, 1936): β-reduction is confluent. If
`t ↠ u` and `t ↠ v`, there is a `w` with `u ↠ w` and `v ↠ w`. Proof: confluence of parallel
reduction (diamond ⇒ confluence), transported along `↠ = ⇒*`. -/
theorem church_rosser {t u v : Term} (hu : ReflTransGen Step t u) (hv : ReflTransGen Step t v) :
    ∃ w, ReflTransGen Step u w ∧ ReflTransGen Step v w := by
  obtain ⟨w, huw, hvw⟩ :=
    diamond_confluent par_diamond (steps_iff_par_steps.1 hu) (steps_iff_par_steps.1 hv)
  exact ⟨w, steps_iff_par_steps.2 huw, steps_iff_par_steps.2 hvw⟩

Axioms used: propext, Quot.soundformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

normal_form_uniqueLean 4Proved here from basic factsFormally verified

/-- **Normal forms are unique**: a term has at most one normal form. By Church–Rosser two normal
forms `u, v` of `t` reduce to a common `w`; a normal term reduces only to itself, so
`u = w = v`. -/
theorem normal_form_unique {t u v : Term} (hu : ReflTransGen Step t u) (hv : ReflTransGen Step t v)
    (nu : Normal u) (nv : Normal v) : u = v := by
  have stuck : ∀ {x y : Term}, Normal x → ReflTransGen Step x y → x = y := by
    intro x y nx hxy
    cases hxy.cases_head with
    | inl h => exact h
    | inr h =>
      obtain ⟨z, hxz, _⟩ := h
      exact absurd hxz (nx z)
  obtain ⟨w, huw, hvw⟩ := church_rosser hu hv
  rw [stuck nu huw, stuck nv hvw]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

plus_unique_valueLean 4Proved here from basic factsFormally verified

/-- Consequently `5̄` is *the* normal form of `plus 2̄ 3̄`: no reduction strategy can produce a
different normal form. -/
theorem plus_unique_value {v : Term} (hv : ReflTransGen Step (app (app plus (church 2)) (church 3)) v)
    (nv : Normal v) : v = church 5 :=
  (normal_form_unique two_plus_three hv (church_normal 5) nv).symm

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LambdaCalculus.leanTry it in the Lean web editor

What is and is not formalised. Everything above — syntax, substitution, β-reduction, $\Omega$ , both fixed-point combinators, Church arithmetic, the evaluator and the full Church–Rosser theorem with uniqueness of normal forms — is proved independently in this module; from Mathlib it uses only the reflexive–transitive closure ReflTransGen (and Relation.church_rosser, for the comparison above). Not formalised: standardisation (Theorem 4), λ-definability of the partial recursive functions and undecidability (Theorem 5), and the typed calculus with Theorems 6 and 7.

ComputationC

An interpreter, and Church–Rosser by exhaustion

The first experiment is a small λ-calculus interpreter. It parses named terms into de Bruijn form, reduces them by normal order, and counts β-steps. It also runs $K\, I\, \Omega$ under applicative order.

Church numerals, recursion and non-termination in the λ-calculusPythonExact computationComputationally tested

"""A small lambda-calculus interpreter: Church numerals, recursion, and loops.

Terms are written in the usual named syntax (``\\x. x`` or ``λx. x``), parsed
into de Bruijn indices, and reduced with capture-avoiding substitution. Normal
order (leftmost-outermost redex first) computes Church-numeral arithmetic,
booleans, Kleene's predecessor and a factorial defined with the fixed-point
combinator Y, counting beta-steps. Omega = (λx. x x)(λx. x x) runs out of fuel,
and K I Omega shows that the strategy matters: normal order finds the normal
form, applicative order (arguments first) never does. Every result is an exact
computation for these particular terms.
"""

import re

# A term is ("var", index), ("app", function, argument) or ("lam", body).

def parse(text, defs=None):
    """Parse a named λ-term into de Bruijn form.

    Syntax: ``\\x. body`` or ``λx. body`` (abstraction extends to the right),
    application by juxtaposition (left-associative), parentheses, and names
    from ``defs`` (a dict name -> already-parsed closed term) used as macros.
    """
    defs = defs or {}
    tokens = re.findall(r"[\\λ.()]|[A-Za-z0-9_']+", text)
    pos = 0

    def peek():
        return tokens[pos] if pos < len(tokens) else None

    def take(expected=None):
        nonlocal pos
        tok = peek()
        if tok is None or (expected is not None and tok != expected):
            raise ValueError(f"expected {expected!r} at token {pos}: {text!r}")
        pos += 1
        return tok

    def term(scope):
        if peek() in ("\\", "λ"):
            take()
            name = take()
            take(".")
            return ("lam", term([name] + scope))
        result = None
        while peek() not in (None, ")"):
            arg = atom(scope)
            result = arg if result is None else ("app", result, arg)
            if peek() in ("\\", "λ"):
                arg = term(scope)
                result = ("app", result, arg)
        if result is None:
            raise ValueError(f"empty term: {text!r}")
        return result

    def atom(scope):
        tok = take()
        if tok == "(":
            inner = term(scope)
            take(")")
            return inner
        if tok in scope:
            return ("var", scope.index(tok))
        if tok in defs:
            return defs[tok]
        raise ValueError(f"unbound name {tok!r} in {text!r}")

    result = term([])
    if pos != len(tokens):
        raise ValueError(f"unexpected {peek()!r} in {text!r}")
    return result

def shift(t, d, cutoff=0):
    """Add ``d`` to every free index (those >= ``cutoff``)."""
    if t[0] == "var":
        return ("var", t[1] + d) if t[1] >= cutoff else t
    if t[0] == "app":
        return ("app", shift(t[1], d, cutoff), shift(t[2], d, cutoff))
    return ("lam", shift(t[1], d, cutoff + 1))

def subst(t, j, s):
    """Capture-avoiding substitution t[s/j]: the shift under λ avoids capture."""
    if t[0] == "var":
        return s if t[1] == j else t
    if t[0] == "app":
        return ("app", subst(t[1], j, s), subst(t[2], j, s))
    return ("lam", subst(t[1], j + 1, shift(s, 1)))

def beta(body, arg):
    """Contract the redex (λ. body) arg."""
    return shift(subst(body, 0, shift(arg, 1)), -1)

def step_normal(t):
    """One normal-order step (leftmost-outermost redex), or None if normal."""
    if t[0] == "var":
        return None
    if t[0] == "lam":
        b = step_normal(t[1])
        return None if b is None else ("lam", b)
    f, a = t[1], t[2]
    if f[0] == "lam":
        return beta(f[1], a)
    f2 = step_normal(f)
    if f2 is not None:
        return ("app", f2, a)
    a2 = step_normal(a)
    return None if a2 is None else ("app", f, a2)

def step_applicative(t):
    """One applicative-order step: reduce inside the function and argument
    first, and contract a redex only when both parts are already normal."""
    if t[0] == "var":
        return None
    if t[0] == "lam":
        b = step_applicative(t[1])
        return None if b is None else ("lam", b)
    f, a = t[1], t[2]
    f2 = step_applicative(f)
    if f2 is not None:
        return ("app", f2, a)
    a2 = step_applicative(a)
    if a2 is not None:
        return ("app", f, a2)
    return beta(f[1], a) if f[0] == "lam" else None

def normalize(t, fuel=10_000, step=step_normal):
    """Reduce until normal; return (normal form or None, steps used)."""
    for n in range(fuel):
        nxt = step(t)
        if nxt is None:
            return t, n
        t = nxt
    return None, fuel

def church(n):
    """The Church numeral λf. λx. f^n x."""
    body = ("var", 0)
    for _ in range(n):
        body = ("app", ("var", 1), body)
    return ("lam", ("lam", body))

def decode_church(t):
    """Return n if ``t`` is exactly the Church numeral n, else None."""
    if t is None or t[0] != "lam" or t[1][0] != "lam":
        return None
    body, n = t[1][1], 0
    while body[0] == "app" and body[1] == ("var", 1):
        body, n = body[2], n + 1
    return n if body == ("var", 0) else None

def standard_defs():
    """Church encodings used in the lesson, as parsed closed terms."""
    d = {"ZERO": church(0), "ONE": church(1)}
    for name, src in [
        ("TRUE", r"\x. \y. x"), ("FALSE", r"\x. \y. y"),
        ("AND", r"\p. \q. p q p"), ("OR", r"\p. \q. p p q"),
        ("NOT", r"\p. p FALSE TRUE"),
        ("PAIR", r"\a. \b. \f. f a b"),
        ("FST", r"\p. p TRUE"), ("SND", r"\p. p FALSE"),
        ("SUCC", r"\n. \f. \x. f (n f x)"),
        ("PLUS", r"\m. \n. \f. \x. m f (n f x)"),
        ("TIMES", r"\m. \n. \f. m (n f)"),
        ("EXP", r"\m. \n. n m"),
        ("ISZERO", r"\n. n (\z. FALSE) TRUE"),
        ("PRED", r"\n. FST (n (\p. PAIR (SND p) (SUCC (SND p))) "
                 r"(PAIR ZERO ZERO))"),
        ("Y", r"\f. (\x. f (x x)) (\x. f (x x))"),
        ("FACT", r"Y (\r. \n. ISZERO n ONE (TIMES n (r (PRED n))))"),
        ("OMEGA", r"(\x. x x) (\x. x x)"),
        ("I", r"\x. x"), ("K", r"\x. \y. x"),
    ]:
        d[name] = parse(src, d)
    for n in range(10):
        d[str(n)] = church(n)
    return d

def run(src, defs, step=step_normal, fuel=10_000):
    """Parse ``src`` with ``defs`` and normalize; return (term, steps)."""
    return normalize(parse(src, defs), fuel, step)

def main():
    d = standard_defs()
    print("Normal-order reduction of Church encodings (exact beta-steps)")
    for src in ["PLUS 2 3", "TIMES 2 3", "EXP 2 3", "PRED 3", "FACT 3"]:
        nf, steps = run(src, d)
        print(f"  {src:<10} ->  Church numeral {decode_church(nf)}"
              f"   ({steps} steps)")
    print()
    print("Booleans: AND p q = p q p, OR p q = p p q")
    names = {d["TRUE"]: "TRUE", d["FALSE"]: "FALSE"}
    for p in ("TRUE", "FALSE"):
        for q in ("TRUE", "FALSE"):
            a, _ = run(f"AND {p} {q}", d)
            o, _ = run(f"OR {p} {q}", d)
            print(f"  p = {p:<5}  q = {q:<5}  AND -> {names[a]:<5}"
                  f"  OR -> {names[o]}")
    print()
    omega = d["OMEGA"]
    nf, steps = normalize(omega, 1000)
    print("Omega = (λx. x x)(λx. x x)")
    print(f"  one step turns Omega into Omega again: {step_normal(omega) == omega}")
    print(f"  normal form within {steps} steps: {nf is not None}")
    nf, steps = run("K I OMEGA", d)
    print("K I Omega")
    print(f"  normal order:      normal form I after {steps} steps:"
          f" {nf == d['I']}")
    nf, steps = run("K I OMEGA", d, step=step_applicative, fuel=1000)
    print(f"  applicative order: normal form within {steps} steps:"
          f" {nf is not None}")
    print()
    print("Epistemic status: exact computations on these particular terms, "
          "checked\nby an interpreter. They illustrate, but do not prove, "
          "that Church\nnumerals compute arithmetic in general, that Omega "
          "has no normal form\n(proved in the lesson and in Lean) or that "
          "normal order always finds a\nnormal form when one exists (the "
          "standardisation theorem).")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

What to notice: $\mathsf{PLUS}\, \bar 2\, \bar 3$ takes 6 steps and $\mathsf{TIMES}\, \bar 2\, \bar 3$ takes 7, the same counts as the Lean evaluator. Kleene's predecessor takes 36 steps for $\mathsf{PRED}\, \bar 3$ , and the factorial via $Y$ needs 1477 steps for $3! = 6$ : Church numerals are a proof of concept, not an efficient representation. $K\, I\, \Omega$ normalises in 2 steps in normal order and never in applicative order.

The second experiment tests the Church–Rosser theorem on every term with at most one free variable and at most 10 nodes (variables, applications and abstractions) — 38,438 terms. For each it builds the complete reduction graph, every redex in every order, and checks that any two reducts have a common reduct and that no term reaches two normal forms.

Church–Rosser on every small λ-term: an exhaustive checkPythonExhaustive finite checkExact computationComputationally tested

"""Testing the Church-Rosser theorem on every small λ-term.

We enumerate every λ-term (de Bruijn indices, at most one free variable) up
to a given size, build its complete β-reduction graph (all redexes, all
orders) when that graph is small, and check two consequences of confluence:
every two reducts of a term have a common reduct, and no term reaches two
different normal forms. We also count terms that have a normal form but also
an infinite reduction (weakly but not strongly normalising, like K I Omega),
and compare the shortest and longest routes to a normal form. This is
exhaustive evidence for finitely many terms; the theorem is proved in the
lesson and in Lean.
"""

from collections import deque

# Terms: ("var", i), ("app", s, t), ("lam", t).

def terms_of_size(size, depth, free=1, _memo=None):
    """All terms of exactly ``size`` nodes whose indices are < depth + free."""
    memo = {} if _memo is None else _memo
    key = (size, depth)
    if key in memo:
        return memo[key]
    out = []
    if size == 1:
        out = [("var", i) for i in range(depth + free)]
    elif size >= 2:
        out += [("lam", t) for t in terms_of_size(size - 1, depth + 1, free, memo)]
        for left in range(1, size - 1):
            for s in terms_of_size(left, depth, free, memo):
                for t in terms_of_size(size - 1 - left, depth, free, memo):
                    out.append(("app", s, t))
    memo[key] = out
    return out

def shift(t, d, cutoff=0):
    """Add ``d`` to every free index (those >= ``cutoff``)."""
    if t[0] == "var":
        return ("var", t[1] + d) if t[1] >= cutoff else t
    if t[0] == "app":
        return ("app", shift(t[1], d, cutoff), shift(t[2], d, cutoff))
    return ("lam", shift(t[1], d, cutoff + 1))

def subst(t, j, s):
    """Capture-avoiding substitution t[s/j]."""
    if t[0] == "var":
        return s if t[1] == j else t
    if t[0] == "app":
        return ("app", subst(t[1], j, s), subst(t[2], j, s))
    return ("lam", subst(t[1], j + 1, shift(s, 1)))

def reducts(t, _memo={}):
    """The set of all one-step β-reducts of ``t`` (every redex position)."""
    if t in _memo:
        return _memo[t]
    out = set()
    if t[0] == "lam":
        out = {("lam", b) for b in reducts(t[1])}
    elif t[0] == "app":
        f, a = t[1], t[2]
        if f[0] == "lam":
            out.add(shift(subst(f[1], 0, shift(a, 1)), -1))
        out |= {("app", f2, a) for f2 in reducts(f)}
        out |= {("app", f, a2) for a2 in reducts(a)}
    _memo[t] = frozenset(out)
    return _memo[t]

def size_of(t):
    """Number of nodes of a term."""
    if t[0] == "var":
        return 1
    if t[0] == "lam":
        return 1 + size_of(t[1])
    return 1 + size_of(t[1]) + size_of(t[2])

def reduction_graph(t, cap=200):
    """All terms reachable from ``t`` with their reducts, or None if more
    than ``cap`` terms are reachable."""
    graph, queue = {}, deque([t])
    while queue:
        u = queue.popleft()
        if u in graph:
            continue
        graph[u] = reducts(u)
        if len(graph) > cap:
            return None
        queue.extend(v for v in graph[u] if v not in graph)
    return graph

def reachable(graph, start):
    """Terms reachable from ``start`` (including itself) in a finite graph."""
    seen, stack = {start}, [start]
    while stack:
        for v in graph[stack.pop()]:
            if v not in seen:
                seen.add(v)
                stack.append(v)
    return seen

def has_cycle(graph):
    """Whether the finite reduction graph contains a cycle."""
    colour = {}
    for root in graph:
        if root in colour:
            continue
        colour[root] = 1
        stack = [(root, iter(graph[root]))]
        while stack:
            node, it = stack[-1]
            nxt = next(it, None)
            if nxt is None:
                colour[node] = 2
                stack.pop()
            elif colour.get(nxt) == 1:
                return True
            elif nxt not in colour:
                colour[nxt] = 1
                stack.append((nxt, iter(graph[nxt])))
    return False

def path_lengths(graph, start, target):
    """Shortest and longest path lengths from start to target (acyclic)."""
    best = {}

    def longest(u):
        if u == target:
            return 0
        if u not in best:
            options = [longest(v) for v in graph[u]]
            best[u] = 1 + max(x for x in options if x is not None) \
                if any(x is not None for x in options) else None
        return best[u]

    dist, queue = {start: 0}, deque([start])
    while queue:
        u = queue.popleft()
        for v in graph[u]:
            if v not in dist:
                dist[v] = dist[u] + 1
                queue.append(v)
    return dist.get(target), longest(start)

def analyse(t, cap=200):
    """Classify one term: returns a dict of facts about its reduction graph."""
    graph = reduction_graph(t, cap)
    if graph is None:
        return {"explored": False}
    normal = [u for u in graph if not graph[u]]
    reach = {u: reachable(graph, u) for u in graph}
    locally_confluent = all(
        reach[b] & reach[c]
        for u in graph for b in graph[u] for c in graph[u])
    return {"explored": True, "normal_forms": len(normal),
            "joinable": locally_confluent, "cycle": has_cycle(graph),
            "graph_size": len(graph)}

def survey(max_size=8, cap=200):
    """Analyse every term with at most one free variable up to ``max_size``."""
    stats = {"terms": 0, "explored": 0, "with_nf": 0, "two_nf": 0,
             "not_joinable": 0, "wn_not_sn": 0, "no_nf": 0, "largest": 0}
    memo = {}
    for size in range(1, max_size + 1):
        for t in terms_of_size(size, 0, 1, memo):
            stats["terms"] += 1
            facts = analyse(t, cap)
            if not facts["explored"]:
                continue
            stats["explored"] += 1
            stats["largest"] = max(stats["largest"], facts["graph_size"])
            stats["with_nf"] += facts["normal_forms"] >= 1
            stats["no_nf"] += facts["normal_forms"] == 0
            stats["two_nf"] += facts["normal_forms"] >= 2
            stats["not_joinable"] += not facts["joinable"]
            stats["wn_not_sn"] += facts["normal_forms"] >= 1 and facts["cycle"]
    return stats

NAMED = {
    "I": ("lam", ("var", 0)),
    "K": ("lam", ("lam", ("var", 1))),
    "omega": ("lam", ("app", ("var", 0), ("var", 0))),
    "omega3": ("lam", ("app", ("app", ("var", 0), ("var", 0)), ("var", 0))),
}

def examples():
    """Named terms illustrating the possible shapes of reduction graphs."""
    i, k, w, w3 = (NAMED[n] for n in ("I", "K", "omega", "omega3"))
    z = ("var", 0)
    return [
        ("(λx. x x)((λy. y) z)", ("app", w, ("app", i, z))),
        ("K I Omega", ("app", ("app", k, i), ("app", w, w))),
        ("Omega", ("app", w, w)),
        ("(λx. x x x)(λx. x x x)", ("app", w3, w3)),
    ]

def main():
    max_size = 10
    s = survey(max_size)
    print(f"All {s['terms']} λ-terms of size <= {max_size} with at most one"
          " free variable")
    print(f"  reduction graph built (<= 200 terms):        {s['explored']}")
    print(f"  largest graph built:                         {s['largest']}")
    print(f"  with a normal form:                          {s['with_nf']}")
    print(f"  with no normal form:                         {s['no_nf']}")
    print(f"  reaching two different normal forms:         {s['two_nf']}")
    print(f"  with two reducts that cannot be joined:      {s['not_joinable']}")
    print()
    print("Some larger terms:")
    for name, t in examples():
        g = reduction_graph(t, cap=200)
        if g is None:
            print(f"  {name:<24} more than 200 reducts: the graph keeps growing")
            continue
        nfs = [u for u in g if not g[u]]
        terms = f"{len(g)} term" + ("s" if len(g) != 1 else "")
        count = {0: "no normal form", 1: "one normal form"}.get(
            len(nfs), f"{len(nfs)} normal forms")
        line = f"  {name:<24} {terms}, {count}"
        if nfs and has_cycle(g):
            line += ", also an infinite reduction"
        elif nfs:
            short, long_ = path_lengths(g, t, nfs[0])
            line += f", routes of {short} to {long_} steps"
        else:
            line += ", every reduction is infinite"
        print(line)
    print()
    print("Epistemic status: an exhaustive check of finitely many terms (and "
          "only\nof those whose reduction graphs are small). It is evidence "
          "for the\nChurch-Rosser theorem, not a proof: the proof, by "
          "parallel reduction,\nis in the lesson and is machine-checked in "
          "Lean.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

No counterexample, as the theorem guarantees. Notice $(\lambda x.\, x\, x)((\lambda y.\, y)\, z)$ : different routes to its normal form take 2 or 3 steps, so the answer is independent of the strategy but the cost is not. And $(\lambda x.\, x\, x\, x)(\lambda x.\, x\, x\, x)$ has an ever-growing reduction graph. Both experiments are evidence for finitely many terms; the theorems are proved above and in Lean.

Explore

Explore: reduction graphs and Church booleans

Here is the full reduction graph of $(\lambda x.\, x\, x)(I\, z)$ with $I = \lambda y.\, y$ . Each arrow contracts one redex. Follow any path from the top: all of them end at $z\, z$ .

Contracting the outer redex first duplicates

I\, z

, so the left routes take 3 steps; contracting

I\, z

first takes 2. Confluence: the normal form

z\, z

is the same.

The parallel-reduction proof fills every such picture with diamonds: from $M$ , any two parallel reductions meet again at the complete development $M^\ast$ in one parallel step each.

The triangle property (Lemma C) makes parallel reduction a diamond: every parallel reduct of

M

reaches

M^\ast

in one more parallel step.

Church booleans are selectors, so $\mathsf{AND}\, p\, q = p\, q\, p$ means "if $p$ then $q$ else $p$ ". Is that really "and"? Compare it with $p \wedge q$ in the truth table, writing "if $p$ then $q$ else $p$ " as $(p \wedge q) \vee (\neg p \wedge p)$ . Then try $\mathsf{OR}\, p\, q = p\, p\, q$ , "if $p$ then $p$ else $q$ ".

Church's AND, read as if-then-else

AND p q = p q p means ‘if p then q else p’.

Formula

Read as: (p ∧ q) ∨ (¬p ∧ p)

Compare with

Read as: p ∧ q

Use the symbols ¬ ∧ ∨ → ↔, the words not, and, or, implies, iff, or ASCII ~ & | -> <->. Variables are single lowercase letters. ¬ binds tightest, then ∧, ∨, →, ↔; p → q → r means p → (q → r).

Try:

Contingent — true in 1 of 4 rows, false in the others.

Equivalent — the two formulas agree in all 4 rows.

p	q	p ∧ q	¬p	¬p ∧ p	p ∧ q ∨ ¬p ∧ p	p ∧ q
T	T	T	F	F	T	T
T	F	F	F	F	F	F
F	T	F	T	F	F	F
F	F	F	T	F	F	F

4 rows: one for every way of making the 2 variables true or false.

Exercises

1. The λ-calculus

Warm-upHuman

List the free variables of the term $\lambda x.\, x\, y\, (\lambda y.\, y\, z)$ . Enter each variable name once.

2. The λ-calculus

Warm-upHuman

What does $(\lambda x.\, \lambda y.\, x)\, y$ reduce to in one β-step (with $y$ free)?

Choose one

\lambda z.\, y

\lambda y.\, y

y

\lambda y.\, x

3. The λ-calculus

CoreHuman

With Church numerals $\bar n = \lambda f\, x.\, f^n\, x$ , the term $\bar 3\, \bar 2$ (the numeral $3$ applied to the numeral $2$ ) β-reduces to a Church numeral $\bar k$ . What is $k$ ?

4. The λ-calculus

CoreHuman

Which of these terms have no normal form? Here $\Omega = (\lambda x.\, x\, x)(\lambda x.\, x\, x)$ , $K = \lambda x\, y.\, x$ , $I = \lambda x.\, x$ . Choose all that apply.

Choose all that apply

\Omega

\lambda z.\, \Omega

K\, I\, \Omega

(\lambda x.\, x\, x)(\lambda y.\, y)

5. The λ-calculus

CoreHuman

Why does the proof of the Church–Rosser theorem go through parallel reduction $\Rightarrow$ instead of showing directly that one-step reduction $\to$ has the diamond property?

Choose one

Because

\to

does not have the diamond property: contracting a redex can duplicate another redex, so joining may need several steps on one side.Because

\to

is not terminating.Because

\Rightarrow

is terminating while

\to

is not.Because the diamond property for

\to

is true but too hard to prove.

6. The λ-calculus

StretchHuman

In Turing's proof of weak normalisation we contract a redex $R = (\lambda x{:}A.\, P)\, Q$ of maximal degree $d$ chosen so that $Q$ contains no redex of degree $d$ . Which part of the argument needs this choice?

Choose one

Redexes inside

Q

may be copied many times by the substitution

P[Q/x]

; the choice ensures all the copies have degree less than

d

.It ensures that no new redexes are created.It ensures that the redexes inside

P

survive.It ensures the term is typable after the step.

7. The λ-calculus

CoreHuman

Which of these terms has a type in the simply typed λ-calculus (for suitable types on the bound variables)?

Choose one

\lambda f\, x.\, f\,(f\, x)

\lambda x.\, x\, x

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

\Omega

8. The λ-calculus

CoreFormal

In the lesson's Lean file, Step t u is one β-step and ReflTransGen Step t u is $t \twoheadrightarrow u$ . Which statement is the Church–Rosser theorem, as proved there?

Choose one

∀ {t u v}, ReflTransGen Step t u → ReflTransGen Step t v → ∃ w, ReflTransGen Step u w ∧ ReflTransGen Step v wDiamond Step∀ t, ∃ u, ReflTransGen Step t u ∧ Normal u∀ {t u v}, Step t u → Step t v → u = v

9. The λ-calculus

CoreComputational

Python's lambda can run Church numerals directly. With church(n) and to_int below, define times(m, n) and exp(m, n) returning the Church numerals for $m \cdot n$ and $m^n$ , using only application and lambda (no conversion to int inside them).

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

Substituting without renaming bound variables. $(\lambda x\, y.\, x)\, y$ is not $\lambda y.\, y$ : the free $y$ would be captured. Rename the bound variable first: $(\lambda x\, z.\, x)\, y \to \lambda z.\, y$ . De Bruijn indices make the problem disappear, which is why proof assistants use them.

Misconception

"Every λ-term has a normal form." $\Omega = (\lambda x.\, x\, x)(\lambda x.\, x\, x)$ reduces only to itself, so it has none (proved in Lean above); so does $\lambda x.\, \Omega$ , since reduction also happens under $\lambda$ . Only typed calculi guarantee normal forms.

Misconception

"If a term has a normal form, every reduction strategy finds it." $K\, I\, \Omega$ has normal form $I$ , but reducing $\Omega$ first loops forever. Church–Rosser says the normal form is unique; standardisation says normal order finds it. Neither says every strategy terminates.

Misconception

"Church–Rosser means reduction terminates." Confluence is about agreement, not termination: $\Omega$ is confluent (all its reducts are $\Omega$ ) and never terminates. Uniqueness and existence of normal forms are separate questions.

Misconception

" $M =_\beta N$ means one reduces to the other." β-equality allows reductions in both directions. $Y\, F =_\beta F\,(Y\, F)$ , but neither reduces to the other; they have a common reduct (Corollary 3 says this is always the case for β-equal terms).

ViewpointsH

Viewpoints

Computation— Evaluation strategies and functional programming

To a programmer, the λ-calculus is the core of every functional language, and the strategies of this lesson are real design choices. Most languages (Python, OCaml, Scheme) use call-by-value: evaluate arguments first — applicative order, which loops on $K\, I\, \Omega$ but never duplicates work. Haskell uses call-by-need, normal order with sharing, so that a duplicated argument such as the $I\, z$ above is evaluated at most once. In a call-by-value language $Y$ loops even when used correctly; one uses the η-expanded $Z = \lambda f.\, (\lambda x.\, f\,(\lambda v.\, x\, x\, v))(\lambda x.\, f\,(\lambda v.\, x\, x\, v))$ instead. Closures, currying ( $\lambda x\, y.\, M$ as a function returning a function) and higher-order functions such as map all come from here. Peter Landin's SECD machine (1964) was the first abstract machine for evaluating λ-terms.

Logic— A failed logic and a successful calculus

Church introduced λ-notation as part of a system of logic intended as a foundation of mathematics. In 1935 Kleene and Rosser showed that system inconsistent, and Curry later distilled the problem into a short paradox built on the same self-application as $Y$ : with a fixed point of $\lambda x.\, (x \to P)$ , every proposition $P$ becomes provable. What survived was the pure calculus of functions, whose consistency as an equational theory is exactly Corollary 3 ( $\mathsf{TRUE} \ne_\beta \mathsf{FALSE}$ ). Church then used it to give the first published undecidable problem (1936), and with types it became a logic again: under the Curry–Howard correspondence, simply typed terms are proofs in intuitionistic propositional logic and β-reduction is the elimination of detours in proofs. See type theory and proof theory.

Topology— Scott's models: continuity tames self-application

Can the untyped calculus be modelled by actual functions? Self-application suggests a set $D$ with $D \cong D^D$ , which Cantor's theorem forbids unless $|D| = 1$ . In 1969 Dana Scott found the way out: work with complete lattices and only the continuous functions for the Scott topology (the open sets are the upward-closed sets that cannot be reached by a directed supremum from outside). He constructed a lattice $D_\infty$ , as an inverse limit, with $D_\infty \cong [D_\infty \to D_\infty]$ , the space of continuous functions — a non-trivial model in which every λ-term denotes an element and β-equal terms denote the same element. The Scott topology is $T_0$ but not Hausdorff: its specialisation order is the information order, " $x \sqsubseteq y$ when $y$ is at least as defined as $x$ ". Continuity — a finite part of the output depends only on a finite part of the input — is a topological statement about computation, and domain theory grew from it.

Algebra— Combinators and combinatory algebras

Bound variables can be eliminated entirely. In combinatory logic (Schönfinkel 1924, Curry 1930) there are just two constants with the rules $K\, x\, y = x$ and $S\, x\, y\, z = x\, z\,(y\, z)$ , and every λ-term can be translated into an expression in $S$ and $K$ by "bracket abstraction" (for instance $I = S\, K\, K$ , as computed above). Algebraically, a combinatory algebra is a set with a binary operation (application) containing elements $K, S$ obeying these two laws; it is combinatorially complete: every polynomial in the operation is represented by an element. Models of the λ-calculus are combinatory algebras satisfying a few extra axioms (λ-algebras), and the λ-calculus becomes an equational algebraic theory — though a strange one, since application is neither associative nor commutative.

Category theory— Cartesian closed categories

Joachim Lambek observed (around 1980) that the simply typed λ-calculus with products is the internal language of cartesian closed categories: types are objects, a term $x : A \vdash M : B$ is an arrow $A \to B$ , abstraction is the bijection $\Hom(A \times B, C) \cong \Hom(A, C^B)$ , and β- and η-equality are the two triangle laws of that adjunction. Untyped models live in a CCC as reflexive objects $U$ with $U^U$ a retract of $U$ — Scott's $D_\infty$ is one in the category of complete lattices and continuous maps. See categorical logic.

History & global context

History and global context

Moses Schönfinkel (working in Göttingen) introduced combinators in "Über die Bausteine der mathematischen Logik" (1924); Haskell Curry developed combinatory logic from his 1930 dissertation onwards.
Alonzo Church introduced λ-notation in "A set of postulates for the foundation of logic" (Annals of Mathematics, 1932–33). Stephen Kleene and J. Barkley Rosser showed the logical system inconsistent (1935). Kleene, then Church's student, found the λ-definition of the predecessor; he later recalled that the idea came to him at the dentist's.
Church and Rosser proved confluence in "Some properties of conversion" (Transactions of the AMS, 1936). Church's "An unsolvable problem of elementary number theory" (1936) proposed identifying effective computability with λ-definability and gave the first undecidability result; Kleene (1936) and Alan Turing ("Computability and λ-definability", 1937) proved the equivalences with recursive functions and Turing machines.
Church's simple theory of types (1940) introduced the typed calculus. Turing's normalisation argument was published by Robin Gandy in 1980; William Tait proved strong normalisation in 1967. The parallel-reduction proof of Church–Rosser is due to Tait and Per Martin-Löf, and the complete-development form to Masako Takahashi (1995). N. G. de Bruijn introduced nameless indices for the Automath proof checker (1972).
John McCarthy's LISP (1960) borrowed λ-notation; Peter Landin (1964–66) showed how to understand programming languages through the λ-calculus; Corrado Böhm proved his separation theorem (1968); Dana Scott built the first mathematical models (1969). Henk Barendregt's monograph (1981; revised 1984) made the subject a branch of mathematics.

Functions as rules

Terms as trees, reduction as plugging in

Definitions

Examples: combinators, data and recursion

The main theorems

Types tame the calculus

The λ-calculus in Lean

An interpreter, and Church–Rosser by exhaustion

Explore: reduction graphs and Church booleans

Exercises

Common misconceptions

Viewpoints

History and global context

Further reading