Lecture notes — Recursion and Arithmetic

Published

2026-08-19 00:00

Keywords

ver. 1.0.0

Where we are

In Conditions, Booleans and Integers you built truth values as selectors, the conditional, the boolean operators, and the natural numbers with succ, pred and iszero.

It stopped one step short of arithmetic, and the reason is worth stating plainly. succ moves up by one. pred moves down by one. To add $m$ and $n$ you must apply succ $n$ times — and the calculus has no way to repeat anything.

Unit 1 said repetition in functional programming is recursion. So define addition recursively and the problem is solved. Except it is not, and finding out why is the first real work of this unit.

What you will be able to do

explain-recursion-as-repetition — Explain how recursion provides repetition through nested function application.
diagnose-the-self-reference-problem — Explain why a definition that mentions its own name cannot work in the λ calculus.
pass-a-function-to-itself — Give a function access to itself by passing it as one of its own arguments.
use-applicative-order-notation — Use applicative order reduction and say where it forces the derivations to be arranged.
derive-the-recursion-function — Derive the recursion function (the paradoxical combinator) and explain how it delays self-application.
use-rec-notation — Use the rec notation as sugar for the recursion function.
build-arithmetic-operations — Build arithmetic and comparison operations on the natural numbers using recursion.

What we will cover

Iteration and recursion — two forms of repetition, only one of which is available here.
Primitive and general recursion — repetition with a known and an unknown number of steps.
Self-application — passing a function to itself so it never needs its own name.
Applicative order — evaluating an argument before substituting it.
Paradoxical combinator — the recursion function, called $Y$ in the literature; a fixed point finder.
rec notation — sugar that lets a defined name appear in its own defining expression.
Arithmetic operations — power, natural subtraction, comparison and division.

Repetition without a loop

The route this unit takes:

see the failure concretely, on addition
pass a function to itself as an argument, so it never needs its own name
fix the evaluation order the derivations assume
generalise the trick into a single recursion function
wrap it in rec notation
build the arithmetic that has been waiting

This is the hardest unit of the module and the one that completes it. After this, the calculus can compute anything.

Learning outcomes

explain-recursion-as-repetition: Explain how recursion provides repetition through nested function application.
diagnose-the-self-reference-problem: Explain why a definition that mentions its own name cannot work in the λ calculus.

Iteration and recursion

Iteration repeats by going round again, updating variables each time. That needs mutable state, which we do not have. Recursion repeats by nesting: a call whose answer depends on another call of the same shape, on a smaller problem.

Every recursive definition needs two parts:

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

Both are load-bearing. No base case and it never stops. A recursive case that does not shrink the problem and it never stops either.

Primitive and general recursion

It is useful to distinguish:

primitive recursion, where the number of repetitions is known

A finite depth of call nesting, so it is equivalent to bounded repetition through iteration with a finite memory.
general recursion, where the number of repetitions is unknown

The nesting depth is unknown, so it is equivalent to unbounded repetition through iteration with an infinite memory.

Primitive recursion is weaker than general recursion. Note also that imperative languages often provide repetition through recursive procedures and functions as well as through iteration — recursion is not exclusive to this style.

Where the difficulty is. The structure above is unremarkable; you have written recursive functions before. The problem specific to this calculus is not the structure. It is that a recursive definition needs the function to refer to itself.

Learning outcomes

explain-recursion-as-repetition: Explain how recursion provides repetition through nested function application.

Concepts

recursion: distinguishes iteration from recursive nesting, and primitive from general recursion

Why a recursive definition fails

It might appear that our definition notation already enables recursion — just use the name from the left of the definition in the expression on the right.

Two numbers may be added by repeatedly incrementing the first and decrementing the second until the second is zero:

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

And it seems to work:

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

The expansion

But in unit 2 we required all names in expressions to be replaced by their definitions before the expression is evaluated. Apply that rule here:

λ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

This is not a subtle bug. It is a consequence of what a name is here:

in 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 a self-mentioning definition has no finite expansion at all

We want the replacement to take place a finite number of times, depending on the particular arguments. But there is no way of knowing what argument values are required when the function is defined. If we did know, we could construct specific functions for specific cases rather than a general purpose one.

This was not a problem in earlier units because replacement was always finite.

What we actually need

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

That word — delaying — is the whole design of everything that follows.

Learning outcomes

diagnose-the-self-reference-problem: Explain why a definition that mentions its own name cannot work in the λ calculus.

Concepts

recursion: shows why a self-mentioning definition has no finite expansion

Passing a function to itself

Function use always occurs in an application, and may be delayed through abstraction at the point where the function is used. For any function, the application

<function> <argument>

is equivalent to

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

The original function becomes the argument in a new application. That is the lever.

First attempt

Introduce a new argument at the recursion point:

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

Now we need an argument for add1 with the same effect as add. We cannot pass add — that is the non-terminating replacement again. So pass add1 into itself:

def add = add1 add1

which expands to:

(λ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)

We have failed to pass add1 down far enough. In the original definition, the application f (succ x) (pred y) has only two arguments. After substitution, add1 (succ x) (pred y) has no argument corresponding to the bound variable f.

We need the effect of add1 add1 (succ x) (pred y), so that add1 may be passed on to subsequent recursions.

Second attempt

Pass the argument for f to the argument itself as well:

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

with, as before:

def add = add2 add2

Now the self-reference has become an ordinary argument, and arguments are something the calculus already handles.

The cost

It works, and it is unpleasant. Every recursive call must pass the function to itself explicitly, and every definition must be written in this contorted shape. It is a technique, not a solution.

But the idea to keep is this: self-application is what makes recursion possible. The next two sections factor the trick out, so it is performed once by a general-purpose function rather than written by hand into every definition.

Learning outcomes

pass-a-function-to-itself: Give a function access to itself by passing it as one of its own arguments.
explain-recursion-as-repetition: Explain how recursion provides repetition through nested function application.

Concepts

self-application: removes self-reference by abstraction, passing the function in as its own argument

Applicative order

We met the two evaluation orders in unit 2 and set the difference aside. It now matters, so we fix a convention.

Applicative order reduces the argument to a value before substituting it into the function body — Pascal’s call by value. The chapter adopts it for the derivations that follow, and we use its notation.

Why this is not cosmetic

Recall from unit 2 that self-application applied to itself reduces forever. Now put the two facts together:

the recursion trick works by applying a function to itself
applicative order insists on evaluating an argument before substituting it
so a self-application appearing as an argument gets evaluated first — and never finishes

The reduction never reaches the function body, where the base case that would have stopped it lives.

The requirement this sets

Whatever we build in the next section cannot simply hand a function to itself. It has to arrange for the self-application to happen only when it is needed — after the conditional has had its chance to select the base case.

That requirement is the entire design of the recursion function. Read the next section with this constraint in mind, or its shape will look arbitrary.

Learning outcomes

use-applicative-order-notation: Use applicative order reduction and say where it forces the derivations to be arranged.

Concepts

evaluation-order: fixes applicative order and shows why it constrains the recursion construction

The recursion function

A more general approach: find a constructor function to build a recursive function from a non-recursive one, with a single abstraction at the recursion point.

The example

Multiplication, defined recursively. To multiply two numbers, add the first to the product of the first and the decremented second; if the second is zero, so is the product:

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 (mult three (pred (pred two)))) -> ... ->
add three (add three zero) -> ... ->
add three three => ... =>
six

Remove the self-reference by abstraction at the recursion point:

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

and we would like a function recursive such that:

def mult = recursive mult1

What `recursive` has to do

It must not only pass a copy of its argument to that argument, but also ensure self-application will continue: the copying mechanism must be passed on as well. So it should be of the form:

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))

In the body we have <'mult1' and copy> x (pred y) but we require mult1 <'mult1' and copy> x (pred y), so that the copy gets passed on again through mult1’s bound variable f to the next level.

So the copy mechanism must satisfy:

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

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

Finding it

We know that the self-application function $\lambda s.(s\ s)$ will self-replicate when applied to itself — but the replication never ends. What we need is self-replication that pauses to hand control back to $f$ each time round. That gives:

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

and then:

def mult = recursive mult1

Where the delay lives

Compare $\lambda s.(s\ s)$ with $\lambda s.(f\ (s\ s))$. The second wraps the self-application inside a call to $f$. So each round of replication passes through $f$ — which is the conditional — giving the base case a chance to stop the whole thing before the next self-application is demanded.

That wrapping is the entire trick. Everything else is bookkeeping.

Why this completes the module. The calculus already had abstraction and application. With the recursion function it has unbounded repetition too, and there is nothing computable left that it cannot express.

Learning outcomes

derive-the-recursion-function: Derive the recursion function (the paradoxical combinator) and explain how it delays self-application.
pass-a-function-to-itself: Give a function access to itself by passing it as one of its own arguments.
use-applicative-order-notation: Use applicative order reduction and say where it forces the derivations to be arranged.

Concepts

paradoxical-combinator: derives the recursion function as a self-replicating application routed through f
self-application: shows the self-application at the heart of the combinator, wrapped so it terminates

`rec` notation

The function recursive is known as a paradoxical combinator or a fixed point finder, and is called $Y$ in the λ calculus literature.

Rather than always defining an auxiliary function with an abstraction and then using recursive to construct a recursive version, we allow the defined name to appear in the defining expression, using a new definition form:

rec <name> = <expression>

This indicates that the occurrence of the name should be replaced using abstraction, and the paradoxical combinator then applied to the whole defining expression.

So for addition we write:

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

instead of:

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

and for multiplication:

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

When we expand or evaluate a recursive definition we just leave the recursive reference in place.

Still just sugar

rec adds nothing to the language. The grammar is still three productions and the conversions are still β, α and η. When a recursive derivation confuses you, expanding rec back to the combinator is how to find out what is really happening.

This is the third time the module has done this — syntactic sugar in unit 2, the number and boolean notations in unit 3, rec here. It is how a real functional language is built: a tiny core, and layers of notation each explained by translation into the layer below.

Learning outcomes

use-rec-notation: Use the rec notation as sugar for the recursion function.
derive-the-recursion-function: Derive the recursion function (the paradoxical combinator) and explain how it delays self-application.

Concepts

paradoxical-combinator: names the combinator as $Y$ and wraps it in the rec definition form
syntactic-sugar: adds rec as an abbreviation that expands to the combinator

Arithmetic from recursion

With recursion available, the arithmetic that has been waiting since unit 3 falls out. Everything below uses only what the module has already built.

Power

To raise one number to the power of another, multiply the first by the first to the power of the decremented second. If the second is zero the power is one:

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)))) -> ... ->
mult two (mult two (mult two (power two (pred (pred (pred three)))))) -> ...

Subtraction

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

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

Notice this returns zero if the second number is larger than the first:

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

because pred returns zero from decrementing zero. This is known as natural subtraction.

Comparison

The difference between two equal numbers is zero — but subtracting a number from a smaller one also gives zero, so we need the absolute difference, regardless of order:

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

If both are the same, both subtractions give zero. If one is greater, the other subtraction gives zero, so the sum is the real difference. Hence:

def equal x y = iszero (abs_diff x y)

equal two three => ... =>
iszero (abs_diff two three) -> ... ->
iszero (add (sub two three) (sub three two)) -> ... ->
iszero (add zero one) -> ... ->
iszero one => ... =>
false

Equality can equally well be defined recursively — two numbers are equal if both are zero, unequal if one is zero, and otherwise equal if decrementing both gives equal numbers:

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)

Inequalities follow the same way:

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

Division

Division, like decrementation, is problematic because of zero. It is usual to define division by zero as undefined, but we have no way of dealing with undefined values — so we define it to be zero and remember to check for a zero divisor.

For a non-zero divisor, count how often it can be subtracted from the dividend until the dividend is smaller:

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

div nine four => ... =>
div1 nine four => ... =>
succ (div1 (sub nine four) four)) -> ... ->
succ (div1 five four) -> ... ->
succ (succ (div1 (sub five four) four)) -> ... ->

Key ideas

Every operation has the same shape: a conditional testing a base case, and a recursive call on a smaller number.
The interest is in the base cases — where each definition decides what to do at the boundary.
sub, div and pred all have to make a decision about zero, and all three choose zero rather than an undefined value.
Comparison is built from subtraction, which is why it comes after it.

Learning outcomes

build-arithmetic-operations: Build arithmetic and comparison operations on the natural numbers using recursion.
use-rec-notation: Use the rec notation as sugar for the recursion function.

Concepts

arithmetic-operations: builds power, natural subtraction, comparison and division from succ, pred and recursion
recursion: applies the base-case-plus-smaller-call shape to every operation

What the calculus can now do

Step back over the whole module.

We began with a language of three productions — a name, a function, an application — and three conversion rules. That is all there ever was; nothing was added to the language after unit 2.

From it we built selectors, pairs, truth values, the conditional, the boolean operators, the natural numbers, succ, pred, iszero, and now full arithmetic. Every one of them expands to pure λ terms.

The last piece was repetition, and it was the hard one. Abstraction and application alone are not obviously enough for unbounded computation — the obstacle was real, and the paradoxical combinator is the thing that removes it.

What to take away for real languages. Everything you use in a functional language — 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, or a tuple, the derivation you now know is what is underneath.

Learning outcomes

explain-recursion-as-repetition: Explain how recursion provides repetition through nested function application.
diagnose-the-self-reference-problem: Explain why a definition that mentions its own name cannot work in the λ calculus.
pass-a-function-to-itself: Give a function access to itself by passing it as one of its own arguments.
use-applicative-order-notation: Use applicative order reduction and say where it forces the derivations to be arranged.
derive-the-recursion-function: Derive the recursion function (the paradoxical combinator) and explain how it delays self-application.
use-rec-notation: Use the rec notation as sugar for the recursion function.
build-arithmetic-operations: Build arithmetic and comparison operations on the natural numbers using recursion.

Concepts

paradoxical-combinator: collects the combinator as the piece that completes the calculus
arithmetic-operations: collects the operations built on top of it

Conclusion

Repetition in functional programming relies on recursion, not iteration.

A loop needs mutable state. Recursion nests calls instead: a base case that stops, and a recursive case on a strictly smaller problem.
A definition that mentions its own name cannot work here.

A name is an abbreviation expanded before evaluation, not a reference resolved at call time. Expanding a self-mentioning definition never terminates, so it never becomes a λ expression at all.
Self-application solves it, clumsily at first.

Give the function an extra parameter and pass the function in through it. add2 f x y must pass f f, not just f, or the next level of recursion has nothing to call.
The paradoxical combinator delays the self-application.

def recursive f = λs.(f (s s)) λs.(f (s s)) routes each round of replication through f, so the conditional gets a chance to select the base case before the next self-application is demanded.
rec is syntactic sugar over the combinator.

It adds nothing to the language. The grammar is still three productions; expanding rec is how to see what a recursive derivation really does.
Arithmetic follows quickly once recursion exists.

Power, natural subtraction, equality, inequality and division are all the same shape — a base case and a call on a smaller number. The interesting decisions are all at the zero boundary.

← Recursion and Arithmetic

--- title: Lecture notes — Recursion and Arithmetic keywords: - ver. 1.0.0 date: '2026-08-19' --- [← Recursion and Arithmetic](index.qmd){.hg-back} ## Where we are In **Conditions, Booleans and Integers** you built truth values as selectors, the conditional, the boolean operators, and the natural numbers with `succ`, `pred` and `iszero`. It stopped one step short of arithmetic, and the reason is worth stating plainly. `succ` moves up by one. `pred` moves down by one. To add $m$ and $n$ you must apply `succ` $n$ times — and the calculus has no way to repeat anything. Unit 1 said repetition in functional programming is recursion. So define addition recursively and the problem is solved. Except it is not, and finding out why is the first real work of this unit. ## What you will be able to do 1. `explain-recursion-as-repetition` — Explain how recursion provides repetition through nested function application. 2. `diagnose-the-self-reference-problem` — Explain why a definition that mentions its own name cannot work in the λ calculus. 3. `pass-a-function-to-itself` — Give a function access to itself by passing it as one of its own arguments. 4. `use-applicative-order-notation` — Use applicative order reduction and say where it forces the derivations to be arranged. 5. `derive-the-recursion-function` — Derive the recursion function (the paradoxical combinator) and explain how it delays self-application. 6. `use-rec-notation` — Use the rec notation as sugar for the recursion function. 7. `build-arithmetic-operations` — Build arithmetic and comparison operations on the natural numbers using recursion. ## What we will cover - **Iteration and recursion** — two forms of repetition, only one of which is available here. - **Primitive and general recursion** — repetition with a known and an unknown number of steps. - **Self-application** — passing a function to itself so it never needs its own name. - **Applicative order** — evaluating an argument before substituting it. - **Paradoxical combinator** — the recursion function, called $Y$ in the literature; a fixed point finder. - **`rec` notation** — sugar that lets a defined name appear in its own defining expression. - **Arithmetic operations** — power, natural subtraction, comparison and division. ## Repetition without a loop The route this unit takes: 1. see the failure concretely, on addition 2. pass a function **to itself** as an argument, so it never needs its own name 3. fix the evaluation order the derivations assume 4. generalise the trick into a single **recursion function** 5. wrap it in `rec` notation 6. build the arithmetic that has been waiting This is the hardest unit of the module and the one that completes it. After this, the calculus can compute anything. ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "explain-recursion-as-repetition" >}}: Explain how recursion provides repetition through nested function application. - {{< badge outcome "diagnose-the-self-reference-problem" >}}: Explain why a definition that mentions its own name cannot work in the λ calculus. ::: ## Iteration and recursion Iteration repeats by going round again, updating variables each time. That needs mutable state, which we do not have. Recursion repeats by **nesting**: a call whose answer depends on another call of the same shape, on a smaller problem. Every recursive definition needs two parts: - a **base case** that terminates without a further call - a **recursive case** that calls again on something strictly smaller Both are load-bearing. No base case and it never stops. A recursive case that does not shrink the problem and it never stops either. ### Primitive and general recursion It is useful to distinguish: - **primitive recursion**, where the number of repetitions is known > A finite depth of call nesting, so it is equivalent to bounded repetition through iteration with a finite memory. - **general recursion**, where the number of repetitions is unknown > The nesting depth is unknown, so it is equivalent to unbounded repetition through iteration with an infinite memory. Primitive recursion is weaker than general recursion. Note also that imperative languages often provide repetition through recursive procedures and functions as well as through iteration — recursion is not exclusive to this style. **Where the difficulty is.** The structure above is unremarkable; you have written recursive functions before. The problem specific to this calculus is not the structure. It is that a recursive definition needs the function to *refer to itself*. ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "explain-recursion-as-repetition" >}}: Explain how recursion provides repetition through nested function application. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "recursion" >}}: distinguishes iteration from recursive nesting, and primitive from general recursion ::: ## Why a recursive definition fails It might appear that our definition notation already enables recursion — just use the name from the left of the definition in the expression on the right. Two numbers may be added by repeatedly incrementing the first and decrementing the second until the second is zero: ```text def add x y = if iszero y then x else add (succ x) (pred y) ``` And it seems to work: ```text add one two => ... => add (succ one) (pred two) => ... => add (succ (succ one)) (pred (pred two)) => ... => (succ (succ one)) == three ``` ### The expansion But in unit 2 we required **all names in expressions to be replaced by their definitions before the expression is evaluated**. Apply that rule here: ```text λ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 This is not a subtle bug. It is a consequence of what a name *is* here: - in 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 a self-mentioning definition has no finite expansion at all We want the replacement to take place a finite number of times, depending on the particular arguments. But there is no way of knowing what argument values are required when the function is *defined*. If we did know, we could construct specific functions for specific cases rather than a general purpose one. This was not a problem in earlier units because replacement was always finite. ::: {.callout-important title="What we actually need"} Some means of **delaying** the repetitive use of the function until it is actually required. That word — delaying — is the whole design of everything that follows. ::: ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "diagnose-the-self-reference-problem" >}}: Explain why a definition that mentions its own name cannot work in the λ calculus. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "recursion" >}}: shows why a self-mentioning definition has no finite expansion ::: ## Passing a function to itself Function use always occurs in an application, and may be **delayed through abstraction at the point where the function is used**. For any function, the application ```text <function> <argument> ``` is equivalent to ```text λf.(f <argument>) <function> ``` The original function becomes the argument in a new application. That is the lever. ### First attempt Introduce a new argument at the recursion point: ```text def add1 f x y = if iszero y then x else f (succ x) (pred y) ``` Now we need an argument for `add1` with the same effect as `add`. We cannot pass `add` — that is the non-terminating replacement again. So pass `add1` into itself: ```text def add = add1 add1 ``` which expands to: ```text (λ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) ``` **We have failed to pass `add1` down far enough.** In the original definition, the application `f (succ x) (pred y)` has only two arguments. After substitution, `add1 (succ x) (pred y)` has no argument corresponding to the bound variable `f`. We need the effect of `add1 add1 (succ x) (pred y)`, so that `add1` may be passed on to subsequent recursions. ### Second attempt Pass the argument for `f` to the argument itself as well: ```text def add2 f x y = if iszero y then x else f f x y ``` with, as before: ```text def add = add2 add2 ``` Now the self-reference has become an ordinary argument, and arguments are something the calculus already handles. ### The cost It works, and it is unpleasant. Every recursive call must pass the function to itself explicitly, and every definition must be written in this contorted shape. It is a technique, not a solution. But the idea to keep is this: [self-application is what makes recursion possible.]{.hg-key} The next two sections factor the trick out, so it is performed once by a general-purpose function rather than written by hand into every definition. ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "pass-a-function-to-itself" >}}: Give a function access to itself by passing it as one of its own arguments. - {{< badge outcome "explain-recursion-as-repetition" >}}: Explain how recursion provides repetition through nested function application. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "self-application" >}}: removes self-reference by abstraction, passing the function in as its own argument ::: ## Applicative order We met the two evaluation orders in unit 2 and set the difference aside. It now matters, so we fix a convention. **Applicative order** reduces the argument to a value before substituting it into the function body — Pascal's call by value. The chapter adopts it for the derivations that follow, and we use its notation. ### Why this is not cosmetic Recall from unit 2 that self-application applied to itself reduces forever. Now put the two facts together: - the recursion trick works by applying a function to itself - applicative order insists on evaluating an argument **before** substituting it - so a self-application appearing as an argument gets evaluated first — and never finishes The reduction never reaches the function body, where the base case that would have stopped it lives. ::: {.callout-important title="The requirement this sets"} Whatever we build in the next section cannot simply hand a function to itself. It has to arrange for the self-application to happen **only when it is needed** — after the conditional has had its chance to select the base case. That requirement is the entire design of the recursion function. Read the next section with this constraint in mind, or its shape will look arbitrary. ::: ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "use-applicative-order-notation" >}}: Use applicative order reduction and say where it forces the derivations to be arranged. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "evaluation-order" >}}: fixes applicative order and shows why it constrains the recursion construction ::: ## The recursion function A more general approach: find a **constructor function** to build a recursive function from a non-recursive one, with a single abstraction at the recursion point. ### The example Multiplication, defined recursively. To multiply two numbers, add the first to the product of the first and the decremented second; if the second is zero, so is the product: ```text def mult x y = if iszero y then zero else add x (mult x (pred y)) ``` ```text mult three two => ... => add three (mult three (pred two)) -> ... -> add three (add three (mult three (pred (pred two)))) -> ... -> add three (add three zero) -> ... -> add three three => ... => six ``` Remove the self-reference by abstraction at the recursion point: ```text def mult1 f x y = if iszero y then zero else add x (f x (pred y)) ``` and we would like a function `recursive` such that: ```text def mult = recursive mult1 ``` ### What `recursive` has to do It must not only pass a copy of its argument to that argument, but also ensure **self-application will continue**: the copying mechanism must be passed on as well. So it should be of the form: ```text def recursive f = f <'f' and copy> ``` Apply it to `mult1`: ```text 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)) ``` In the body we have `<'mult1' and copy> x (pred y)` but we require `mult1 <'mult1' and copy> x (pred y)`, so that the copy gets passed on again through `mult1`'s bound variable `f` to the next level. So the copy mechanism must satisfy: ```text <'f' and copy> => ... => f <'f' and copy> ``` The copy mechanism must be an **application**, and that application must be **self-replicating**. ### Finding it We know that the self-application function $\lambda s.(s\ s)$ will self-replicate when applied to itself — but the replication never ends. What we need is self-replication that pauses to hand control back to $f$ each time round. That gives: ```text def recursive f = λs.(f (s s)) λs.(f (s s)) ``` and then: ```text def mult = recursive mult1 ``` ::: {.callout-note title="Where the delay lives"} Compare $\lambda s.(s\ s)$ with $\lambda s.(f\ (s\ s))$. The second wraps the self-application inside a call to $f$. So each round of replication passes through $f$ — which is the conditional — giving the base case a chance to stop the whole thing before the next self-application is demanded. That wrapping is the entire trick. Everything else is bookkeeping. ::: **Why this completes the module.** The calculus already had abstraction and application. With the recursion function it has unbounded repetition too, and there is nothing computable left that it cannot express. ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "derive-the-recursion-function" >}}: Derive the recursion function (the paradoxical combinator) and explain how it delays self-application. - {{< badge outcome "pass-a-function-to-itself" >}}: Give a function access to itself by passing it as one of its own arguments. - {{< badge outcome "use-applicative-order-notation" >}}: Use applicative order reduction and say where it forces the derivations to be arranged. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "paradoxical-combinator" >}}: derives the recursion function as a self-replicating application routed through f - {{< badge concept "self-application" >}}: shows the self-application at the heart of the combinator, wrapped so it terminates ::: ## `rec` notation The function `recursive` is known as a **paradoxical combinator** or a **fixed point finder**, and is called $Y$ in the λ calculus literature. Rather than always defining an auxiliary function with an abstraction and then using `recursive` to construct a recursive version, we allow the defined name to appear in the defining expression, using a new definition form: ```text rec <name> = <expression> ``` This indicates that the occurrence of the name should be replaced using abstraction, and the paradoxical combinator then applied to the whole defining expression. So for addition we write: ```text rec add x y = if iszero y then x else add (succ x) (pred y) ``` instead of: ```text def add1 f x y = if iszero y then x else f (succ x) (pred y) def add = recursive add1 ``` and for multiplication: ```text rec mult x y = if iszero y then zero else add x (mult x (pred y)) ``` When we expand or evaluate a recursive definition we just leave the recursive reference in place. ::: {.callout-tip title="Still just sugar"} `rec` adds nothing to the language. The grammar is still three productions and the conversions are still β, α and η. When a recursive derivation confuses you, expanding `rec` back to the combinator is how to find out what is really happening. This is the third time the module has done this — syntactic sugar in unit 2, the number and boolean notations in unit 3, `rec` here. It is how a real functional language is built: a tiny core, and layers of notation each explained by translation into the layer below. ::: ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "use-rec-notation" >}}: Use the rec notation as sugar for the recursion function. - {{< badge outcome "derive-the-recursion-function" >}}: Derive the recursion function (the paradoxical combinator) and explain how it delays self-application. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "paradoxical-combinator" >}}: names the combinator as $Y$ and wraps it in the rec definition form - {{< badge concept "syntactic-sugar" >}}: adds rec as an abbreviation that expands to the combinator ::: ## Arithmetic from recursion With recursion available, the arithmetic that has been waiting since unit 3 falls out. Everything below uses only what the module has already built. ### Power To raise one number to the power of another, multiply the first by the first to the power of the decremented second. If the second is zero the power is one: ```text rec power x y = if iszero y then one else mult x (power x (pred y)) ``` ```text power two three => ... => mult two (power two (pred three)) -> ... -> mult two (mult two (power two (pred (pred three)))) -> ... -> mult two (mult two (mult two (power two (pred (pred (pred three)))))) -> ... ``` ### Subtraction ```text rec sub x y = if iszero y then x else sub (pred x) (pred y) ``` ```text sub four two => ... => sub (pred four) (pred two) => ... => sub (pred (pred four)) (pred (pred two)) => ... => (pred (pred four)) => ... => two ``` Notice this returns zero if the second number is larger than the first: ```text sub one two => ... => sub (pred one) (pred two) => ... => pred (pred one) -> ... -> pred zero => ... => zero ``` because `pred` returns zero from decrementing zero. This is known as **natural subtraction**. ### Comparison The difference between two equal numbers is zero — but subtracting a number from a smaller one also gives zero, so we need the **absolute** difference, regardless of order: ```text def abs_diff x y = add (sub x y) (sub y x) ``` If both are the same, both subtractions give zero. If one is greater, the other subtraction gives zero, so the sum is the real difference. Hence: ```text def equal x y = iszero (abs_diff x y) ``` ```text equal two three => ... => iszero (abs_diff two three) -> ... -> iszero (add (sub two three) (sub three two)) -> ... -> iszero (add zero one) -> ... -> iszero one => ... => false ``` Equality can equally well be defined recursively — two numbers are equal if both are zero, unequal if one is zero, and otherwise equal if decrementing both gives equal numbers: ```text 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) ``` Inequalities follow the same way: ```text def greater x y = not (iszero (sub x y)) def greater_or_equal x y = iszero (sub y x) ``` ### Division Division, like decrementation, is problematic because of zero. It is usual to define division by zero as undefined, but we have no way of dealing with undefined values — so we define it to be zero and remember to check for a zero divisor. For a non-zero divisor, count how often it can be subtracted from the dividend until the dividend is smaller: ```text 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 ``` ```text div nine four => ... => div1 nine four => ... => succ (div1 (sub nine four) four)) -> ... -> succ (div1 five four) -> ... -> succ (succ (div1 (sub five four) four)) -> ... -> ``` ::: {.highlights} <h1>Key ideas</h1> - Every operation has the same shape: a conditional testing a base case, and a recursive call on a smaller number. - The interest is in the **base cases** — where each definition decides what to do at the boundary. - `sub`, `div` and `pred` all have to make a decision about zero, and all three choose zero rather than an undefined value. - Comparison is built from subtraction, which is why it comes after it. ::: ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "build-arithmetic-operations" >}}: Build arithmetic and comparison operations on the natural numbers using recursion. - {{< badge outcome "use-rec-notation" >}}: Use the rec notation as sugar for the recursion function. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "arithmetic-operations" >}}: builds power, natural subtraction, comparison and division from succ, pred and recursion - {{< badge concept "recursion" >}}: applies the base-case-plus-smaller-call shape to every operation ::: ## What the calculus can now do Step back over the whole module. We began with a language of three productions — a name, a function, an application — and three conversion rules. That is all there ever was; nothing was added to the *language* after unit 2. From it we built selectors, pairs, truth values, the conditional, the boolean operators, the natural numbers, `succ`, `pred`, `iszero`, and now full arithmetic. Every one of them expands to pure λ terms. The last piece was repetition, and it was the hard one. Abstraction and application alone are not obviously enough for unbounded computation — the obstacle was real, and the paradoxical combinator is the thing that removes it. **What to take away for real languages.** Everything you use in a functional language — 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, or a tuple, the derivation you now know is what is underneath. ::: {.hypergen-refs .outcomes} <h1>Learning outcomes</h1> - {{< badge outcome "explain-recursion-as-repetition" >}}: Explain how recursion provides repetition through nested function application. - {{< badge outcome "diagnose-the-self-reference-problem" >}}: Explain why a definition that mentions its own name cannot work in the λ calculus. - {{< badge outcome "pass-a-function-to-itself" >}}: Give a function access to itself by passing it as one of its own arguments. - {{< badge outcome "use-applicative-order-notation" >}}: Use applicative order reduction and say where it forces the derivations to be arranged. - {{< badge outcome "derive-the-recursion-function" >}}: Derive the recursion function (the paradoxical combinator) and explain how it delays self-application. - {{< badge outcome "use-rec-notation" >}}: Use the rec notation as sugar for the recursion function. - {{< badge outcome "build-arithmetic-operations" >}}: Build arithmetic and comparison operations on the natural numbers using recursion. ::: ::: {.hypergen-refs .concepts} <h1>Concepts</h1> - {{< badge concept "paradoxical-combinator" >}}: collects the combinator as the piece that completes the calculus - {{< badge concept "arithmetic-operations" >}}: collects the operations built on top of it ::: ## Conclusion - Repetition in functional programming relies on recursion, not iteration. > A loop needs mutable state. Recursion nests calls instead: a base case that stops, and a recursive case on a strictly smaller problem. - A definition that mentions its own name cannot work here. > A name is an abbreviation expanded before evaluation, not a reference resolved at call time. Expanding a self-mentioning definition never terminates, so it never becomes a λ expression at all. - Self-application solves it, clumsily at first. > Give the function an extra parameter and pass the function in through it. `add2 f x y` must pass `f f`, not just `f`, or the next level of recursion has nothing to call. - The paradoxical combinator delays the self-application. > `def recursive f = λs.(f (s s)) λs.(f (s s))` routes each round of replication through `f`, so the conditional gets a chance to select the base case before the next self-application is demanded. - `rec` is syntactic sugar over the combinator. > It adds nothing to the language. The grammar is still three productions; expanding `rec` is how to see what a recursive derivation really does. - Arithmetic follows quickly once recursion exists. > Power, natural subtraction, equality, inequality and division are all the same shape — a base case and a call on a smaller number. The interesting decisions are all at the zero boundary. ::: {.hg-nav} [← Recursion and Arithmetic](index.qmd){.hg-prev} :::

Where we are

What you will be able to do

What we will cover

Repetition without a loop

Learning outcomes

Iteration and recursion

Primitive and general recursion

Learning outcomes

Concepts

Why a recursive definition fails

The expansion

The diagnosis

Learning outcomes

Concepts

Passing a function to itself

First attempt

Second attempt

The cost

Learning outcomes

Concepts

Applicative order

Why this is not cosmetic

Learning outcomes

Concepts

The recursion function

The example

What recursive has to do

Finding it

Learning outcomes

Concepts

rec notation

Learning outcomes

Concepts

Arithmetic from recursion

Power

Subtraction

Comparison

Division

Key ideas

Learning outcomes

Concepts

What the calculus can now do

Learning outcomes

Concepts

Conclusion

What `recursive` has to do

`rec` notation