9

I am referring to the question here: powerful algorithms too complex to implement.

If an algorithm is powerful, but too complex to implement, how can you be sure that the algorithm is correct? Without implementation you won't be able to test the algorithm in a real world scenario, and such a complex algorithm can contain bugs, which may invalidate the algorithm.

This is what I do not understand; if you have the techniques to prove the correctness of an algorithm, then you would have the algorithm to implement it already, isn't it? Or else how can we be sure that the proving technique is correct?

I'm sorry if I sound elementary!

Update from Kaveh ( reproduced here because the argument is better!):

If you can formally prove the correctness of an algorithm in a formal system like Coq then you can also extract the algorithm (because essentially you have implemented the algorithm), but the key fact is that for most algorithms we don't give formal proofs of correctness for the algorithm, we use informal proofs of correctness. The proofs can be false, which does happen from time to time, and even a formal proof of correctness will not make us absolutely sure that the algorithm is correct.

Community
  • 1
Graviton
  • 409
  • 5
  • 13
  • If it's too complex to implement, there'll be no implementations, so it's a moot point. Ignoring that, the techniques will be the same as usual: debugging and verification. Except that it will be a tedious activity, likely to be beyond the state of the art in those areas. – Dave Clarke Jan 24 '11 at 09:03
  • 6
    This is why we have techniques to prove correctness of algorithms, even if (correct) implementation on a real machine is hard. – Raphael Jan 24 '11 at 10:42
  • @Raphael, but this is what I do not understand; if you have the techniques to prove it, then you would have the algorithm to implement it already, isn't it? – Graviton Jan 24 '11 at 11:15
  • 1
    You have the algorithm, but that doesn't mean that it is easy to implement. – Vinicius dos Santos Jan 24 '11 at 11:43
  • 9
    I agree with Raphael. It appears that the question is based on an assumption that the correctness of an algorithm is usually proved by implementing it, but it is not the case. Proving the correctness of an algorithm and implementing an algorithm are completely different things, and one thing does not imply the other in either direction. – Tsuyoshi Ito Jan 24 '11 at 11:45
  • 1
    I think that the question is too elementary for this site. Voted to close it as off topic. – Tsuyoshi Ito Jan 24 '11 at 11:46
  • I think the real question is what makes some algorithms much easier to prove correct than to implement. – Jouni Sirén Jan 24 '11 at 12:03
  • 1
    @Graviton On paper, you have an abstract machine model (semantics) and often don't care about data structures very much. Numeric effects (floating point numbers, overflows, ...) are most often ignored. Or take an extreme example: given (false) assumptions, you can prove algorithms "correct" that can never be implemented. This is just the good old gap between theory and practice resp. the used techniques. You can use non-constructive techniques for proofs (e.g. by contradiction) but that won't help you implementing. – Raphael Jan 24 '11 at 12:16
  • 8
    Simple algorithms with complex proofs of correctness -- how do you know that they are right? Just because an algorithm works on test examples doesn't mean it works on all inputs. – Peter Shor Jan 24 '11 at 12:31
  • 2
    I agree with most of the comments, but I think they are missing a key point.

    If you can formally prove the correctness of an algorithm in a formal system like Coq then you can also extract the algorithm (because essentially you have implemented the algorithm), but the key fact is that for most algorithms we don't give formal proofs of correctness for the algorithm, we use informal proofs of correctness. The proofs can be false, that does happen from time to time, and even a formal proof of correctness will not make us absolutely sure that the algorithm is correct.

     – Kaveh Jan 24 '11 at 13:38
  • @Kaveh, I think you summed up my argument in a succinct and perfect manner. I'll incorporate your part into the question. – Graviton Jan 24 '11 at 13:40
  • I.e. there is no way to be absolutely sure that an algorithm is correct. (and even if it is correct, it does not mean that it will work with no problem in practice, the OS and the physical machine running the algorithm, ... can fault and cause the algorithm give incorrect results.) – Kaveh Jan 24 '11 at 13:42
  • One of the examples given as answer to the other question was Risch's integration algorithm. Assuming Wikipedia to be roughly correct, the reason there is no complete implementation is that it relies on being able to check whether an expression is identically zero, which is really nasty when the expression can be built up from basic arithmetic and nth roots. So if one step in your algorithm says "if (E = 0) then ... else ..." it can be easy to prove that the transformation is correct but complex to implement the test. (This is a special case of Raphael's answer). – Peter Taylor Jan 24 '11 at 15:40
  • Kaveh, I assumed a proof (i.e. correct), of course. A non-proof does never show anything, agreed. Fear of mistakes can not be an argument against proofs, otherwise TCS would be pretty pointless. By the way, we all missed one important point: Proving the correctness of a pen&paper algorithm is fine but does not imply the correctness of a given implementation. There are ways around that, but one has to be bear that in mind. Note that this also applies to the transformation step from source code to machine code. – Raphael Jan 25 '11 at 12:32
  • A professor of mine used to joke that for any given iterative implementation of Quicksort found in any text book, there would be at least one mistake. So far I have not been able to prove him wrong. – Raphael Jan 25 '11 at 12:32
  • 5
    "Beware of bugs in the above code; I have only proved it correct, not tried it." ~Donald Knuth – Lev Reyzin Jan 25 '11 at 14:07

1 Answers1

11

Several years ago, there has been a (rather harsh) debate on a topic similar to this. It all started when several complex proofs turned out to be incorrect, and some researchers started to raise doubts on the very nature of proofs (well, I should have said "provable cryptography," but for the sake of generality, I didn't). Both sides of the controversy accused the other to misunderstand the concepts. Here's a link for more info.

Proofs are our (mathematical) tools to prove theorems/algorithms are correct, but when they became too complex, we may slip and prove wrong things to be right. The recent 100-or-so-page proof on P≠NP is an excellent example. However, this does not rule out the very nature of proofs: Nothing's wrong with them.

One last point: I think studying the philosophy of science will give us more insight on this. (Under the given link, see the bullet "How do we know whether a mathematical proof is correct?")

a3nm
  • 9,269
  • 27
  • 86
Sadeq Dousti
  • 16,479
  • 9
  • 69
  • 152