This chapter is concerned with the close relationship between *recursion*and *induction*
in programming. When defining a recursive function, be sure to write down a clear,
concise *specification* of its behavior, then mentally (or on paper) give an *inductive*
*proof* that your code satisfies the specification. What is a specification?
It includes (at least) these ingredients:

- Assumptions about the types and values of the arguments to the function. For example, an integer argument might be assumed to have a non-negative value.
- Guarantees about the result value, expressed in terms of the argument values, under the assumptions governing the arguments.

What does it mean to prove that your program satisfies the specification? It
means to give a rigorous argument that if the arguments satisfy the assumptions on the
input, then the program will terminate with a value satisfying the guarantees stated in
the specification. In the case of a recursively-defined function the argument
invariably has the form of a inductive proof based on an *induction principle* such
as mathematical induction for the natural numbers or, more generally, structural induction
for other recursively-defined types. The rule of thumb is this

*when programming recursively, think inductively*

If you keep this rule firmly in mind, you'll find that you are able to get your code right more often without having to resort to the tedium of step-by-step debugging on test data.

Let's start with a very simple series of examples, all involving the computation of the
integer exponential function. Our first example is to compute *2 ^{n} *for
integers

exp : int -> int

satisfying the specification

if n>=0, then exp n evaluates to 2^{n}.

The *precondition*, or *assumption*, is that the argument *n* is
non-negative. The *postcondition*, or *guarantee*, is that the result
of applying *exp* to *n* is the number *2 ^{n}*. The
caller is required to establish the precondition before applying

Here's the code:

fun exp 0 = 1

| exp n = 2 * exp (n-1)

Does this function satisfy the specification? It does, and we can prove this by
induction on *n*. If *n=0*, then *exp n* evaluates to *1*
(as you can see from the first line of its definition), which is, of course, *2 ^{0}*.
Otherwise, assume that

That was pretty simple. Now let us consider the running time of *exp*
expressed as a function of *n*. Assuming that arithmetic operations are
executed in constant time (they are), then we can read off a recurrence describing its
execution time as follows:

T(0) = O(1)

T(n+1) = O(1)+ T(n)

In fact this recurrence could itself be thought of as defining a function in ML simply
by rewriting it into ML syntax! However, in most cases we are interested in *solving*
a recurrence by finding a closed-form expression for it. In this case the solution
is easily obtained:

T(n) = O(n)

Thus we have a *linear time* algorithm for computing the integer exponential
function.

What about space? This is a much more subtle issue than time because it is much
more difficult in a high-level language such as ML to see where the space is used.
Based on our earlier discussions of recursion and iteration we can argue informally that
the definition of *exp* given above requires space given by the following
recurrence:

S(0) = O(1)

S(n+1) = O(1) + S(n)

The justification is that the implementation requires a constant amount of storage to record the pending multiplication that must be performed upon completion of the recursive call.

Solving this simple recurrence yields the equation

S(n) = O(n)

expressing that *exp* is also a *linear space* algorithm for the integer
exponential function.

Can we do better? Yes, on both counts! Here's how. Rather than count
down by one's, multiplying by two at each stage, we use successive squaring to achieve
logarithmic time and space requirements. The idea is that if the exponent is even,
we square the result of raising *2* to half the given power; otherwise, we reduce
the exponent by one and double the result, ensuring that the next exponent will be even.
Here's the code:

fun square (n:int) = n*n

fun double (n:int) = n+n

fun fast_exp 0 = 1

| fast_exp n =

if n mod 2 = 0 then

square (fast_exp (n div 2))

else

double (fast_exp (n-1))

Its specification is precisely the same as before. Does this code satisfy the
specification? Yes, and we can prove this by using *complete induction*, a
form of mathematical induction in which we may prove that *n>0* has a desired
property by assuming not only that the predecessor has it, but that *all preceding
numbers* have it, and arguing that therefore *n* must have it. Here's how
it's done. For *n=0* the argument is exactly as before. Suppose, then,
that *n>0*. If *n *is even, the value of *exp n* is the
result of squaring the value of *exp (n div 2)*. Inductively this value is *2 ^{(n
div 2)}*, so squaring it yields

Here's a recurrence governing the running time of *fast_exp* as a function of
its argument:

T(0) = O(1)

T(2n) = O(1) + T(n)

T(2n+1) = O(1) + T(2n) = O(1) + T(n)

Solving this recurrence using standard techniques yields the solution

T(n) = O(lg n)

You should convince yourself that *fast_exp* also requires logarithmic space
usage.

Can we do better? Well, it's not possible to improve the time requirement (at
least not asymptotically), but we can reduce the space required to *O(1)* by
putting the function into iterative (tail recursive) form. However, this may not be
achieved in this case by simply adding an accumulator argument, without also increasing
the running time! The obvious approach is to attempt to satisfy the specification

if n>=0, then iterative_fast_exp (n, a) evaluates to 2^{n}*a

Here's some code that achieves this specification:

fun iterative_fast_exp (0, a) = a

| iterative_fast_exp (n, a) =

if n mod 2 = 0 then

iterative_fast_exp (n div 2, iterative_fast_exp (n div 2, a))

else

iterative_fast_exp (n-1, 2*a)

It is easy to see that this code works properly for *n=0* and for *n>0*
when *n* is odd, but what if *n>0* is even? Then by induction we
compute *2 ^{(n div 2)}*2^{(n div 2})*a* by two recursive calls to

T(0) = 1

T(2n) = O(1) + 2T(n)

T(2n+1) = O(1) + T(2n) = O(1) + 2T(n)

Here again we have a standard recurrence whose solution is

T(n) = O(n lg n)

Yuck! Can we do better? The key is to recall the following important fact:

2.^{(2n)}= (2^{2})^{n}= 4^{n}

We can achieve a logarithmic time and exponential space bound by a *change of base*.
Here's the specification:

if n>=0, then generalized_iterative_fast_exp (b, n, a) evaluates to b^{n}*a

Here's the code:

fun generalized_iterative_fast_exp (b, 0, a) = a

| generalized_iterative_fast_exp (b, n, a) =

if n mod 2 = 0 then

generalized_iterative_fast_exp (b*b, n div 2, a)

else

generalized_iterative_fast_exp (b, n-1, b*a)

Let's check its correctness by complete induction on *n*. The base case is
obvious. Assume the specification for arguments smaller than *n>0*.
If *n* is even, then by induction the result is *(b*b) ^{(n div 2)}*a = b^{n}*a*,
and if

The trick to achieving an efficient implementation of the exponential function was to
compute a more general function that can be implemented using less time and space.
Since this is a trick employed by the implementor of the exponential
function, it is important to insulate the client from it. This is easily achieved by
using a `local`

declaration to "hide" the generalized function,
making available to the caller a function satisfying the original specification.
Here's what the code looks like in this case:

local

fun generalized_iterative_fast_exp (b, 0, a) =

| generalized_iterative_fast_exp (b, n, a) =... as above ...in

fun exp n = generalized_iterative_fast_exp (2, n, 1)

end

The point here is to see how induction and recursion go hand-in-hand, and how we used induction not only to verify programs after-the-fact, but, more importantly, to help discover the program in the first place. If the verification is performed simultaneously with the coding, it is far more likely that the proof will go through and the program will work the first time you run it.

It is important to notice the correspondence between strengthening the specification by
adding additional assumptions (and guarantees) and adding accumulator arguments.
What we observe is the apparent paradox that it is often *easier* to do something
(superficially) *harder*! In terms of proving, it is often easier to push
through an inductive argument for a stronger specification, precisely because we get to
assume the result as the inductive hypothesis when arguing the inductive step(s).
We are limited only by the requirement that the specification be proved outright at the
base case(s); no inductive assumption is available to help us along here. In terms
of programming, it is often easier to compute a more complicated function involving
accumulator arguments, precisely because we get to exploit the accumulator when making
recursive calls. We are limited only by the requirement that the result be defined
outright for the base case(s); no recursive calls are available to help us along here.

Let's consider a more complicated example, the computation of the greatest common
divisor of a pair of non-negative integers. Recall that *m is a divisor of n,
m|n, *iff *n* is a multiple of *m*, which is to say that there is some *k>=0*
such that *n=km*. The *greatest common divisor *of non-negative
integers *m* and *n* is the largest *p* such that *p|m* and *p|n*.
(By convention the g.c.d. of 0 and 0 is taken to be 0.) Here's the
specification of the *gcd *function:

if m,n>=0, then gcd(m,n) evaluates to the g.c.d. of m and n

Euclid's algorithm for computing the g.c.d. of *m* and* n* is defined by
complete induction on the product *mn*. Here's the algorithm:

fun gcd (m:int, 0):int = m

| gcd (0, n:int):int = n

| gcd (m:int, n:int):int =

if m>n then gcd (m mod n, n) else gcd (m, n mod m)

Why is this algorithm correct? We may prove that *gcd* satisfies the
specification by complete induction on the product *mn*. If *mn* is
zero, then either *m*or *n* is zero, in which case the answer is, correctly,
the other number. Otherwise the product is positive, and we proceed according to
whether *m>n* or *m<=n*. Suppose that *m>n*.
Observe that *m mod n = m - (m div n)n, *so that* (m mod n)n = mn - (m div n)n ^{2}
< mn*, so that by induction we return the g.c.d. of

At this point you may well be thinking that all this inductive reasoning is surely
helpful, but it's no replacement for good old-fashioned "bulletproofing" ---
conditional tests inserted at critical junctures to ensure that key invariants do indeed
hold at execution time. Sure, you may be thinking, these checks have a run-time
cost, but they can be turned off once the code is in production, and anyway the cost is
minimal compared to, say, the time required to read and write from disk. It's hard
to complain about this attitude, provided that sufficiently cheap checks *can* be
put into place and provided that you know *where* to put them to maximize their
effectiveness. For example, there's no use checking *i>0* at the start of
the *then* clause of a test for *i>0*. Barring compiler bugs, it
can't possibly be anything other than the case at that point in the program. Or it
may be possible to insert a check whose computation is more expensive (or more
complicated) than the one we're trying to perform, in which case we're defeating the
purpose by including them!

This raises the question of where should we put such checks, and what checks should be
included to help ensure the correct operation (or, at least, graceful malfunction) of our
programs? This is an instance of the general problem of writing *self-checking
programs*. We'll illustrate the idea by elaborating on the g.c.d. example a bit
further. Suppose we wish to write a self-checking g.c.d. algorithm that computes the
g.c.d., and then checks the result to ensure that it really is the greatest common divisor
of the two given non-negative integers before returning it as result. The code might
look something like this:

exception GCD_ERROR

fun checked_gcd (m, n) =

let

val d = gcd (m, n)

in

if d mod m = 0 andalso d mod n = 0 andalso???then

d

else

raise GCD_ERROR

end

It's obviously no problem to check that putative g.c.d., *d*, is in fact a
common divisor of *m*and *n*, but how do we check that it's the *greatest*
common divisor? Well, one choice is to simply try all numbers between *d* and
the smaller of *m* and *n* to ensure that no intervening number is also a
divisor, refuting the maximality of *d*. But this is clearly so inefficient
as to be impractical. But there's a better way, which, it has to be emphasized,
relies on the kind of mathematical reasoning we've been considering right along.
Here's an important fact:

*d is the g.c.d. of m and n iff d divides m and n and can be written
as a linear combination of m and n*.

That is, *d* is the g.c.d. of *m*and *n* iff *m=kd* for
some *k*>=0, *n=ld* for some *l*>=0, and *d=am+bn* for
some integers (possibly negative!) *a* and *b*. We'll prove this
constructively by giving a program to compute not only the g.c.d.* d* of* m*
and *n*, but also the coefficients *a*and *b* such that *d=am+bn*.
Here's the specification:

if m,n>=0, then ggcd (m, n) evaluates to (d, a, b) such that d divides m, d divides n, and d=am+bn; consequently, d is the g.c.d. of m and n.

And here's the code to compute it:

fun ggcd (0, n) = (n, 0, 1)

| ggcd (m, 0) = (m, 1, 0)

| ggcd (m, n) =

if m>n then

let

val (d, a, b) = ggcd (m mod n, n)

in

(d, a, b - a*(m div n))

end

else

let

val (d, a, b) = ggcd (m, n mod m)

in

(d, a - b*(n div m), b)

end

We may easily check that this code satisfies the specification by induction on the
product *mn*. If *mn=0*, then either *m* or *n* is 0, in
which case the result follows immediately. Otherwise assume the result for smaller
products, and show it for *mn>0*. Suppose *m>n*; the other case
is handled analogously. Inductively we obtain *d*, *a*, and *b*
such that *d* is the g.c.d. of *m mod n* and *n*, and hence is the
g.c.d. of *m*and *n*, and *d=a(m mod n) + bn*. Since *m mod
n = m - (m div n)n*, it follows that *d = am + (b-a(m div n))n*, from which the
result follows.

Now we can write a self-checking g.c.d. as follows:

exception GCD_ERROR

fun checked_gcd (m, n) =

let

val (d, a, b) = ggcd (m, n)

in

if m mod d = 0 andalso n mod d = 0 andalso d = a*m+b*n then

d

else

raise GCD_ERROR

end

This algorithm takes no more time (asymptotically) than the original, and, moreover, ensures that the result is correct. This illustrates the power of the interplay between mathematical reasoning methods such as induction and number theory and programming methods such as bulletproofing to achieve robust, reliable, and, what is more important, elegant programs.