Chapter 6, Exercise7, BinarySearch
161I would like to see solutions to Exercise 7 at the end of Chapter 6 in the 2007 edition of the Maple 11 Introductory Programming Guide. It's on page 255. The exercise reads as follows:
“Demonstrate that the BinarySearch procedure always terminates.”
“Hint: Suppose the dictionary has n entries. How many words in the dictionary D does BinarySearch look at in the worst case?”
My solution (I’m a Maple novice and I’m reading the book.) is:
View 4937_Chapter6Exercise7.mw on MapleNet or Download 4937_Chapter6Exercise7.mw
View file details
The lengths of most of the test dictionaries are powers of two. The dictionaries are utterly without diversity. The dictionaries are minimizing. Is there a better test set?
The exercise says “demonstrate”. Would a proof solve the problem? Does anyone have a pointer to such a proof? Does such a proof have anything to do with the halting problem?
- William Fish's blog
- Login or register to post comments
- Also try the options scaling, gridrefine and crossingrefine
42 min 42 sec ago - Try implicitplot
1 hour 25 min ago - The patch
3 hours 1 min ago - thx!
3 hours 27 min ago - The source of the bug
3 hours 45 min ago - my concern is ...
4 hours 41 min ago - plotting with the "Standard interface"
5 hours 24 sec ago - variant
5 hours 18 min ago - sorry
here is the
5 hours 33 min ago - Thanks!
6 hours 11 min ago
Comments
Demonstrate
To me (as a mathematician) "demonstrate" means "prove". Moreover "always" means "always", not just "in those cases I tested". When a procedure such as this fails, it's usually not in a typical case, but a very special one that you'd be unlikely to include in your test suite, so it's really good to have a proof. Maple is not much help in this, you have to use your head (I guess automatic theorem-proving software might be used, but that's really overkill here).
Prove Which?
Robert Israel,
Thank you. It's always a pleasure to read what you type.
''To me (as a mathematician) "demonstrate" means "prove". Moreover "always" means "always"...''
You live a hard life [but the difficulties are worth it and so it’s a good life?].
As you typed: “…it’s really good to have a proof.” and “Maple is not much help in this,…” but this is an exercise in an introductory book about Maple...
What should be proved? Although, I can’t find any, there must be many proofs of the binary search. It seems more important to prove that this particular implementation of a binary search always terminates with the correct answer.
“Software testing alone cannot prove that a system does not contain any defects. Neither can it prove that it does have a certain property. Only the process of formal verification can prove that a system does not have a certain defect or does have a certain property. It is impossible to prove or test that a system has "no defect" since it is impossible to formally specify what "no defect" means. All that can be done is prove that a system does not have any of the defects that can be thought of, and has all of the properties that together make it functional and useful.”
http://en.wikipedia.org/wiki/Formal_verification
On the other hand:
“Binary search is one of the trickiest "simple" algorithms to program correctly. A study has shown that an astounding 91.379 percent of professional programmers fail to code a binary search correctly after a whole hour of working on it, and another study shows that accurate code for it is only found in five out of twenty textbooks. (Kruse, 1999) Given this insight, it is important to remember that the best way to verify the correctness of a binary search algorithm is to thoroughly test it on a computer. It is difficult to visually analyze the code without making a mistake.”
http://en.wikipedia.org/wiki/Binary_search
Please provide additional direction.
Prove which?
The question asks you to prove that the BinarySearch procedure as listed in the "Performing a Binary Search" section always terminates, presumably for any inputs that Maple can evaluate. The computation would not terminate if you gave BinarySearch an input whose evaluation would not terminate, e.g.
where
but presumably that doesn't count; it's not BinarySearch that's not terminating, it's the evaluation of its arguments.
It does not ask you to prove that the result is correct.
Termination with an error message (which is possible) counts as termination.
Hint: perform mathematical induction on f - s, which must be a nonnegative integer or the procedure terminates right away.
Correctness
Please examine the following:
View 4937_Chapter6Exercise7b.mw on MapleNet or Download 4937_Chapter6Exercise7b.mw
View file details
Is that way cool or what?
Sorted list needed
BinarySearch works if the list it is given is sorted in lexicographic order. Note that
returns the sorted list, but doesn't sort it in-place
(that only happens for sorting polynomials).
You'd need to say
Oops
I thought that I had found a case that didn't work and I was far too intrigued by that possibility.
I or someone smarter than me could perform mathematical induction on f-s and the Maple procedure could still have a bug in it. Isn’t that something that I should be concerned about?
Correctness
As I said, the exercise doesn't ask you to prove that the result is correct, just that the procedure terminates. That doesn't mean that it isn't possible to prove that the result is correct when the inputs are valid (in particular, in this case, when the list D is sorted in increasing lexicographic order) - it is indeed possible. And yes, I think it is something that you should be "concerned about". Proving a program correct, when that is possible, is a great way to avoid bugs. Unfortunately, it gets very difficult when the program is long and complicated.
Proof
In the following “s” is short for “start”, “m” is short for “middle” and “f” is short for “finish”:
On the first call to BinarySearch f-s is the length of the dictionary less one. On every recursive call to BinarySearch (calls after the first), f-s is less than it was in the previous (higher level) call. This is because
and either the value of s is replaced by m+1 or the value of f is replaced by m-1. Termination is certain because either the dictionary entry is found or f-s becomes zero and BinarySearch ends with the dictionary entry not found.
Is that a proof?
Can you recommend a reference on how to prove stuff?
determine the order
Seems reasonable to me. You might make it more useful by showing the upper bound on the number of iterations. For n items, it should be O(lg(n)).
Proof
It's almost a complete proof; not quite perfect though.
1) It's not necessarily true that "On the first call to BinarySearch f-s is the length of the dictionary less one", although that may be what the programmer intended. This doesn't affect the fact that BinarySearch will terminate.
2) You really should prove that s <= m <= f if s <= f. Actually that's not necessarily true if s and f are negative (but then the program terminates with an error).
3) The search doesn't terminate with entry not found when f-s becomes 0, rather when it becomes -1.
The classic book on how to prove stuff is "How to Solve It" by Polya.
proofs
Imre Lakatos' "Proof and Reasoning" is an entertaining read. Leslie Lamport, the originator of LaTeX, has written a brief PDF, How to Write a Proof, describing his method for writing structured proofs.
Structured Proof
Leslie Lamport says "Since then, I have never believed a result without a careful, structured proof". She seems to be saying that there are a lot of true conjectures that are supported by proofs that contain "serious mistakes". So, a proof such as the one that I wrote is worth very little. If one is going to write a proof they must get serious, learn how to write structured proofs and take the time to do a thorough job.
Is this correct? Is there a computerized (affordable) assistant available to help me?
Proof assistants
There are tons and tons of proof assistants - see for example The seventeen provers of the world (also available online). A word of warning: provers are very hard to use. People are not used to being that formal, and ``usability'' has so far escaped these systems entirely.
Usability of Proof Assistants
Note that "The seventeen provers of the world" shows the proofs but not the process of proving. You need to see a live demonstration to know how the proofs are generated. There may not be a good "Getting Started" guide for some proofs assistants.
I have experienced the pain of using a proof assistant to proof some theories, including a failing attempt of proofing the ones in "The seventeen provers of the world".
Other than getting used to the formality and logic, the learning curve of using proof assistants is pretty steep. The designers of proof assistants have attempted to increase their usability, but not all attempts are successful. Some proof assistants provide more automation than others (e.g. otter?). Beware that automation is a double-edged sword - It can destroy the usability of the proof assistant as well. Some proof assistants provide a "maybe useful" user interface (e.g. Proof General). These interfaces may not be useful for novice users.
I am sure that Jacques can give more insights of using proof assistants. That's all for my two cents.
Lamport
FYI, Dr Lamport is a he, not a she.
Leslie
Oops. Sorry, no offense intended.
A picture is worth a thousand words.
Thanks for the FYI and the link.
http://en.wikipedia.org/wiki/Unisex_name