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:
(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:
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:
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:
nil
is a value of type 'a list
'a list
,
then h::
t is a value of type 'a list
.'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:
nil
.::
t, assuming that P
holds for t.Similarly, we may define functions by structural recursion over lists as follows:
nil
.::
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
Zero
.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.