Addition
ADD composes iteration. Conceptual understanding.
We have Church numerals -- iteration counts -- and SUCC, which adds one more application. But adding one at a time is tedious. If TWO means "apply f twice" and THREE means "apply f three times," then adding them should mean "apply f five times." We need an operation that combines two iteration counts into one.
What Is Addition?
Recall that a Church numeral n is a function that applies f exactly n times:
- TWO =
λf.λx.f (f x)(two applications) - THREE =
λf.λx.f (f (f x))(three applications)
Addition combines two numerals by composing their iterations. If m applies f m times and n applies f n times, then ADD m n should apply f a total of m + n times. The idea: let n do its applications first, then let m do its applications on top of that result.
ADD Definition
The addition function takes two Church numerals m and n and produces a new numeral that applies f a total of m + n times:
ADD = λm.λn.λf.λx. m f (n f x)
Reading from right to left:
n f x-- apply f n times to x (n does its iterations)m f (n f x)-- apply f m more times to that result
The result is λf.λx. followed by m + n applications of f. Both
numerals share the same f and x, and their iterations are composed
sequentially.
ADD via SUCC
There is a second way to define addition that uses SUCC directly:
ADD = λm.λn. m SUCC n
This reads: "apply SUCC m times to n." Since SUCC adds one application of f each time, applying it m times adds m to n.
For example, ADD TWO THREE:
- Start with THREE
- Apply SUCC once: FOUR
- Apply SUCC again: FIVE
This works because a Church numeral m is an iterator -- it applies any function m times. Here the function being iterated is SUCC itself.
ADD ONE TWO
ADD = λm.λn.λf.λx. m f (n f x)
Recall:
- ONE =
λf.λx.f x(applies f once) - TWO =
λf.λx.f (f x)(applies f twice)
To compute ADD ONE TWO conceptually:
- TWO does its part:
TWO f x = f (f x)(two applications) - ONE does its part on that result:
ONE f (f (f x)) = f (f (f x))(one more application)
Total: three applications of f. The result is THREE.
ADD ZERO
ADD = λm.λn.λf.λx. m f (n f x)
Recall that ZERO = λf.λx.x -- it applies f zero times, returning x
unchanged.
What happens when we add ZERO to some numeral n?
ADD ZERO n = λf.λx. ZERO f (n f x)
Since ZERO ignores f and returns its second argument unchanged:
ZERO f (n f x) = n f x
ZERO contributes nothing. The result is just n.
Why Addition Works
Addition in lambda calculus is not a new primitive operation bolted onto the system. It falls out directly from what Church numerals already are.
A Church numeral n takes a function f and a starting value x, and applies f exactly n times. Addition composes two such iteration counts: give both numerals the same f and x, let one do its iterations, then let the other continue from where the first left off.
ADD = λm.λn.λf.λx. m f (n f x)
This works because the numerals share the same f. The inner numeral n applies f n times to x. The outer numeral m applies the same f m more times to that intermediate result. The total is m + n applications -- a new Church numeral.
No special arithmetic machinery is needed. Numerals are iterators, and composing iterations is addition.
ADD TWO TWO
ADD = λm.λn.λf.λx. m f (n f x)
Recall:
- TWO =
λf.λx.f (f x)(applies f twice)
To compute ADD TWO TWO conceptually:
- The second TWO does its part:
TWO f x = f (f x)(two applications) - The first TWO does its part on that result:
TWO f (f (f x)) = f (f (f (f x)))(two more)
Total: four applications of f.
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 Addition →