Sample Code for this Chapter

The importance of induction and recursion are not limited to functions defined over the integers.  Rather, the familiar concept of mathematical induction over the natural numbers is an instance of the more general notion of structural induction over values of an inductively-defined type.  Rather than develop a general treatment of inductively-defined types, we will rely on a few examples to illustrate the point.

Let's begin by considering the natural numbers as an inductively defined type.   The set of natural numbers, N, may be thought of as the smallest set containing 0 and closed under the formation of successors.  In other words, n is an element of N iff either n=0 or n=m+1 for some m in N.  Still another way of saying it is to define N by the following clauses:

1. 0 is an element of N.
2. If m is an element of N, then so is m+1.
3. Nothing else is an element of N.

(The third clause is sometimes called the extremal clause; it ensures that we are talking about N and not just some superset of it.) All of these definitions are equivalent ways of saying the same thing.

Since N is inductively defined, we may prove properties of the natural numbers by structural induction, which in this case is just ordinary mathematical induction.  Specifically, to prove that a property P(n) holds of every n in N, it suffices to demonstrate the following facts:

1. Show that P(0) holds.
2. Assuming that P(m) holds, show that P(m+1) holds.

The pattern of reasoning follows exactly the structure of the inductive definition --- the base case is handled outright, and the inductive step is handled by assuming the property for the predecessor and show that it holds for the numbers.

The principal of structural induction also licenses the definition of functions by structural recursion.  To define a function f with domain N, it suffices to proceed as follows:

1. Give the value of f(0).
2. Give the value of f(m+1) in terms of the value of f(m).

Given this information, there is a unique function f with domain N satisfying these requirements.  Specifically, we may show by induction on n>=0 that the value of f is uniquely determined on all values m<=n.   If n=0, this is obvious since f(0) is defined by clause (1).   If n=m+1, then by induction the value of f is determined for all values k<=m.  But the value of f at n is determined as a function of f(m), and hence is uniquely determined.  Thus f is uniquely determined for all values of n in N, as was to be shown.

The natural numbers, viewed as an inductively-defined type, may be represented in ML using a `datatype` declaration, as follows:

datatype nat = Zero | Succ of nat

The constructors correspond one-for-one with the clauses of the inductive definition.   The extremal clause is implicit in the `datatype` declaration since the given constructors are assumed to be all the ways of building values of type `nat`.   This assumption forms the basis for exhaustiveness checking for clausal function definitions.

(You may object that this definition of the type `nat` amounts to a unary (base 1) representation of natural numbers, an unnatural and space-wasting representation.   This is indeed true; in practice the natural numbers are represented as non-negative machine integers to avoid excessive overhead.  Note, however, that this representation places a fixed upper bound on the size of numbers, whereas the unary representation does not.  Hybrid representations that enjoy the benefits of both are, of course, possible and occasionally used when enormous numbers are required.)

Functions defined by structural recursion are naturally represented by clausal function definitions, as in the following example:

fun double Zero = Zero
| double (Succ n) = Succ (Succ (double n))

fun exp Zero = Succ(Zero)
| exp (Succ n) = double (exp n)

The type checker ensures that we have covered all cases, but it does not ensure that the pattern of structural recursion is strictly followed --- we may accidentally define f(m+1) in terms of itself or some f(k) where k>m, breaking the pattern.  The reason this is admitted is that the ML compiler cannot always follow our reasoning: we may have a clever algorithm in mind that isn't easily expressed by a simple structural induction.  To avoid restricting the programmer, the language assumes the best and allows any form of definition.

Using the principle of structure induction for the natural numbers, we may prove properties of functions defined over the naturals.  For example, we may easily prove by structural induction over the type `nat` that for every n in N, `exp` n evaluates to a positive number.  (In previous chapters we carried out proofs of more interesting program properties.)

Generalizing a bit, we may think of the type `'a list` as inductively defined by the following clauses:

1. `nil` is a value of type `'a list`
2. If h is a value of type 'a, and t is a value of type `'a list`, then h`::`t is a value of type `'a list`.
3. Nothing else is a value of type `'a list`.

This definition licenses the following principle of structural induction over lists.   To prove that a property P holds of all lists l, it suffices to proceed as follows:

1. Show that P holds for `nil`.
2. Show that P holds fpr h`::`t, assuming that P holds for t.

Similarly, we may define functions by structural recursion over lists as follows:

1. Define the function for `nil`.
2. Define the function for h`::`t in terms of its value for t.

The clauses of the inductive definition of lists correspond to the following (built-in) datatype declaration in ML:

datatype 'a list = nil | :: of 'a * 'a list

(We are neglecting the fact that `::` is regarded as an infix operator.)

The principle of structural recursion may be applied to define the reverse function as follows:

fun reverse nil = nil
| reverse (h::t) = reverse t @ [h]

There is one clause for each constructor, and the value of reverse for h`::`t is defined in terms of its value for t.  (We have ignored questions of time and space efficiency to avoid obscuring the induction principle underlying the definition of `reverse`.)

Using the principle of structural induction over lists, we may prove that `reverse` l evaluates to the reversal of l.  First, we show that `reverse` `nil` yields `nil`, as indeed it does and ought to.  Second, we assume that `reverse` t yields the reversal of t, and argue that `reverse` `(`h`::`t`)` yields the reversal of h`::`t, as indeed it does since it returns `reverse` t `@` `[`h`]`.

Generalizing even further, we can introduce new inductively-defined types such as 2-3 trees in which interior nodes are either binary (have two children) or ternary (have three children).  Here's a definition of 2-3 trees in ML:

datatype 'a two_three_tree =
Empty |
Binary of 'a * 'a two_three_tree * 'a two_three_tree |
Ternary of 'a * 'a two_three_tree * 'a two_three_tree * 'a two_three_tree

How might one define the "size" of a value of this type?  Your first thought should be to write down a template like the following:

fun size Empty = ???
| size (Binary (_, t1, t2)) = ???
| size (Ternary (_, t1, t2, t3)) = ???

We have one clause per constructor, and will fill in the ellided expressions to complete the definition.  In many cases (including this one) the function is defined by structural recursion.  Here's the complete definition:

fun size Empty = 0
| size (Binary (_, t1, t2)) = 1 + size t1 + size t2
| size (Ternary (_, t1, t2, t3)) = 1 + size t1 + size t2 + size t3

Obviously this function computes the number of nodes in the tree, as you can readily verify by structural induction over the type `'a two_three_tree`.

Does this pattern apply to every datatype declaration?  Yes and no.   No matter what the form of the declaration it always makes sense to define a function over it by a clausal function definition with one clause per constructor.   Such a definition is guaranteed to be exhaustive (cover all cases), and serves as a valuable guide to structuring your code.  (It is especially valuable if you change the datatype declaration, because then the compiler will inform you of what clauses need to be added or removed from functions defined over that type in order to restore it to a sensible definition.)  The slogan is:

To define functions over a datatype, use a clausal definition with one clause per constructor

The catch is that not every datatype declaration supports a principle of structural induction because it is not always clear what constitutes the predecessor(s) of a constructed value.  For example, the declaration

datatype D = Int of int | Fun of D->D

is problematic because a value of the form `Fun` f is not constructed directly from another value of type `D`, and hence it is not clear what to regard as its predecessor.  In practice this sort of definition comes up only rarely; in most cases datatypes are naturally viewed as inductively defined.

It is interesting to observe that the pattern of structural recursion may be directly codified in ML as a higher-order function.  Specifically, we may associate with each inductively-defined type a higher-order function that takes as arguments values that determine the base case(s) and step case(s) of the definition, and defines a function by structural induction based on these arguments.  An example will illustrate the point.   The pattern of structural induction over the type `nat` may be codified by the following function:

fun nat_recursion base step =
let
fun loop Zero = base
| loop (Succ n) = step (loop n)
in
loop
end

This function has the following type

'a -> ('a -> 'a) -> nat -> 'a

Given the first two arguments, `nat_recursion` yields a function of type ```nat -> 'a``` whose behavior is determined at the base case by the first argument and at the inductive step by the second.  Here's an example of the use of `nat_recursion` to define the exponential function:

val double = nat_recursion Zero (fn result => Succ (Succ result))
val exp = nat_recursion (Succ Zero) double

Note well the pattern!  The arguments to `nat_recursion` are

1. The value for `Zero`.
2. The value for `Succ` n defined in terms of its value for n.

Similarly, the pattern of list recursion may be captured by the following functional:

fun list_recursion base step =
let
fun loop nil = base
| loop (h::t) = step (h, loop t)
in
loop
end

The type of the function `list_recursion` is

'a -> ('b * 'a -> 'a) -> 'b list -> 'a

It may be instantiated to define the `reverse` function as follows:

val reverse = list_recursion nil (fn (h, t) => t @ [h])

Finally, the principle of structural recursion for values of type ```'a two_three_tree``` is given as follows:

fun two_three_recursion base binary_step ternary_step =
let
fun loop Empty = base
| loop (Binary (v, t1, t2)) =
binary_step (v, loop t1, loop t2)
| loop (Ternary (v, t1, t2, t3)) =
ternary_step (v, loop t1, loop t2, loop t3)

Notice that we have two inductive steps, one for each form of node.  The type of `two_three_recursion` is

'a -> ('b * 'a * 'a -> 'a) -> ('b * 'a * 'a * 'a -> 'a) -> 'b two_three_tree -> 'a

We may instantiate it to define the function size as follows:

val size =
two_three_recursion 0
(fn (_, s1, s2)) => 1+s1+s2)
(fn (_, s1, s2, s3)) => 1+s1+s2+s3)

Summarizing, the principle of structural induction over a recursive datatype is naturally codified in ML using pattern matching and higher-order functions.  Whenever you're programming with a datatype, you should use the techniques outlined in this chapter to structure your code.