<< Предыдущая стр. 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

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 стр.)ОГЛАВЛЕНИЕ Следующая >>