4. A First Example: Equality On Natural Numbers

Consider equality on natural numbers.

The function should return true when two natural numbers are the same and false otherwise.

Since each input is either zero or suc(...), we begin with the four constructor combinations:

Three cases are immediate.

zero equals zero.

zero does not equal a successor.

A successor does not equal zero.

So:

One case remains.

Two successors are equal exactly when what comes before their outer suc constructors is equal:

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

The completed table is:

The table makes three things especially easy to inspect.

Coverage

Every constructor combination appears.

There are two constructors for the first argument and two for the second.

The resulting four combinations all have entries.

This shows that no constructor case has simply been omitted.

Structure

The rows and columns are not arbitrary classifications imposed on the numbers afterwards.

They come directly from the way natural numbers are constructed.

Each input has one of the forms represented by the headers.

The table mirrors the structure of the type.

Recursive direction

Only one entry is recursive:

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

The recursive comparison is performed on k and l, each structurally smaller than the input from which it came.

If both numbers continue to be successors, the same reduction can be repeated.

Eventually at least one side reaches zero.

The table does not establish termination merely by being a table.

What it does is put two relevant features in plain view:

• all constructor combinations are covered;
• the only recursive call is made on smaller arguments.

In this simple setting, these are precisely the kinds of features we inspect when checking that evaluation proceeds toward a base case.

But case coverage alone is not enough.

Consider this table:

Both constructor cases have entries.

Yet the second entry merely calls the function again on the same input.

It does not move toward zero.

If we evaluate

$ f(suc(zero)), $

we obtain

$ f(suc(zero)), $

again and again.

The table makes the problem visible precisely because coverage and recursive progress occupy separate places in the representation.

A recursive definition can satisfy the first without satisfying the second.