Successor
SUCC adds one more function application.
We have numbers as iteration counts: ZERO applies f zero times, ONE applies it once, TWO applies it twice. But right now, each numeral is a standalone definition. We need a way to get from one number to the next -- a single operation that takes any numeral and produces its successor. Without this, we cannot build arithmetic.
What Is Successor?
Recall that a Church numeral n is λf.λx. followed by n applications
of f:
- ZERO =
λf.λx.x - ONE =
λf.λx.f x - TWO =
λf.λx.f (f x)
The successor function SUCC takes a numeral and returns the next
numeral. Since each numeral applies f some number of times, SUCC
must produce a term that applies f exactly one more time than
the input did.
The Definition of SUCC
The successor function is defined as:
SUCC = λn.λf.λx.f (n f x)
Reading the definition:
- Take a numeral
n - Take a function
fand a starting valuex - First, let
ndo its work:n f xappliesfexactly n times tox - Then apply
fone more time to the result
The key insight: n f x is "n applications of f to x." Wrapping one
more f around it gives "n + 1 applications of f to x" -- which is
exactly the next Church numeral.
SUCC ZERO
SUCC = λn.λf.λx.f (n f x) and ZERO = λf.λx.x.
Applying SUCC to ZERO:
- SUCC ZERO =
λf.λx.f (ZERO f x) - ZERO f x = x (ZERO applies f zero times)
- So SUCC ZERO =
λf.λx.f x
That result -- λf.λx.f x -- applies f exactly once to x.
That is ONE.
SUCC ONE
SUCC = λn.λf.λx.f (n f x) and ONE = λf.λx.f x.
Applying SUCC to ONE:
- SUCC ONE =
λf.λx.f (ONE f x) - ONE f x = f x (ONE applies f once)
- So SUCC ONE =
λf.λx.f (f x)
That result -- λf.λx.f (f x) -- applies f exactly twice to x.
That is TWO.
How SUCC Works
SUCC = λn.λf.λx.f (n f x)
The mechanism has two phases:
- Delegate: Pass f and x to n. The numeral n applies f to x exactly n times, producing the result of n iterations.
- Wrap: Apply f one more time to that result.
SUCC does not inspect n's internal structure. It does not need to know how many times n applies f. It simply lets n do its work, then adds one more application on the outside.
Building Numbers from ZERO
With SUCC and ZERO, we can construct every Church numeral:
- ZERO =
λf.λx.x - ONE = SUCC ZERO
- TWO = SUCC (SUCC ZERO)
- THREE = SUCC (SUCC (SUCC ZERO))
Each application of SUCC adds one more f. Starting from zero applications and applying SUCC n times gives exactly n applications of f -- which is the Church numeral n.
This mirrors the Peano axioms for natural numbers: zero exists, and every number has a successor. From these two pieces, every natural number can be reached.
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 Successor →