Sample Code for This Chapter

This chapter is concerned with the close relationship between recursionand 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:

  1. 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.
  2. 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 2n for integers n>=0.  We seek to define the function

exp : int -> int

satisfying the specification

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

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 2n.  The caller is required to establish the precondition before applying exp; in exchange, the caller may assume that the result is 2n.

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, 20.   Otherwise, assume that exp is correct for n-1>=0, and consider the value of exp n.  From the second line of its definition we can see that this is the value of 2*p, where p is the value of exp (n-1).  Inductively, p=2n-1, so 2*p = 2*2n-1 = 2n, as desired.  Notice that we need not consider arguments n<0 since the precondition of the specification requires that this be so.  We must, however, ensure that each recursive call satisfies this requirement in order to apply the inductive hypothesis.

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  2(n div 2)*2(n div 2) = 22*(n div 2) = 2n, as required.  If, on the other hand, n is odd, the value is the result of doubling exp (n-1).  Inductively the latter value is 2(n-1), so doubling it yields 2n, as required.

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 2n*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 iterative_fast_exp.   This yields the desired result, but what is the running time?  Here's a recurrence to describe its running time as a function of n:

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) = (22)n = 4n.

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 bn*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 = bn*a, and if n is odd, we obtain inductively the result b(n-1)*b*a=bn*a.   This completes the proof.

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 mor 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)n2 < mn, so that by induction we return the g.c.d. of m mod n and n.  It remains to show that this is the g.c.d. of m and n.   If d divides both m mod n and n, then kd = (m mod n) = (m - (m div n)n) and ld = n for some non-negative k and l.   Consequently, kd = m - (m div n)ld, so m = (k+(m div n)l)d, which is to say that d divides m.  Now if d' is any other divisor of m and n, then it is also a divisor of (m mod n) and n, so d>d'.  That is, d is the g.c.d. of m and n.   The other case, m<=n, follows similarly.  This completes the proof.

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 mand 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 mand 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 aand 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 mand 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.

Sample Code for This Chapter