4. A First Example: Equality on ℕ

We now look at a concrete example where recursion tables show their full strength: equality on the natural numbers.

We want to define the equality function. That function returns $true$ if two numbers are the same, and $false$ otherwise.

Using the constructors of the natural numbers, we begin by listing all possible cases:

Each cell represents one possible form of input. To define the function, we must fill every cell.

The row headers indicate the first argument of the function, and the column headers indicate the second. The cells where they meet indicate the result of the function on these two inputs.

Some cases are immediate.

• $zero$ and $zero$ are equal
• $zero$ and $suc(l)$ are not equal
• $suc(k)$ and $zero$ are not equal

This gives:

One case remains.

How do we compare $suc(k)$ and $suc(l)$?

They are equal exactly when $k$ and $l$ are equal. So we define:

$$ suc(k) = suc(l) \mapsto k = l $$

This completes the table:

Every possible input case is covered.

If we get suc(k) = suc(l), we reduce it to k = l. We do that until we reach one of the base cases. One of the two numbers, or both, must be $zero$ eventually.

The recursion case does not guess or inspect further structure. It simply removes one layer of construction from both numbers and repeats the same question. Each step moves closer to the base case.

This is where recursion tables show their force.

We do not need a separate argument to see that the function is total. Every case is visible in the table.

We do not need a separate argument to see that the function terminates. Each recursive step reduces both inputs toward $zero$.

The definition becomes convincing because its behavior can be inspected. Nothing is hidden. There is no case left unspecified, and no path that leads away from a result.

This is the kind of situation in which conviction about a definition forms easily: when all possibilities are visible and the process can be followed step by step.

Recursion tables thus show three things without proving them:

First, completeness.

The table has four cells, and all of them are filled. There is no situation left open. If you try to imagine an input for which the function is not defined, you will not find one, because every possible combination of zero and suc already appears.

Second, structure.

The rows and columns are not arbitrary. They follow the way the inputs are built. One input is either zero or suc(m). The other is either zero or suc(n). The table simply lists these possibilities and shows what happens in each case.

Third, direction.

In the bottom right cell, the function does not return a value immediately. Instead, it has to reduce the problem to one closer to the base cases, so it will eventually lead to a base case, where a value is given directly. Recursive application of the function will eventually reach one of the cases where a value is given directly.

Taken together, this means that the table tells the readers everything they need to know about the function.

One can check that every case is covered. One can see how the inputs are taken apart. And one can follow how the computation proceeds until it reaches a result.

This is what recursion tables are meant to provide: not a formal proof, but a way to inspect a definition and understand how it works by looking at it.