A variable, a way to make a function, a way to apply one — nothing else. From those three marks Alonzo Church built a universal computer in 1936, months before Turing built his. A number is a function: n = λf.λx. f applied to x, n times. Arithmetic becomes term-rewriting. Down the center, terms go in, one β-reduction rule fires until nothing more can, and the decoded integer comes out. The blue team builds and proves it; the red team tries to break it.
source · AMBER Church, An Unsolvable Problem of Elementary Number Theory, Amer. J. Math. 58 (1936) 345–363 — where λ-definability and the Church numerals first appear. No public scan on archive.org (JSTOR 10.2307/2371045); honest link is the archive.org search. The related monograph is Barendregt, The Lambda Calculus (1984). Rendered, not quoted.
The whole calculus is three term shapes and one rule.
Terms: a variable; an abstraction λx.M (a function of x); an application M N (feed N to M).
β-reduction: (λx.M) N → M[x:=N] — substitute the argument for the bound variable. That single move is the entire engine.
To avoid a free variable in N being captured by a λ inside M, this engine uses de Bruijn indices: a variable is a number counting binders outward, so substitution needs no fresh-name games — it just shifts indices. Reduction is normal-order (leftmost-outermost), which by the standardisation theorem reaches a term's normal form whenever one exists.
The same year, in a different notation, Turing defined the machine: a head on an infinite tape. Church defined the function: a term that rewrites. In 1937 they were proved to compute exactly the same class — the Church–Turing thesis.
λ-calculus is the functional root of every language with first-class functions; the tape is the imperative root of every CPU. Two spheres, one power. The twin waits in THE FOLD: this sphere's output — "computation has a smallest shape" — is that one's premise.
The blue team's live check: independently re-reduce SUCC, PLUS, and MULT on real terms and confirm the decoded integers. If red tampers with the engine, this badge is where it shows.
Everything is encoded as a λ-term. A number is how many times you apply a function:
| name | λ-term | means |
|---|---|---|
| 0 | λf.λx. x | apply f zero times |
| 1 | λf.λx. f x | apply f once |
| n | λf.λx. f (f … (f x)) | apply f n times |
| SUCC | λn.λf.λx. f (n f x) | add one |
| PLUS | λm.λn.λf.λx. m f (n f x) | m + n |
| MULT | λm.λn.λf. m (n f) | m × n |
These six terms are the entire input. The panel below builds each input number by iterating SUCC on 0 — Peano-style — then reduces the operator applied to them.
Each β-step contracts the leftmost-outermost redex. "Normal form" runs to the end; the result is decoded by counting the f's — never looked up.
Change any control and the term is rebuilt from the six λ-terms above — then reduced live by the one β-rule.
What the machine proves, live and from scratch: arithmetic is reduction. No numbers are stored — every value is a normal-form term, decoded by counting applications.
The blue team's witness (left) re-derives these; the red team (right) tries to make them lie.
And a Church numeral is a spectacularly slow integer: MULT 6 6 here takes over a hundred rewrites to reach 36. As a model it is universal; as a calculator it is a proof of concept, not a competitor to binary. This panel only survives because it feeds the engine terms known to terminate.
"Church proved lambda calculus can add — that was the point." Cut. The point was unsolvability: no decision procedure for λ-convertibility. Addition just shows the system is rich enough to encode arithmetic first.
"Church numerals are the only encoding." Cut. Scott and Mogensen–Scott encodings exist and are often better; the numeral here is Church's, chosen because SUCC/PLUS/MULT are legible — not because it is canonical.
"Any reduction order gives the same answer." Kept, corrected. The value is confluent (Church–Rosser), but only normal-order is guaranteed to find it. Applicative order can diverge where normal order halts — so this engine commits to leftmost-outermost.
The red team's move: corrupt SUCC to λn.λf.λx. f x — it drops the n and always returns 1, so it no longer adds one. Every number built from it collapses.
Break SUCC and the inputs stop counting: PLUS 2 3 no longer decodes to 5, the panel's answer changes, and the witness (window 7) recomputes, disagrees, and turns red. Nothing is faked — the value genuinely changes and it is caught.