Church Numerals

Advanced Logic Arithmetic

λ-calculus has no numbers. So Church invented them — and the trick is one of the loveliest ideas in mathematics: a number is how many times you do something.

Counting as applying

0 = λf.λx.x apply f zero times — just return x 1 = λf.λx.f x apply f once 2 = λf.λx.f (f x) apply f twice 3 = λf.λx.f (f (f x)) three times

Read λf.λx.… as "give me a way to step (f) and a place to start (x)." The numeral n is the machine that steps n times. This is called a Church numeral.

Why this is profound Numbers-as-repetition isn't a hack — it's arguably what numbers are. "Three" means "do it three times." Church didn't encode counting; he revealed it.

Successor: add one application

SUCC = λn.λf.λx.f (n f x) "take numeral n, then step, then start — and do one extra f on top"

Watch SUCC 1 become 2 — four β-steps, one at a time:

Addition and multiplication

PLUS = λm.λn.λf.λx.m f (n f x) do n steps, then m more MULT = λm.λn.λf.m (n f) an m-fold stack of n-steppers

The catch

Church numerals add and multiply beautifully. Subtraction is famously painful — PRED exists but took the field years to find. It needs pairs, which are the next page's business.

Practice

λf.λx.f (f (f x)) encodes which number? ___

ZERO = λf.λx.x — applying ZERO g v gives…

Write the Church numeral for 2: ___

SUCC n adds one by…

Next: booleans & pairs · Back: beta reduction

← Math home · Research & references