On formal proofs
August 23rd, 2007Some of you have expressed some concern about whether you need to write “formal proofs” for questions on the homework. The question you raise is an interesting one, and I’ll try to explain why.
It is likely that your only encounter with proof techniques has been the Euclidean geometric construction proofs that you might have done in school, with the two columns, and the QED, etc etc. Euclidean proofs are good examples of how the algorithm design (in this case the geometric construction) goes hand in hand with the proof of correctness, but let’s not get into that right now. As an aside though, you’ll be surprised to know that Euclid often gave incorrect proofs ! This article by Keith Devlin on proofs is worth reading, and in it he describes how Hilbert (one of the more famous mathematicians of this century) observed that Euclid often used axioms that he had not stated, and so his proofs were not technically correct.
In an algorithms class, a proof most often consists of two parts, the first part being a description of the algorithm that claims to solve the desired problem (or a construction that proves the existence of something), and the second part being proofs of correctness and resource usage (as I talked about in Lecture 1). Let’s break down these two parts.
I. The algorithm
Any algorithm you provide must consist of a sequence of unambiguous, simple, mechanically executable steps. What this means is that if I mentally try to run your algorithm (and I will!), I should be able to do so no matter what input I try. You are welcome to make simplifying assumptions, “Without loss of generality let G be a connected graph”, as long as you explain what to do if it’s not (”If G is not connected, we run the algorithm on each component”). Largely speaking, I will not penalize people for ignoring something like connectivity, UNLESS that is key to the whole point of the algorithm. A trivial example: if I ask you to find the connected components of a graph, it is safe to say that you can’t assume the graph is connected (!). In general, if you assume that the input is not the general case, then there should be some easy way of handling the cases not fed to the algorithm, and they must be processed within the overall time bound. Another example: if I ask for something to be done on a set of numbers in linear time (like finding a median), and your first step is to assume the input is sorted, this will not work, because sorting itself takes longer than the desired linear time bound.
It’s overkill (but not by much) to write actual code, with syntax and all. A more appropriate form is a kind of pseudo code with indentation to indicate structures (python code is a good example of what pseudo code might look like). It’s often hard to tell whether your algorithm is well defined, because you have all the steps in your head, so a good way of checking is to mechanically try the algorithm on some input and see whether each step is well defined.
II. Correctness and time bounds.
A proof of correctness is this: a statement of what the algorithm is supposed to produce on a given input (for example, in problem 4, the result is the answer YES/NO depending on whether there is consensus or not), and an argument that the algorithm does this correctly in ALL cases. It will often seem to you that it’s obvious that an algorithm is correct. This can happen, especially with really simple algorithms like mergesort. But more often, you will need to argue that what the algorithm does in fact yields the correct answer.
There are many ways of doing this:
Induction is one approach. Namely, show that it works for all inputs of size n, and then show that if it works for an input of size n, it works for an input of size n+1. This is common with divide and conquer algorithms, and recursive algorithms in general: by assuming that the algorithm works correctly on the smaller input, you can reason about the larger input.
Proof by contradiction is another: assume the algorithm does something incorrectly: this implies some input on which it fails. Now step through the algorithm and show that this cannot be, by deriving a contradiction.
In general though, a proof is a work of art, in that there are no fixed rules. The only rule is that an inference should follow from a prior statement, and the reasoning steps should be simple, and easy to reproduce (just like an algorithm). Ultimately, in the world of algorithms, a proof is that argument that convinces the reader, the reviewer, and the general public. Sometimes, all three of these are wrong: the proof of Fermat’s theorem was discovered to have a hole that took a year or two to fix, and the recent proof of Poincare’s conjecture is still being verified. In algorithms research, it is not uncommon to find bugs in proofs much later on as well.
In your case, the reader, reviewer, and general public, is a skeptical, but reasonable person. Someone who will listen to logic, but will question any step they find doubtful. That is how I evaluate student-written proofs. Often, there’s a clear bug in a proof, and I can find a counter example. In that case, I’ll write it down, and you’ll see the problem. Often, a key reasoning step is missing (in the business, this phenomenon is termed, ‘and a miracle occurred’!). You’ll get points docked for that, but not a lot, unless it’s clear that you didn’t even realize the step was missing (based on other parts of the proof).
No actual proof ever written by actual practising researchers is rigorous enough for a computer to verify, contrary to what the standard definitions of proofs might tell you. I will not hold you to that standard either. However, since taking an algorithms class is really a cover for learning abstract and formal reasoning, I will expect more detail of you than I’d expect from a researcher, because I want you to learn how to think formally.
The best way to learn how to write proofs (as is the best way to learn how to write) is to read lots of proofs, and write them as well. I will do my best to give you examples of good proofs during the lectures, and the textbook contains many more examples.
Questions ?