Sometimes correctness of programs is further divided into:
partial correctness: meaning that if a program terminates, then its output is correct; and
total correctness: meaning that a program does terminate, and its output is correct.
Total correctness is therefore the conjunction of partial correctness and termination. Thus far, we have been proving partial correctness.
To prove that a program terminates is difficult. Indeed, it is impossible in general for an algorithm to do so: a computer can't precisely decide whether a program will terminate. (Look up the "halting problem" for more details.) But, a smart human sometimes can do so.
There is a simple heuristic that can be used to show that a recursive function terminates:
- All recursive calls are on a "smaller" input, and
- all base cases are terminating.
For example, consider the factorial function:
let rec fact n = if n = 0 then 1 else n * fact (n - 1)
The base case,
1, obviously terminates. The recursive call is on
n - 1,
which is a smaller input than the original
fact always terminates
(as long as its input is a natural number).
The same reasoning applies to all the other functions we've discussed above.
To make this more precise, we need a notion of what it means to be smaller.
Suppose we have a binary relation
< on inputs. Despite the notation, this
relation need not be the less-than relation on integers---although that will
fact. Also suppose that it is never possible to create an infinite
x0 > x1 > x2 > x3 ... of elements using this relation. (Where of
a > b iff
b < a.) That is, there are no infinite descending chains
of elements: once you pick a starting element
x0, there can be only a finite
number of "descents" according to the
< relation before you bottom out and hit
a base case. This property of
< makes it a well-founded relation.
So, a recursive function terminates if all its recursive calls are on
elements that are smaller according to
<. Why? Because there can be only
a finite number of calls before a base case is reached, and base cases must
< relation is well-founded on the natural numbers, because
eventually any chain must reach the base case of 0. But it is not
well-founded on the integers, which can get just keep getting smaller:
-1 > -2 > -3 > ....
Here's an interesting function for which the usual
< relation doesn't suffice
to prove termination:
let rec ack = function | (0, n) -> n + 1 | (m, 0) -> ack (m - 1, 1) | (m, n) -> ack (m - 1, ack (m, n - 1))
This is known as Ackermann's function. It grows faster than any exponential
function. Try running
ack (1, 1),
ack (2, 1),
ack (3, 1), then
1) to get a sense of that. It also is a famous example of a function that can
be implemented with
while loops but not with
for loops. Nonetheless, it
To show that, the base case is easy: when the input is
(0, _), the function
terminates. But in other cases, it makes a recursive call, and we need
to define an appropriate
< relation. It turns out lexicograpic ordering
on pairs works. Define
(a, b) < (c, d) if:
a < c, or
a = cand
b < d.
< order in those two cases is the usual
< on natural numbers.
In the first recursive call,
(m - 1, 1) < (m, 0) by the first case of the
m - 1 < m. In the nested recursive call
ack (m - 1, ack (m, n - 1)), both cases are needed:
(m, n - 1) < (m, n)because
m = mand
n - 1 < n
(m - 1, _) < (m, n)because
m - 1 < m.