<<

. 84
( 107 .)



>>

than zero, repeat the following two steps: add count to sum, and
then decrease count by 1. The desired result is the value of sum.
We need to explain how the one new construct works, though by now you
should be able to guess the meaning of “subtractive assignment.”



Chapter 16
Proving programs correct / 463



—¦ Subtractive assignment. An example is the statement, count ’= 1. After
executing such a statement the value of the program variable on the left
is one less than it was before the execution of the statement.
The ¬rst thing we need to prove is that for any natural number n, the proving correctness
of sumDownFrom
program terminates after executing exactly n passes through the loop. This
induction is similar (but easier) than the corresponding proof for sumUpTo,
since it involves a direct induction on the value of count. We leave the proof
as Exercise 16.27.
Now let™s prove that when the program terminates, the value in the vari-
able sum is the sum of the ¬rst n natural numbers, as desired. This will again
require a proof by induction. We will prove that for any k ¤ n, after k itera-
tions of the while loop, the values of the variables sum and count satisfy the
following equation:
(0 + 1 + 2 + . . . + count) + sum = 0 + 1 + 2 + . . . + n
This invariant is a lot more interesting than the one given for sumUpTo. The
new program again accumulates the desired result in the program variable
sum, but the sum is accumulated “downward,” initially n and then adding
n ’ 1, n ’ 2, and so on down to 0, where it stops. The loop invariant re¬‚ects
this by saying that at any time you have to add the missing initial segment
(0 + . . . + count) to the value of sum to get the desired result. But this initial
segment gets shorter and shorter, until ¬nally count = 0 and the program
terminates.
Proof: Basis: After 0 iterations of the while loop, count = n and
sum = 0, and so the equation becomes
(0 + 1 + 2 + . . . + n) + 0 = 0 + 1 + 2 + . . . + n
which is obviously true.
Induction: We assume that the equation holds after k iterations of
the body of the loop, and must show that it holds again after k + 1
iterations of the loop. Let sum be the value of sum after k iterations
of the loop, and sum be the value of sum after k + 1 iterations.
Similarly for count.
Then our inductive hypothesis can be expressed as
(0 + 1 + 2 + . . . + count) + sum = 0 + 1 + 2 + . . . + n
We need to show that this holds for sum and count . After k + 1
iterations, the value of sum is increased by count, and the value of
count is decreased by 1, and so we have



Section 16.5
464 / Mathematical Induction


0 + 1 + . . . + count + sum = 0 + 1 + . . . + (count ’ 1) + (sum + count)
= 0 + 1 + . . . + (count ’ 1) + count + sum
= (0 + 1 + . . . + count) + sum
= 0 + 1+ ...+ n

This concludes our induction.

Finally, we know that when the test condition on the loop becomes false,
count must equal 0, and so at this point 0 + . . . + count + sum = 0 +
sum = 0 + 1 + . . . + n. So after n iterations, the program terminates with
sumDownFrom(n) = 0 + 1 + . . . + n.
These proofs may seem to make heavy going of what are fairly straightfor-
ward facts about the example programs we™ve looked at. True enough. But for
more complicated programs, the kind that actually arise in sophisticated ap-
plications, many such recursive and looping constructions are used, and their
properties can be far from obvious. (This is why software fails so often!) Pro-
grammers must be able to think through such inductive proofs easily, whether
they write them down or not, in order to make sure their programs do indeed
do what they intend.

Exercises


16.27 Prove that when given any natural number n as input, the program sumDownFrom terminates
 after exactly n iterations of the while loop.

16.28 Give a proof that the following function computes n!, i.e., the factorial of its argument n. (0!
 is de¬ned to be 1, while for any other natural number n, n! = 1 — 2 — . . . — n.)
public natural fact(natural n) {
natural f = 1;
natural count = n;
while(count > 0) {
f—= count;
count ’= 1;
}
return f;
}

The construct f —= count multiplies the value of f by count.




Chapter 16
Proving programs correct / 465



16.29 In the real Java programming language, there is no way to stipulate that a program variable
 must contain a natural number. The best that can be done is to specify that the variable must
contain an integer, that is, the value may be positive or negative.
The program below is the same as the sumUpTo example above, except that it uses the
Java keyword “int” to specify the type of the program variables n, count and sum.
Write a speci¬cation for this program, and prove that the program implements the speci-
¬cation. [Hint: it is easiest to decide what the program does when passed a negative number,
and then write the speci¬cation to say that that is what the program should do. Then do the
proof.]
public int sumTo(int n) {
int sum = 0;
int count = 0;
while(count < n) {
count += 1;
sum += count;
}
return sum;
}

16.30 All programming languages have limits on the size of the values that integer typed variables
 have. This complicates the job of proving that a real program meets its speci¬cation. The
largest integer available in Java is 232 ’ 1. How would this impact the proof of correctness of
the ¬rst program in this section?

16.31 In this chapter we have not presented a real theory of inductive de¬nitions. Rather, we have
 given several examples of inductive de¬nitions, and shown how they are related to proofs
by induction. This is all that most students need. There is, however, an extensive theory of
inductive de¬nitions. In this problem we sketch the start of this theory. The reader interested
in pursuing it further should consult Aczel™s chapter on inductive de¬nitions in The Handbook
of Mathematical Logic.
Let D be some set. By a monotone operator on D we mean a function “ which assigns to
each X ⊆ D a subset “(X) ⊆ D satisfying the following “monotonicity” condition:

∀X ∀Y [X ⊆ Y ’ “(X) ⊆ “(Y )]

We can think of any of our inductive de¬nitions as given by such a monotone op-
erator, and we can think of any such monotone operator as giving us an inductive
de¬nition. The ¬rst four parts of this problem give examples of monotone operators,
the remainder explores the relation between such operators and inductive de¬nitions.




Section 16.5
466 / Mathematical Induction



1. Let D be the set of real numbers and let “(X ) =

X ∪ {x + 1 | x = 0 ∨ x ∈ X}

Show that “ is a monotone operator. Show that “(N) = N, where N is the set of natural
numbers. Show that if “(X) = X then N ⊆ X.

2. Let D be the set of strings made up from the connectives and the propositional letters
used in the de¬nition of the ambig-w¬s. Let “(X) be the set of all propositional letters,
together with anything obtained by one application of the connectives to something
in X. Thus, if A1 A1 ∈ X then the following would all be members of “(X ): ¬A1 A1,
A1 A1 § A1 A1 , and so forth. Show that “ is a monotone operator. Show that if S is the
set of ambig-w¬s, then “(S) = S.

3. Suppose that f is an n-ary function from some set D into D. Let “f (X) =

X ∪ {f (d1 , . . . , dn ) | d1 , . . . , dn ∈ X}

Show that “ is a monotone operator.

4. Let “1 and “2 be monotone operators. De¬ne a new operator by

“(X) = “1 (X) ∪ “2(X)

Show that “ is also monotone.

5. Now let “ be any monotone operator on a set D.

(a) Show that “(“(D)) ⊆ “(D)
(b) Call a subset X of D “-closed if “(X) ⊆ X. By the preceding, we know that there
is at least one “-closed set. (What is it?) Let I be the intersection of all “-closed
sets. Prove that I is “-closed. This set I is thus the smallest “-closed set. It is said
to be the set inductively de¬ned by the monotone operator “.
(c) What is the set inductively de¬ned by the operators in each of 1 and 2?
(d) Let I be the set inductively de¬ned by “. Prove that “(I) = I.

6. Let I0 = …, I1 = “(I0 ), I2 = “(I1 ), . . . , In+1 = “(In ), for any natural number n. These
sets are called the “¬nite iterates” of “. Show (by induction!) that for each n, In ⊆ I,
where I is the set inductively de¬ned by “.




Chapter 16
Proving programs correct / 467



7. In many cases, the set inductively de¬ned by “ is just the union of all these ¬nite iterates.
This is the case with all of the inductive de¬nitions we have given in this book. Why? To
answer this, prove that if “ is “¬nitely based” (in a sense to be de¬ned in a moment), then
the set inductively de¬ned by “ is the union of its ¬nite iterates. Now for the de¬nition.
An operator “ is said to be ¬nitely based provided

∀X ∀x [x ∈ “(X) ’ ∃Y ⊆ X(Y ¬nite § x ∈ “(Y ))]

8. When a monotone operator is not ¬nitely based, one typically has to keep iterating “
“into the trans¬nite” if you want to build up the set from below. Trying to make sense of
these trans¬nite inductions was Cantor™s original motivation for developing his theory of
sets. We have not developed enough set theory to go into this here. But you might like to
try to come up with an example of this phenomenon. You will, of course, need to think
of an operator that is not ¬nitely based.




Section 16.5
Chapter 17

Advanced Topics in
Propositional Logic

This chapter contains some more advanced ideas and results from proposi-
tional logic, logic without quanti¬ers. The most important part of the chapter
is the proof of the Completeness Theorem for the propositional proof system
FT that you learned in Part I. This result was discussed in Section 8.3 and
will be used in the ¬nal chapter when we prove the Completeness Theorem
for the full system F. The ¬nal two sections of this chapter treat topics in
propositional logic of considerable importance in computer science.


Section 17.1
Truth assignments and truth tables

In Part I, we kept our discussion of truth tables pretty informal. For example,
we did not give a precise de¬nition of truth tables. For some purposes this
modeling truth tables
informality su¬ces, but if we are going to prove any theorems about fol,
such as the Completeness Theorem for the system FT , this notion needs to
be modeled in a mathematically precise way. As promised, we use set theory
to do this modeling.
We can abstract away from the particulars of truth tables and capture
what is essential to the notion as follows. Let us de¬ne a truth assignment for
truth assignments
a ¬rst-order language to be any function h from the set of all atomic sentences
of that language into the set {true, false}. That is, for each atomic sentence
A of the language, h gives us a truth value, written h(A), either true or false.
Intuitively, we can think of each such function h as representing one row of
the reference columns of a large truth table.
Given a truth assignment h, we can de¬ne what it means for h to make an
modeling semantics
arbitrary sentence of the language true or false. There are many equivalent
ˆ
ways to do this. One natural way is to extend h to a function h de¬ned on
the set of all sentences and taking values in the set {true, false}. Thus if
we think of h as giving us a row of the reference column, then ˆ ¬lls in the
h
values of the truth tables for all sentences of the language, that is, the values
corresponding to h™s row. The de¬nition of ˆ is what you would expect, given
h



468
Truth assignments and truth tables / 469



<<

. 84
( 107 .)



>>