Predecessor

Why PRED Is Hard

A Church numeral n is λf.λx. followed by n applications of f:

• TWO = λf.λx.f (f x) -- applies f twice
• THREE = λf.λx.f (f (f x)) -- applies f three times

SUCC wraps one more f around the outside: easy. PRED needs to remove one f from the inside: hard.

Why is removal hard? Because a Church numeral applies f forward from x. Once f has been applied, there is no built-in way to undo it. You cannot "unapply" a function -- lambda calculus has no inverse operation. SUCC adds a layer on the outside, but PRED cannot simply strip one off, because the applications are nested inward.

The PRED Problem

Here is the problem stated precisely:

A Church numeral n, given f and x, produces f^n(x) -- the result of applying f to x exactly n times.

What we want: given n, produce a new numeral that applies f exactly n - 1 times.

What we have: no way to "unapply" f. Once f has been applied, the result is just a value -- we cannot extract the input that produced it.

What we cannot do: run the numeral for n steps and somehow stop one step early. A Church numeral does not expose its iteration count as a number we can inspect. It just runs f all n times and hands back the result.

We need a different strategy entirely.

The Pair Trick

We cannot unapply f. We cannot stop one step early. But we can remember where we were one step ago.

The idea: instead of applying f directly, iterate a different operation that maintains a pair of values -- the previous result and the current result. At each step, shift the pair forward:

• Start: (previous, current)
• After one shift: (current, next)

After n shifts, the "previous" slot holds the value from step n-1. Extract it, and you have the predecessor.

This is the key insight behind PRED: use pairs to create a memory of the previous step, because Church numerals do not provide one natively.

(We use "pair" here as an informal concept — two values bundled together. The formal lambda calculus encoding of pairs comes in a later topic. For now, the strategy is what matters.)

Shifting Pairs

Here is the pair-shifting strategy in action. Define a "shift" operation on pairs:

shift: (a, b) becomes (b, b+1)

The previous value is discarded, the current value moves to the "previous" slot, and a new "current" is produced by adding one.

Start with (0, 0) and apply shift n times:

• Start: (0, 0)
• After 1 shift: (0, 1) -- b was 0, becomes previous; 0+1 = 1 is current
• After 2 shifts: (1, 2) -- b was 1, becomes previous; 1+1 = 2 is current
• After 3 shifts: (2, 3) -- b was 2, becomes previous; 2+1 = 3 is current

After n shifts, the pair is (n-1, n). Extract the first element to get n-1 -- the predecessor.

PRED ZERO

PRED uses the pair-shifting strategy: start with (ZERO, ZERO), apply the shift operation n times, and extract the first element.

For PRED ZERO, we apply the shift zero times. The pair stays at its starting value: (ZERO, ZERO). Extracting the first element gives ZERO.

This makes sense by convention: Church numerals represent natural numbers (0, 1, 2, ...). There are no negative Church numerals. Going below zero is not an error -- it simply stays at zero.

PRED ONE

PRED ONE: start with (ZERO, ZERO) and shift once.

• Start: (ZERO, ZERO)
• After 1 shift: (ZERO, ONE) -- ZERO moves to "previous," SUCC ZERO = ONE becomes "current"

Extract the first element: ZERO.

PRED ONE = ZERO. The predecessor of one is zero, as expected.

PRED THREE

PRED THREE: start with (ZERO, ZERO) and shift three times.

• Start: (ZERO, ZERO)
• After 1 shift: (ZERO, ONE)
• After 2 shifts: (ONE, TWO)
• After 3 shifts: (TWO, THREE)

Extract the first element: TWO.

The pattern is consistent: after n shifts, the pair is always (n-1, n), and the first element is the predecessor.

Why PRED Needs Pairs

Consider the alternatives:

• Unapply f? No. Functions are not generally invertible.
• Stop one step early? No. A Church numeral runs all n steps without exposing a step counter.
• Subtract directly? No. Subtraction does not exist yet -- we are trying to build it.

Pairs solve the problem because they provide something Church numerals lack: memory. A Church numeral n applies a function n times and produces a single result. It does not remember intermediate values. By iterating on pairs, we carry two values forward at every step -- the current result and the previous one. This "sliding window" gives us access to the value from one step back.

PRED does not go backward. It goes forward while remembering the past.

No Negative Church Numerals

Church numerals represent natural numbers: 0, 1, 2, 3, ...

A Church numeral n applies f exactly n times. You cannot apply f a negative number of times -- the concept does not make sense. There is no Church numeral for -1.

This means PRED ZERO = ZERO is not a limitation or a workaround. It falls out naturally from the pair-shifting construction: zero shifts leaves (ZERO, ZERO), and extracting the first element gives ZERO. The construction does not need a special case -- it simply bottoms out at zero.

If negative numbers are needed, they can be represented as pairs of Church numerals (a, b) meaning a - b, but that is a separate encoding built on top of Church numerals.

PRED -- What Matters

The full lambda expression for PRED is complex -- too complex to memorize or evaluate by hand. What matters is understanding the idea and the guarantees:

1. PRED exists as a pure lambda term. No extensions to the calculus are needed.
2. PRED uses pairs to remember the previous step while iterating forward.
3. PRED (SUCC n) = n for any Church numeral n. Predecessor undoes successor.
4. PRED ZERO = ZERO by convention. No negative Church numerals.

With PRED in hand, we can define subtraction: SUB m n applies PRED to m exactly n times. Subtraction "bottoms out" at zero -- it never goes negative.