Subtraction

SUB via iterated PRED. Why subtraction is hard.

5 topics • ~490 words

We learned to undo one layer of typesetting — the laborious pair-shifting trick that peels back a single impression. Now iterate the undoing. Each pass of PRED strips one round of f. Subtraction is just the peeling tool, used repeatedly.

We have addition, multiplication, and exponentiation -- all built from the same pattern: a Church numeral iterates a function. ADD iterates SUCC. MULT iterates ADD. Now we want subtraction. The natural approach is the same: iterate something that undoes one step. That something is PRED, the predecessor function we built from pairs.

Subtraction via PRED

Addition applies SUCC repeatedly: ADD m n applies SUCC n times to m, producing m + n.

Subtraction follows the same structure but goes the other direction: apply PRED n times to m. Each application of PRED removes one application of f from a Church numeral, so applying it n times removes n.

SUB m n = "start with m, apply PRED n times"

SUB Definition

The definition of SUB follows directly from the idea of iterating PRED:

SUB = λm.λn.n PRED m

Reading this: take two numerals m and n. Use n as an iterator -- it applies PRED to m exactly n times.

Compare with ADD = λm.λn.n SUCC m:

  • ADD gives n to SUCC and m as the starting value
  • SUB gives n to PRED and m as the starting value

The structure is identical. Only the one-step operation changes.

SUB THREE ONE

SUB = λm.λn.n PRED m applies PRED n times to m.

For SUB THREE ONE:

  • Start with THREE
  • ONE applies PRED exactly once
  • PRED THREE = TWO

The Church numeral ONE is λf.λx.f x -- it applies any function exactly once. Here that function is PRED and the starting value is THREE.

SUB Floor at ZERO

What happens when we subtract a larger number from a smaller one?

SUB ONE THREE applies PRED three times to ONE:

  • PRED ONE = ZERO
  • PRED ZERO = ZERO
  • PRED ZERO = ZERO

The result is ZERO. PRED cannot go below ZERO -- there is no Church numeral for negative numbers. Once you reach ZERO, further applications of PRED stay at ZERO.

This means Church subtraction is really monus (truncated subtraction): m ∸ n = max(m − n, 0).

Why Subtraction Is Hard

Compare the definitions of ADD and SUB:

  • ADD = λm.λn.n SUCC m
  • SUB = λm.λn.n PRED m

They have exactly the same structure. Yet subtraction is considered much harder than addition in lambda calculus. Why?

The difficulty is not in SUB itself -- it is in PRED. SUCC is simple: wrap one more f around the result. But PRED must remove an application of f, and Church numerals do not give you direct access to their internal structure. Building PRED required the pair-based trick -- constructing a pair that tracks "previous and current" through each iteration.

SUB inherits all of PRED's complexity. The definition is trivial once you have PRED. Getting PRED is the hard part.

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 Subtraction →