Examples of proofs
WaterWorld
Consider a game called WaterWorld, with the following rules:
- You are an explorer in a sea full of pirates.
-
Whenever you enter a location,
you need to declare wehther or not there is a pirate there;
a single mistake will do you in.
Aside:
If you enter pirate turf without gold, you'll be killed, and conversely if you enter an empty location laden with gold, you'll sink. - When you successfully enter an empty location, you can determine how many (of the up to three) neighboring contain pirates, though not necessarily which ones.
- When you successfully enter a pirate location, you get no information, but are allowed to live.
For instance, in this board,
todo:
Type Checking
When writing a program, we'd like to know be sure that
functions are being
called with (at least) the correct type of inputs
(e.g. the function + should be
called with numbers (not booleans),
and a function which a programmer has declared
to return an integer really should always return an integer).
Aside:
int SEEMS_LIKE_FOREVER = 24; // Time enough to procrastinate.
// goSeeMovie?:
// When invited to see a movie, do you accept?
// Depends on how many hours until homework is due,
// and on how much time is needed to do the homework.
//
bool goSeeMovie?( int hrsTilHwDue, int timeNeeded ) {
if (hrsTilHwDue >= SEEMS_LIKE_FOREVER)
true;
else
(hrsTilHwDue >=timeNeeded);
}
// Example:
// goSeeMovie?( 8, 8 ) = false
// goSeeMovie?( 48, 48 ) = true
One reason programmers are required to declare the intended
type of each variable,
is so that the computer (the compiler) can prove that
certain errors won't occur.
How can you prove, in the above,
that goSeeMove? really always returns
a boolean
value as promised? (At least, presuming that it is called
with integers, as indicated. Likewise, you might want
to later prove that whenever it is called,
the provided integers are indeed provided.)
(That is, what work does the compiler's type-checker do?)
int SEEMS_LIKE_FOREVER = 0;
bool goGetRootCanal?( int hrsTilHwDue, int timeNeeded ) {
if (hrsTilHwDue >= SEEMS_LIKE_FOREVER)
true;
else if (hrsTilHwDue > SEEMS_LIKE_FOREVER)
timeNeeded;
else
false;
}
Note that most compilers will not accept
this second example as valid code,
even though is is possible to prove it's safe
(if you know some math axioms about how >=
and > work).
(It certainly deserves to be caught by the compiler as poor code,
just not as code that will generate an error.)
Aside:
todo:
Circuit Verification
Given a circuit's blueprints, will it work as advertised? In 19__, Intel had to recall
todo:
Software and hardware companies are increasingly turning to the use of automated proofs (rather than semi-haphazard testing) to verify (parts of) large products correct. It is a difficult task, which is also an active area of research.
Having proofs of correctness is not just comforting; it allows us to save effort (less time testing, and also able to make better optimizations), and prevent recall of faulty products. But: who decides a proof is correct -- the employee with best SAT scores?!? Is there some trusted way to verify proofs, besides careful inspection by a skilled (yet still error-prone) professional?
How can we tell true proofs from false ones? What are the rules of a proof? (Clearly, this is relevant to writing programs -- at least, bug-free programs.) These are the questions which will occupy us.
"Yeah, well prove it!"
Compare the following proofs:
Example 1
- All people are mortal.
- Socrates is a person.
- Therefore, Socrates is mortal.
Example 2
- All [substitution ciphers] are [vulnerable to brute-force attacks].
- The [Julius Caeser cipher] is a [substitution cipher].
- Therefore, the [Julius Caeser cipher] is [vulnerable to brute-force attacks].
Note that you don't need to know anything about cryptography to know that the conclusion follows from the two premises. (Are the premises indeed true? That's a different question.)
todo:
Example 3
- All griznoxes chorble happily.
- A floober is a type of griznox.
- Therefore, floobers chorble happily.
You don't need to be a world-class floober expert to evaluate this argument, either.
As you've noticed, the form of the argument is the same in all these. If you are assured that the first two premises are true, then w/o any true understanding, you (or a computer) can automatically come up with the conclusion. This classical form happens to be called a "syllogism" (though the name isn't important).
Aside:
todo:
Exercise 1
Mistakes in syllogisms are hard to make: what are the only two ways to have an error in a syllogism?
Solution
-
The argument isn't actually in syllogism form.
To be a syllogism, the conclusion would have to be "any hacker doesn't know my file's password." The file may or may not be secure, but the above doesn't prove it.
- All people don't know my file's password.
Aside:
Equivalent to "Nobody knows my file's password". Why did we phrase this sentence awkwardly? Because a syllogism requires the first premise to be of the form "All somethings have some property". - Any hacker is a person.
- Therefore, my file is secure from hackers.
Warning:
Not the correct conclusion for a syllogism.
- All people don't know my file's password.
-
One of the two premises is wrong.
This proof fails of course, if some hackers are non-people (e.g. programs), or if some people know the password. (In fact, presumably you know the password!)
- All people don't know my file's password.
Warning:
Is this really true? - Any hacker is a person.
Warning:
Is this really true? - Therefore, any hacker doesn't know my file's password.
Of course, just because the argument fails, the conclusion might be true for other reasons. (That is, an incorrect argument doesn't prove the conclusion's opposite!)todo:
add link: Example from The Cuckoo's Egg Male singer croons "Everybody loves my baby; My baby don't love [anybody] but me." Conclusion: the speaker is his own baby, and is narcissistic. (Or, the singer is wrong in his assumptions.) - All people don't know my file's password.
Other rules of inference
Of course, there are more ways to deduce things, beyond a syllogism; Who decides what the valid rules of inference are? Is it always clear when people have used the rules correctly?
|
|
Consider the following argument:
- (A) is next to one pirate; and
- (A) has only one explored neighbor;
- Conclusion: If you are a square next to (A), then you contain a pirate
The problem is that the author of the argument presumably meant to conclude "all explored neighbors of (A) contain a pirate". Really, the underlying problem for this mistaken reasoning is These problems both arise, of course, because we were sloppy about what each sentence meant exactly. We used informal English -- a fine language for humans, who can cope with remarkable amounts of ambiguity -- but not a good language for specifying arguments.
Aside:
One reaction to the above arguments is "Well, big deal -- somebody made a mistake (mis-interpreting or mis-stating a claim); that's their problem. (And sheesh, they sure are dolts!)" But as a programmer, that's not true: Writing any large system, human programmers will err, no matter how smart or careful they are. Thus we are looking for systematic ways to prove code correct or incorrect.
