Recursion and Arithmetic

Lambda Calculus

2026-08-19 09:45

Where we are

What unit 3 left you

Truth values, the conditional, NOT/AND/OR.

The natural numbers, with succ, pred and iszero.

But succ steps by one.

To add \(m\) and \(n\) you must apply succ \(n\) times.

And nothing repeats

The calculus has no loop.

Unit 1 said repetition is recursion.

So define addition recursively and we are done.

We are not.

The route

1. see the failure, on addition
2. pass a function to itself
3. fix the evaluation order
4. generalise into a recursion function
5. wrap it in rec
6. build the arithmetic

The hardest unit of the module, and the one that completes it.

Iteration and recursion

Two ways to repeat

Iteration — go round again, updating variables.

Needs mutable state. Unavailable.

Recursion — nest calls, each on a smaller problem.

Every recursive definition needs two parts

• a base case that terminates without a further call
• a recursive case that calls on something strictly smaller

No base case → never stops.

A case that does not shrink → never stops.

Primitive vs general

Primitive recursion

number of repetitions known

finite nesting depth

= bounded iteration, finite memory

General recursion

number of repetitions unknown

unknown nesting depth

= unbounded iteration, infinite memory

Primitive is strictly weaker.

Where the difficulty is

The structure is unremarkable. You have written recursive functions before.

The problem here is that a recursive definition needs the function to refer to itself.

Why a recursive definition fails

It looks like it should work

def add x y =
    if iszero y
    then x
    else add (succ x) (pred y)

add one two => ... =>
add (succ one) (pred two) => ... =>
add (succ (succ one)) (pred (pred two)) => ... =>
three

But recall the rule from unit 2

All names in expressions must be replaced by their definitions before the expression is evaluated.

Apply that rule

λx.λy. if iszero y then x else add (succ x) (pred y) ==

λx.λy. if iszero y then x else
    ((λx.λy. if iszero y then x else add (succ x) (pred y))
     (succ x) (pred y)) ==

λx.λy. if iszero y then x else
    ((λx.λy. if iszero y then x else
        ((λx.λy. if iszero y then x else add (succ x) (pred y))
         (succ x) (pred y)))
     (succ x) (pred y)) == ...

Replacement will never terminate.

The diagnosis

Most languages

a name is a reference

resolved at call time

so a function can name itself

Here

a name is an abbreviation

expanded before evaluation

so it never finishes

Why we cannot just stop early

We want replacement to happen a finite number of times, depending on the arguments.

But there is no way of knowing the arguments when the function is defined.

If we did know, we could construct specific functions for specific cases rather than a general purpose one.

What we need

Some means of delaying the repetitive use of the function until it is actually required.

Passing a function to itself

The lever

Function use always occurs in an application — and can be delayed by abstraction at the point of use.

<function> <argument>

is equivalent to

λf.(f <argument>) <function>

First attempt

def add1 f x y =
    if iszero y
    then x
    else f (succ x) (pred y)

def add = add1 add1

It does not go deep enough

(λf.λx.λy.
    if iszero y
    then x
    else f (succ x) (pred y)) add1 =>
λx.λy.
    if iszero y
    then x
    else add1 (succ x) (pred y)

add1 (succ x) (pred y) has no argument for the bound variable f.

We need

add1 add1 (succ x) (pred y)

so that add1 gets passed on to subsequent recursions.

Second attempt

def add2 f x y =
    if iszero y
    then x
    else f f x y

def add = add2 add2

Self-reference is now an ordinary argument.

The cost

It works, and it is unpleasant.

Every call passes the function to itself explicitly.

Every definition is written in this contorted shape.

A technique, not a solution.

Applicative order

The convention

Applicative order — reduce the argument to a value before substituting it.

Pascal’s call by value.

Why this is not cosmetic

From unit 2: self-application applied to itself reduces forever.

• the recursion trick applies a function to itself
• applicative order evaluates arguments first
• so the self-application is evaluated first — and never finishes

The trap

Reduction never reaches the function body…

…where the base case that would have stopped it lives.

The requirement this sets

We cannot simply hand a function to itself.

The self-application must happen only when needed —

after the conditional has had its chance to select the base case.

This requirement is the entire design of the recursion function. Without it the next section’s shape looks arbitrary.

The recursion function

The goal

A constructor function that builds a recursive function from a non-recursive one, with a single abstraction at the recursion point.

Multiplication, recursively

def mult x y =
    if iszero y
    then zero
    else add x (mult x (pred y))

mult three two => ... =>
add three (mult three (pred two)) -> ... ->
add three (add three zero) -> ... ->
six

Abstract at the recursion point

def mult1 f x y =
    if iszero y
    then zero
    else add x (f x (pred y))

We want:

def mult = recursive mult1

What recursive must do

Pass a copy of its argument to that argument…

…and ensure self-application continues — the copying mechanism must be passed on too.

def recursive f = f <'f' and copy>

Apply it to mult1

recursive mult1 ==
λf.(f <'f' and copy>) mult1 =>
mult1 <'mult1' and copy> ==
(λf.λx.λy.
    if iszero y
    then zero
    else add x (f x (pred y))) <'mult1' and copy> =>
λx.λy.
    if iszero y
    then zero
    else add x (<'mult1' and copy> x (pred y))

The gap

We have:

<'mult1' and copy> x (pred y)

We need:

mult1 <'mult1' and copy> x (pred y)

So the copy must self-replicate

<'f' and copy> => ... => f <'f' and copy>

The copy mechanism must be an application, and that application must be self-replicating.

We have seen self-replication

\[\lambda s.(s\ s)\]

applied to itself replicates forever.

Forever is too long. We need it to pause and hand control to \(f\).

The recursion function

def recursive f = λs.(f (s s)) λs.(f (s s))

def mult = recursive mult1

Where the delay lives

\[\lambda s.(s\ s)\]

replicates forever

\[\lambda s.(f\ (s\ s))\]

replicates through \(f\)

Each round passes through the conditional — which may pick the base case and stop.

That wrapping is the whole trick

Everything else is bookkeeping.

The calculus now has abstraction, application and unbounded repetition.

There is nothing computable left that it cannot express.

rec notation

Naming it

recursive is the paradoxical combinator, or fixed point finder.

Called \(Y\) in the λ calculus literature.

The sugar

rec <name> = <expression>

The name in the definition is replaced by abstraction, and the combinator applied to the whole defining expression.

Before and after

def add1 f x y =
    if iszero y
    then x
    else f (succ x) (pred y)

def add = recursive add1

rec add x y =
    if iszero y
    then x
    else add (succ x) (pred y)

Still just sugar

rec adds nothing to the language.

Three grammar productions. β, α, η.

Third time this module has done this: sugar in unit 2, notation in unit 3, rec here.

Arithmetic from recursion

Power

rec power x y =
    if iszero y
    then one
    else mult x (power x (pred y))

power two three => ... =>
mult two (power two (pred three)) -> ... ->
mult two (mult two (power two (pred (pred three)))) -> ...

Subtraction

rec sub x y =
    if iszero y
    then x
    else sub (pred x) (pred y)

sub four two => ... =>
sub (pred (pred four)) (pred (pred two)) => ... =>
two

Natural subtraction

sub one two => ... =>
pred (pred one) -> ... ->
pred zero => ... =>
zero

Returns zero when the second is larger — because pred zero is zero.

Comparison, via absolute difference

def abs_diff x y = add (sub x y) (sub y x)
def equal x y = iszero (abs_diff x y)

One of the two subtractions is always zero, so the sum is the real difference.

Or recursively

rec equal x y =
    if and (iszero x) (iszero y)
    then true
    else
    if or (iszero x) (iszero y)
    then false
    else equal (pred x) (pred y)

def greater x y = not (iszero (sub x y))
def greater_or_equal x y = iszero (sub y x)

Division

rec div1 x y =
    if greater y x
    then zero
    else succ (div1 (sub x y) y)

def div x y =
    if iszero y
    then zero
    else div1 x y

Count how often the divisor subtracts before the dividend gets smaller.

They all share one shape

1. a conditional testing the base case
2. a base case returning directly
3. a recursive call on a number one step smaller

The interest is in the base cases — where each decides what to do at zero.

Summary

What just happened

Three grammar productions. Three conversion rules.

Selectors, pairs, booleans, the conditional, the naturals, and now full arithmetic.

Every one expands to pure λ terms.

The hard part was repetition

Abstraction and application alone are not obviously enough.

The obstacle was real.

The paradoxical combinator is what removes it.

The six things to carry away

• Repetition is recursion: a base case and a strictly smaller call.
• A self-mentioning definition cannot work — a name is an abbreviation, not a reference.
• Self-application solves it, clumsily: pass f f, not f.
• The combinator delays the self-application by routing it through f.
• rec is sugar over the combinator, adding nothing to the language.
• Arithmetic follows quickly; the decisions are all at the zero boundary.

For real languages

Everything you use — numbers, booleans, conditionals, data structures, recursion — is either primitive for efficiency or definable in the core.

The core has not changed since Church.

When you write if, or a recursive function, the derivation you now know is underneath.