6. From Recursion To Induction And Algorithms

Recursive definitions and proofs by structural induction have a closely related shape.

Recursion defines an object or function by following the constructors of its inputs.

Structural induction proves a property by following the same constructor structure.

For natural numbers, an inductive proof typically has two parts:

• establish the property for zero;
• establish that, if it holds for k, it also holds for suc(k).

This resembles a recursive definition because both follow the same way natural numbers are built.

Recursion tables can make that common structure easier to notice.

Consider the statement:

$$ n+zero=n. $$

For the particular definition of addition used above, the relevant column is already:

There are only two possible constructor forms for n.

When n is zero, adding zero returns zero.

When n is suc(k), adding zero returns suc(k).

For this definition, no additional inductive argument is required: the two possible forms of n are already represented directly by the defining clauses.

Many properties of recursively defined functions are not themselves part of the definition.

A recursion table may show how the function handles each constructor case and where its recursive calls go.

But if we want to prove some further property of the function, we may still need an inductive argument.

The table can help by making the relevant constructor structure visible, but it does not supply that proof by itself.

The table can nevertheless help by showing the constructor structure that such arguments will have to respect.

The same idea extends naturally to algorithms on other inductive data.

Lists

A finite list can be presented using two constructors:

• the empty list [];
• a list formed by attaching an element x to another list xs, written x :: xs.

The length function can then be written as:

$ len([\ ])=0 $

and

$ len(x::xs)=1+len(xs). $

As a table:

There are two constructor cases and both are covered.

The recursive case calls len on xs.

Since xs is the tail from which x :: xs was constructed, it is structurally smaller.

The same pattern appears in many recursive programs involving lists, trees, syntax trees, expressions, and other inductively constructed data.