JUNE 6, 2001

Reading material

If you use the first edition of the textbook, follow the reading material in orange. If you use the second edition, follow the reading material in brown.

(1st) pages 40-41 (Section 2.4.3), pages 134-136 (Section 4.4), pages 162-163 (Section 5.3.1)

(2nd) pages 108-109 (Section 3.4.3), pages 211-214 (Section 5.4), pages 249-250 (Section 6.3.3)

Additional material

Loop invariants

Pre- and postconditions are predicates. Both tell us something about the values of the variables of our programs. For example, `n = 1' and `list is nonempty' are such predicates. We use
     { P } S { Q }
to specify that
     if the variables have values such that the predicate P is satisfied at the start of the execution of statement S
     and the execution of the statement S terminates
     then at termination the variables have values such that the predicate Q is satisfied.
For example,
     { n = 0 } n = n + 1; { n = 1 }
and
     { true } list.insertLast("x"); { list is nonempty }

A loop invariant is also a predicate. It tells us something about the values of the variables while executing a loop. This predicate should be satisfied at the beginning of every iteration of the loop. Consider the loop
     while B do S
with loop invariant LI. If
     { LI B } S { LI },
that is, statement S preserves the loop invariant LI within the loop, then we can conclude that
     { LI } while B do S { LI B },
that is, if the loop invariant LI is satisfied at the start of the execution of the loop and the loop terminates then the loop invariant LI (and of course also B) is satisfied at termination.

Bubble-sort

Algorithm bubbleSort(sequence):
   Input: sequence of integers sequence
   Postcondition: sequence is sorted and contains the same integers as the original sequence
length length of sequence
for i 0 to length - 1 do
     for j 0 to length - i - 2 do
         if jth element of sequence > (j+1)th element of sequence then
             swap jth and (j+1)th element of sequence

A loop invariant for the outer loop is: the last i elements of sequence are sorted and are all greater than or equal to the other elements of sequence. A loop invariant for the inner loop is: the last i elements of sequence are sorted and are all greater than or equal to the other elements of sequence and the jth element of sequence is greater than or equal to the first j elements of sequence.

Proof of Proposition 5.9 and 5.10/ Proposition 6.10 and 6.11 in PostScript and PDF.

Variant function

Before we can reason inductively about recursive algorithms, we need to prove that the algorithm terminates. To show that there is no infinite recursion without tracing through the actual computation, we introduce a variant function. This function maps each instance of the parameters satisfying the precondition to a natural number. That is, it is a function from instances to natural numbers. Consider for example

Algorithm factorial(n):
   Input: integer
   Output: n!
   Precondition: n > 0
if n = 1 then
     return 1
else
     return n * factorial(n - 1)

The variant function variant has to map each instance of the parameters satisfying the precondition, in this example a positive integer, to a natural number. This natural number can be thought of as an upperbound of the number of recursive calls this instance gives rise to. For example, factorial(n) gives rise to n - 1 recursive calls.

To prove that a recursive algorithm does not lead to infinite recursion, it is enough to find a variant function variant with the following two properties:

variant maps instances of the base case(s) to 0.
variant maps (the instances of) recursive calls to a smaller number than (the instance of) original call.

For example, for factorial the above properties amount to:

variant(1) = 0.
variant(n - 1) < variant(n).

The function variant(n) = n - 1 satisfies the above two properties. Note that the variant function is not unique. For example, the variant function defined by variant(n) = 2n - 2 also satisfies the above properties.

Let us have a look at another example. Consider the following algorithm.

Algorithm numberOfNodes(node):
   Input: node of a binary tree
   Output: number of nodes of the subtree rooted at node
if node is a leaf then
     return 1
else
     return numberOfNodes(left child of node) + numberOfNodes(right child of node) + 1

In this example, the instances of the parameters are nodes of a binary tree. The variant function variant has to satisfy

variant(node) = 0 if node is a leaf and
variant(left child of node) < variant(node) and variant(right child of node) < variant(node) if node is not a leaf.

Consider the function variant(node) = number of internal nodes of the subtree rooted at node. One can easily check that it satisfies the above properties, and hence prove that the recursive algorithm eventually terminates.

Now consider the following algorithm.

Algorithm f(n):
   Input: integer
   Output: 1
   Precondition: n > 0
if n = 1 then
     return 1
else
     return f(n + 1)

Again the instances are positive integers. In this case, the variant function variant should satisfy

variant(1) = 0.
variant(n + 1) < variant(n).

We cannot find such a function. This is not surprising. The algorithm does not terminate for any integer greater than 1.

Question

Give a variant function for
Algorithm height(node):
   Input: node of a binary tree
   Output: height of node (length of the longest path from node to an external node)
if node is a leaf then
     return 0
else
     return 1 + max { height(left child of node), height(right child of node) }