TrickiI propose that there should be a page (probably several pages) on how to prove correctness for a (deterministic or randomized) algorithm. However, I'm only aware of a few general methods for doing so; namely, there are "obvious" methods (i.e., the algorithm is correct almost by inspection); there are "energy-increment" methods (the example that comes to mind is showing that the iterative partitioning algorithm in the proof of the regularity lemma terminates); and there are applications of the Szemeredi regularity lemma itself (most useful for establishing, e.g., property testing algorithms – actually, since I can't think of a non-property-testing use in algorithms for the regularity lemma, it might go better on the property testing page itself.)
While I'm aware of these proof methods, I'm fairly sure that I couldn't write articles for any of them (with the possible exception of the almost-by-inspection methods), and I can't off the top of my head think of any other non-trivial ways to prove correctness for a difficult algorithm. Would people be able to write up articles for these or other non-trivial methods?
I think the energy increment argument would come more naturally under the more specific heading of proving that an algorithm terminates. And that can be thought of as an interesting generalization/special case of induction: a nice way of proving that an algorithm, or any other process for that matter, terminates is to define some clever quantity that decreases by some substantial amount at each stage and has to remain positive. (Sometimes it would be a decreasing sequence of integers, and sometimes an increasing sequence of real numbers that is bounded above and takes steps of sizes that would not be absolutely summable if you took infinitely many of them.)
When I read the title of your post but had not yet read the post itself, I interpreted it as what some computer companies try to do: prove that chips really do what they're supposed to do, and that kind of thing. But the examples you give suggest something quite different.
I agree with you about the title, now that I read it over again. I can't really think of a better title, though. It might be better if this topic were to be written "bottom-up" rather than "top-down," i.e., the articles were written first and then collected into a front page, rather than the other way around, since I think the motivating examples are more clear (to me, certainly, and probably to others as well) than the overarching principle of the thing.
Post new comment
(Note: commenting is not possible on this snapshot.)