Consider the simple problem of summing the numbers from one to n. If we know the following equation then we can implement the function easily using only our existing knowledge of Standard ML.
The function is simply fn n => (n * (n+1)) div 2. We will call this function sum. But what if we had not known the above equation? We would require an algorithmic rather than a formulaic solution to the problem. We would have been forced to break down the calculation of the sum of the numbers from one to n into a number of smaller calculations and devise some strategy for recombining the answers. We would immediately use the associative property of addition for this purpose.
We now have a trivial case--when n is one--and a method for decomposing larger cases into smaller ones. These are the essential ingredients for a recursive function.
| sum' (n) = |
|
(1) |
In our implementation of this definition we must mark our function declaration as being recursive in character using the Standard ML keyword rec. The only values which can be defined recursively in Standard ML are functions.
val rec sum' = fn 1 => 1
| n => n + sum' (n - 1);
If you have not seen functions defined in this way before then it may seem somewhat worrying that the sum' function is being defined in terms of itself but there is no trickery here. The equation n = 5n - 20 defines the value of the natural number n precisely through reference to itself and the definition of the sum' function is as meaningful.
We would assert for positive numbers that sum and sum' will always agree but at present this is only a claim. Fortunately, the ability to encode recursive definitions of functions comes complete with its own proof method for checking such claims. The method of proof is called induction and the form of induction which we are using here is simple integer induction.
The intent behind employing induction here is to construct a convincing argument that the functions sum and sum' will always agree for positive numbers. The approach most widely in use in programming practice to investigate such a correspondence is to choose a set of numbers to use as test data and compare the results of applying the functions to the numbers in this set. This testing procedure may uncover errors if we have been fortunate enough to choose one of the positive integers--if there are any--for which sum and sum' disagree. One of the advantages of testing programs in this way is that the procedure is straightforwardly amenable to automation. After some initial investment of effort, different versions of the program may be executed with the same input and the results compared mechanically. However, in this problem we have very little information about which might be the likely values to uncover differences. Sadly, this is often the case when attempting to check the fitness of a computer program for a given purpose.
Rather than simply stepping through a selection of test cases, a proof by induction constructs a general argument. We will show that the equivalence between sum and sum' holds for the smallest allowable value--one in this case--and then show that if the equivalence holds for n it must also hold for n+1. The first step in proving any result, even one as simple as this, is to state the result clearly. So we will now do that.
Proposition
For every positive n, we have that 1 + 2 + ... + n = n(n + 1)/2.
The proof of this proposition is quite short.