Church Numerals
ZERO, ONE, TWO, THREE. Numbers as iteration counts.
With Church booleans, we discovered that selection was hiding in lambda terms we already had. Now the same thing happens with numbers -- but the insight cuts even deeper. A boolean selects between two things. A number tells you how many times to do something. In lambda calculus, "how many times" is not a label attached to an object. It is the action itself: a function that repeats another function n times.
Numbers Are Verbs
A Church numeral is a lambda term that takes a function f and a
starting value x, and applies f to x some number of times:
- ZERO =
λf.λx.x-- applyfzero times (just returnx) - ONE =
λf.λx.f x-- applyfonce - TWO =
λf.λx.f (f x)-- applyftwice - THREE =
λf.λx.f (f (f x))-- applyfthree times
The number n is not a tag or a label. It IS the act of applying f
exactly n times. Numbers are verbs, not nouns.
ZERO Definition
ZERO is the Church numeral for the number 0:
ZERO = λf.λx.x
It takes a function f and a starting value x, and applies f
zero times -- meaning it ignores f entirely and just returns x.
Notice that f does not appear in the body. ZERO receives a process
but never uses it.
ONE Definition
ONE is the Church numeral for the number 1:
ONE = λf.λx.f x
It takes a function f and a starting value x, and applies f
exactly once. Compare with ZERO = λf.λx.x, which does not apply
f at all. ONE applies it once.
TWO Definition
TWO is the Church numeral for the number 2:
TWO = λf.λx.f (f x)
It takes a function f and a starting value x, and applies f
twice: first to x, then to the result f x.
Compare the pattern so far:
- ZERO =
λf.λx.x-- zero applications off - ONE =
λf.λx.f x-- one application off - TWO =
λf.λx.f (f x)-- two applications off
THREE Definition
The pattern for Church numerals is now clear:
- ZERO =
λf.λx.x - ONE =
λf.λx.f x - TWO =
λf.λx.f (f x)
Each numeral wraps one more application of f around the previous
body. THREE should apply f three times.
Pattern Recognition
Look at the Church numerals side by side:
- ZERO =
λf.λx.x - ONE =
λf.λx.f x - TWO =
λf.λx.f (f x) - THREE =
λf.λx.f (f (f x))
Every Church numeral has the same outer shape: λf.λx.____. They
all take a function f and a starting value x. What differs is
the body -- specifically, how many times f is applied.
A Numeral IS a Function
In everyday mathematics, numbers are objects -- things you can add, compare, or store. In lambda calculus, a number is a function. It takes two arguments:
- A function
f-- the process to repeat - A starting value
x-- where to begin
The numeral then applies f to x some number of times and returns
the result. The number does not describe a quantity. It performs one.
Which Numeral?
To identify which number a Church numeral represents, count how many
times f is applied to x in the body:
λf.λx.x-- 0 applications -- ZEROλf.λx.f x-- 1 application -- ONEλf.λx.f (f x)-- 2 applications -- TWOλf.λx.f (f (f x))-- 3 applications -- THREE
The number IS the count of nested f applications.
ZERO and FALSE
Compare these two definitions:
- ZERO =
λf.λx.x-- takes two arguments, returns the second - FALSE =
λx.λy.y-- takes two arguments, returns the second
The parameter names differ (f/x vs x/y), but parameter
names are arbitrary. Both terms take two arguments and return the
second one. By alpha equivalence -- renaming bound variables does
not change a term's meaning -- these are the same lambda term.
Why Iteration?
Church could have encoded numbers many ways. He could have used
a chain of pairs, a sequence of TRUE/FALSE values, or some other
scheme. Instead, he defined the number n as "apply f exactly n
times."
Why iteration? Because lambda calculus has exactly one operation: applying a function to an argument. The most natural way to express "how many" in a system that only has function application is to count applications. The number n becomes "do it n times" -- which is itself a function that takes any process and repeats it.
This encoding is not arbitrary. It makes arithmetic fall out naturally: adding means composing iterations, multiplying means iterating iteration.
Not the Only Way
Church's encodings of booleans and numbers are not the only valid encodings. They are conventions — choices that work well, not theorems that must be true.
We could define TRUE = λx.λy.y and FALSE = λx.λy.x (swapped).
We would then redefine AND, OR, and NOT to match, and logic would
work exactly as before.
Similarly, Church numerals are not the only way to encode numbers. Alternatives like Scott numerals and Barendregt numerals encode numbers with different trade-offs.
Lambda calculus contains the capacity for logic and arithmetic — the raw material from which these structures can be built — but it does not determine a unique encoding. The encoding is a design decision.
Ready to test your understanding?
Bitwit uses spaced repetition to help you truly master concepts like this—not just read about them. Each card generates with different values, so you can't just memorize answers.
Practice Church Numerals →