18
$\begingroup$

In teaching Intro. Algorithms to undergrads, one of the most difficult tasks is to motivate why they need to know how to prove things about algorithms. (For many students, at least in many US universities, they may see some basic proofs in Discrete Mathematics, but Algorithms is often the first time they have to use proofs to reason about algorithms.) While I think I can do a decent job motivating this at an abstract level, concrete examples are much more convincing, hence my question:

I'm looking for concrete examples that show the value of proofs in algorithms.

A couple questions already address this, and if you have answers to those, please add them there:

However, I think there are other ways proofs can be valuable beyond the above. E.g., by working through the proof you can gain an insight that leads to a more efficient algorithm, or to an algorithm for a related problem, or to an idea for developing a better test suite to test your implementation, etc.

Some criteria:

  • Answers here ideally shouldn't fit one of the questions above (as I said, please add an answer there if you have it)

  • Should be presentable to Intro. Algorithms students. While the proof itself need not be presentable, the story should be presentable (e.g. the statement of the problems involved, some idea of how the proof led to something that just "eyeballing correctness" would not have). If you are unsure about this point, go ahead and add it as an answer and I'll do my best to see if it can be presented to this audience.

  • Should be as natural as possible. Artificial examples are kinda okay, but real examples are much more motivating to students.

  • Note that I am talking here about abstract proofs for abstract algorithms, not formal (/automated/etc) proofs of algorithm implementations. As a litmus test, the ideas involved should not be language-specific.

(While this question is not exactly research-level, I think it might get more answers here than on cs.SE, as I suspect the answers will come from historical examples in the theory of algorithms that expert researchers on this site are more likely to be familiar with.)

$\endgroup$
  • 1
    $\begingroup$ Maybe this thought is interesting: On the search for an algorithm it often is helpful to find and prove some "structural properties" of the problem at hand which can then be used in an algorithm. $\endgroup$ – Daniel Jan 2 at 17:32
  • 4
    $\begingroup$ The pitch I make to my students is that you simply can't design algorithms (other than the obvious ones) without thinking about correctness. One may think about it sloppily, of course, but nobody seriously proposes using a non-trivial algorithm without having some idea that it should work. A proof of correctness is just a careful recording of a careful line of reasoning about correctness. (That this needs to be pointed out at all is an artifact of the way students often learn about existing algorithms -- as methods that are known to work, where correctness is not really in question.) $\endgroup$ – Neal Young Jan 2 at 20:01
  • 1
    $\begingroup$ Not sure if this fits with your goals, but basically every security vulnerability is a missing proof: somebody (the programmer) thought: this algorithms is safe, can't be used to steal credit card data etc because of <informal argument> ... Then somebody else finds a way to break the algorithm, because e.g. some control flow paths was ignored in the informal analysis. $\endgroup$ – Martin Berger Jan 3 at 13:26
  • 1
    $\begingroup$ @MartinBerger: This seems like a really good potential source of examples - if you know a specific example that would make a great answer! Unfortunately, most of the examples I know of in this space are either side channel attacks (the model was not inclusive enough) or language-specific (eg not taking into account the fact that C doesn't do bounds checking when accessing an array). $\endgroup$ – Joshua Grochow Jan 3 at 19:20
  • 1
    $\begingroup$ @JoshuaGrochow Array bounds checking doesn't remove the underlying problem (use of wrong indices) but transforms the manifestation of the problem (into an exception), so moving from e.g. C to Java just changes the details of what needs to be proven (think: do you want your airplane's autopilot to throw an exception mid-flight). $\endgroup$ – Martin Berger Jan 4 at 11:30
4
$\begingroup$

Here is a natural problem from graph theory where the proof and the algorithm are closely intertwined. In my view, one can discover this algorithm only via thinking about the proof and the algorithm "in parallel." The task is this:

Input: An undirected graph.

Task: Find a subgraph with maximum edge-connectivity.

Note: What makes the task non-trivial is that a subgraph can have larger edge-connectivity than the whole graph. Since there are exponentially many subgraphs, it would take exponential time to check all of them to find the most connected one, even though we can compute the edge-connectivity of any graph in polynomial time.

Below is a part of a lecture note about solving this problem. It shows that the task can be solved in polynomial time, using a subroutine that finds a minimum cut (which is well know to be doable in polynomial time). For short, edge-connectivity is just called connectivity, and is denoted by $\lambda(G)$.

Finding a subgraph with maximum edge connectivity

$\endgroup$
  • $\begingroup$ This is a nice example problem! I might see if I can use it when we do divide & conquer (we typically do that before mincut, but I can give them mincut as an oracle and it will also be nice foreshadowing). In terms of the proof though, if you just want polynomial time, isn't it trivial that mincut is called at most O(m) times (m=# edges), since each time you call it you remove at least one edge? $\endgroup$ – Joshua Grochow Jan 6 at 8:48
  • 1
    $\begingroup$ @JoshuaGrochow Yes, you are perfectly right! Even if the graph has exponentially many edges (it is possible, due to parallel edges, which were not excluded), your argument still carries over, since each min cut call removes at least one full bundle of edges (=all edges between two nodes), and there are at most $n(n-1)/2$ such bundles. However, the $f(n)\leq n-1$ bound is tighter. In fact, it can hold with equality, as shown by the example of an induced path. $\endgroup$ – Andras Farago Jan 6 at 22:57
2
$\begingroup$

A practical answer: In my career I encountered a few scenarios, some with my direct involvement, where I had to prove that my algorithm performs just as good as the currently best known possible. There are many examples where such knowledge can have a direct effect on one's career... In my experience, making a good claim at a design review meeting or to your direct boss can sometimes be more important than actual implementation. Some examples: The first "trivial" example was at the very beginning of my career. I was the only "engineer" in the company. The internet was only at it's beginning and they wrote code for median finding by first sorting the numbers and then take the center element. I actually had to explain why the linear time algorithm actually works in linear time... The second one involved 2D correlation for motion detection. The idea is too long to explain here, but I had to explain (prove) why the specific conditions of the problem makes it possible for my algorithm to run faster than the obvious one.

$\endgroup$
2
$\begingroup$

I see several advantages of mastering the proof of correctness and complexity of an algorithm. I list them below and illustrate with a concrete example. I tried to stay in the domain of classical textbook algorithms.

Understanding why the algorithm works

Certainly the most obvious reason of having proofs. Many algorithms exploit some structure in the problem in a non obvious way. Without proving their correction, there is no way to really understand why it works. Without understanding this, there is no way of really implementing it.

One example of such algorithm is the Blossom algorithm (wikipedia) to find a maximum matching. The idea is to start from an empty matching and iteratively transform it by mixing it with a kind of path called augmented path. When no such path exist anymore, the matching is maximal. One could argue that this algorithm can be implemented without really understanding why it works but finding an augmenting path is not completely obvious and one really need a precise grasp of the object to make it work without bug.

Dynamic programming algorithms also fall into this category. The change-making problem (wikipedia) is a good illustration of that. You have to be careful in defining the relation between the different records so that you are sure it works. The problem is actually also interesting because for some input, greedy approaches work. The fact that it works with the coin systems student are familiar with could mislead them to believe it will always work. Without proofs, people could be tempted to implement a wrong algorithm.

Mastering an algorithm to make variations

Mastering a good toolbox of classical algorithms is essential to be able to design your own efficient algorithms. Knowing techniques such as binary search, fast exponentiation is inspiring to come up with optimization into more complex problems. Understanding the proof of their correctness or complexity is essential to be able to adapt them correctly in a different framework. This is similar to knowing the proof of a theorem in math. Without the proof, you are forced to use whatever statement of the theorem you were able to find in a textbook. With a proof, you can adapt the theorem, relax some hypothesis sometimes, change the underlying algebraic structure etc.

Binary search (wikipedia) is a good and simple illustration of this fact. By understanding the proof of correctness, you know that you need an notion of order and a sorted array. This could be easily forgotten by someone who does not understand why the algorithm is correct. The proof of complexity is also important: the basic textbook will state that the search does $O(\log n)$ access to the array. But it is misleading and hide the fact that you also do $O(\log n)$ comparisons. Applying binary search for structures where equality is cheap but comparing is expensive tells you that it may be better to do a naive search or use some other techniques. Bloom's filters (wikipedia) are also a good illustration of this fact. You need to understand that the quality of the hash function is primordial in their performances.

Another example: the Bellman-Ford algorithm (wikipedia). It is not too hard to understand why it works. If you do not understand the proof, then it is just a shortest path algorithm. Now, if you understand the proof, you see that by changing the underlying semi-ring, you can compute other quantities such as the sum of weights of all path between two points in a DAG, the number of words of length $k$ accepted by a deterministic finite automaton etc.

Complexity guarantees

Some algorithms work by iteratively applying a function until a fix point is reached, the fix point being the solution to our problem. A proof of correction of these algorithms often gives you an upper bound on the number of needed iterations. Using it gives directly gives you an upper bound on the complexity or trade-off between complexity and quality of approximation. The Newton's method (wikipedia) falls into this category, though it may be too mathematical.

Toward implementations

An algorithm may have many forms. From the general idea to concrete implementation. It is important to understand that they are many stages in the conception of the algorithm. Proving the correctness of each step is a big help to ensure a correct implementation in the end. Many textbook algorithms are not implementations but are given as pseudo-code and they still leave you room for optimization when implementing it. Proving the correctness of the algorithm is only the first step toward an efficient implementation. It gives an overview of the property we need in the data structures, it can reveal parts that could be factorized together and grouped into a subfunction etc.

Dijkstra's algorithm (wikipedia) is a very emblematic example of this fact. You can explain the main ideas before giving the details of each subfunction, before describing the heap datastructure to get good complexity guarantees. To finally converge toward an implementation.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.