18
$\begingroup$

We have Hoare logic. Why is it still possible that an algorithm is right but there is no proof that it's correct? Suppose the algorithm is expressed in C. Then we can argue step by step that it's doing what it's supposed to do.

So my question is:

Give me an example of an algorithm that's right but does not have a proof of correctness.

EDIT: I think a little background can help clarify where I'm going. Let me quote Scott Aaronson:

Since the 1970s, there's been speculation that P $\ne$ NP might be independent (that is, neither provable nor disprovable) from the standard axiom systems for mathematics, such as Zermelo-Fraenkel set theory. To be clear, this would mean that either

  1. a polynomial-time algorithm for NP-complete problems doesn't exist, but we can never prove it (at least not in our usual formal systems), or else

  2. a polynomial-time algorithm for NP-complete problems does exist, but either we can never prove that it works, or we can never prove that it halts in polynomial time.

I'm referring to the second possibility. Since Aaronson can so confidently list it as a possibility, I think there must be an existing example of type 2. That's why I'm asking this question. But it seems a quick and clear answer is not in view.

$\endgroup$
  • 17
    $\begingroup$ What does it mean to say that an algorithm is correct if we don't have a proof of correctness? $\endgroup$ – David Richerby Jan 31 '17 at 10:20
  • 14
    $\begingroup$ Do you mean "proof of correctness is impossible" or "nobody proved it to be correct"? $\endgroup$ – gnasher729 Jan 31 '17 at 11:07
  • 12
    $\begingroup$ Algorithms don't have to be correct... suppose you have this: (1) put an empty bucket on the windowsill in the morning. (2) take it down in the evening. (3) measure the volume of water in the bucket. (4) repeat next morning. This is a description of an algorithm, but it doesn't describe anything that can be, without a stretch, called "correct". Interestingly, most programming code in the world is written in this particular way: it just isn't concerned with correctness of what it does at all. $\endgroup$ – wvxvw Jan 31 '17 at 12:09
  • $\begingroup$ @wvxvw I'm confused then, what does it mean for an algorithm to be "correct" then? If it does what it was intended to do, doesn't that mean it's correct? If the goal of your scenario was to find the average amount of water collected in the bucket during rainfall, for every day, wouldn't the algorithm be correct in that case? $\endgroup$ – Abdul Jan 31 '17 at 13:06
  • 8
    $\begingroup$ @chi you don't understand... it's not that programmers don't care for correctness of their code, it's that for some algorithms the concept of "correctness" is not applicable. Take some .NET WindowsForms application, which says something to the effect: "put this button with this label at this position, then put this other button at this other position and so on..." - there might be some interpretation of what this program does, under which what it does may be judged as (in)correct (eg. graphic designer says it "looks ugly"), but that's as far as it goes. $\endgroup$ – wvxvw Jan 31 '17 at 14:53
49
$\begingroup$

Here is an algorithm for the identity function:

  • Input: $n$
  • Check if the $n$th binary string encodes a proof of $0 > 1$ in ZFC, and if so, output $n+1$
  • Otherwise, output $n$

Most people suspect this algorithm computes the identity function, but we don't know, and we can't prove it in the commonly accepted framework for mathematics, ZFC.

$\endgroup$
  • 2
    $\begingroup$ Are you sure Check if the $n$th binary string encodes a proof of $0 > 1$ in ZFC is an algorithm? $\endgroup$ – Dmitry Grigoryev Jan 31 '17 at 13:50
  • 23
    $\begingroup$ No, but the check can definitely be implemented algorithmically (i.e., by a Turing machine). In fact this is one of the requirements we have for proof systems - that proof validity be checkable algorithmically. $\endgroup$ – Yuval Filmus Jan 31 '17 at 13:52
  • 6
    $\begingroup$ @Puppy ZFC proves $\lnot (0>1)$. But it could also prove $0>1$ if(f) it is inconsistent. Nearly everybody believes ZFC is consistent, of course, but because of the incompleteness theorems we can't know that for sure. $\endgroup$ – chi Jan 31 '17 at 21:34
  • 1
    $\begingroup$ @Nathaniel Not at all. You can easily prove the correctness of every textbook algorithm, for example. This algorithm differs in that it relies on the consistency of ZFC, which is something that ZFC itself cannot prove. $\endgroup$ – Yuval Filmus Feb 2 '17 at 9:15
  • 1
    $\begingroup$ @Nathaniel: If you like, let us continue this discussion in chat. $\endgroup$ – user21820 Feb 2 '17 at 15:07
9
$\begingroup$

Most algorithms have not been proven correct in Hoare logic. The main reason is that such correctness proofs are extremely expensive as of Jan 2017, probably by several orders of magnitude in comparison with 'mere' programming. There is a lot of ongoing work to reduce this cost by automation, but it's an uphill struggle.

Another reason why an algorithm might not have a correctness proof, and one that is more relevant in practise than the incompleteness phenomena that Yuval and chi mentioned, is that we might not know what this specification is. This problem has two dimensions.

  • The customers don't know what they want. This is a well-known problem in software engineering, and software engineers have developed many approaches to deal with this.

  • The specification is difficult. A good example is the correctness of cryptographic algorithms. Only recently Micali & Goldwasser won Turing awards for specifying what cryptographic security means. Note however that that definition is (as far as I'm aware) for "theoretical cryptography" where you have a security parameter $n$ ranging over natural numbers, and adversaries are polynomial time probabilistic Turing machines. To the best of my knowledge (please correct me if I'm wrong) there is a mismatch between theory and practise, and concrete algorithms like AES and SHA256 are not quite within the purview of those theoretical specifications. I don't think there is full specification for such algorithms, hence we cannot, in principle verify them in the sense of e.g. Hoare logic.

$\endgroup$
  • $\begingroup$ AES is within the purview of definitions of cryptographic security. (You do need to use concrete security definitions rather than asymptotic definitions, but you should be doing that anyway if you want security in practice.) $\endgroup$ – D.W. Jan 31 '17 at 14:40
  • $\begingroup$ @D.W. Interesting. I was not aware of this. How is the asymptotic nature of theoretical cryptography circumvented? Can you please point me towards a paper on this? What about concrete cryptographic hash functions? $\endgroup$ – Martin Berger Jan 31 '17 at 14:49
  • $\begingroup$ en.wikipedia.org/wiki/Concrete_security, and the references listed there. Hash functions are a more complex case, because it depends on what you use them for -- but the complexities are largely orthogonal to asymptotic security vs concrete security. $\endgroup$ – D.W. Jan 31 '17 at 18:20
  • 2
    $\begingroup$ For encryption, you need two algorithms: One that encrypts, one that decrypts. One of them cannot be correct on its own. They can only be correct in a pair (you prove that decrypting an encrypted input produces the original). But for encryption, you want it to be uncrackable and that's something you cannot catch with "correctness". $\endgroup$ – gnasher729 Jan 31 '17 at 18:44
  • 1
    $\begingroup$ @D.W. I have to disagree somewhat. While the papers by Rogaway and Bellare are great implying that they in any way allow for security proofs of primitives is misleading. Both of the papers are essentially about protocols (i.e. they assume primitives such as AES, SHA,RSA etc.) are secure and then prove things from there. The essential problem of proving the primitives themselves secure remains. If you have any references for proofs of primitives being secure I'd be interested. The second paper for example assumes RSA is hard which is very much an open problem. $\endgroup$ – DRF Feb 1 '17 at 9:15
5
$\begingroup$

This is tied to the incompleteness of the underlying logic. Indeed, Hoare logic usually contains a weakening or "pre-post" rule $$ \dfrac{ P \implies P' \qquad \{P'\}c\{Q'\} \qquad Q' \implies Q' }{ \{P\}c\{Q\} } $$ where the implications $P\implies P', Q\implies Q'$ need to be proved in an underlying logic, usually First-Order Logic (FOL) with some set-theoretic axiomatization like Zermelo-Fraenkel (ZF).

The tricky part is that we know such logic is incomplete, as proved by Gödel almost one century ago. More concretely, there is a predicate on natural numbers $P(n)$ for which we can prove inside the logic $P(0)$, $P(1)$, $P(2)$ and so on for any given natural constant, but there is no way to prove $\forall n\in \mathbb{N}.\ P(n)$.

From the computer science side, this weird behavior can be exemplified using computability theory. Suppose a Turing Machine $M$ when run on the empty tape does not halt in $n$ steps ($P(n)$). Then, in ZF we can prove such fact by essentially unraveling the execution step-by-step in the proof. However, when $M$ diverges, we can not hope to be able to prove divergence in ZF ($\forall n.\ P(n)$). Indeed, if this were possible for all given $M$, then we could semi-decide divergence by enumerating all the possible proofs for $\forall n.\ P(n)$, and halting when one is found. Since we know that divergence is not RE, this is impossible.

$\endgroup$
5
$\begingroup$

Problem: Print "Yes" if every even number ≥ 4 is the sum of two primes, and "No" if there is an even number ≥ 4 that is not the sum of two primes.

Algorithm: Print "Yes"

Most people think that the algorithm is correct. There is no known proof, and it is quite possible that there is no proof.

$\endgroup$
3
$\begingroup$

Any algorithm that is correct but we don't know how long it takes to run can be transformed into an algorithm that stops in a guaranteed amount of time but we aren't sure if it is correct.

For example, to find a prime larger than $n$, start counting up from $n+1$ testing if each number is prime until you find one. Now modify it to give up and return $0$ if we can't find a prime after $\log(n)^2$ tries. If the modified algorithm ever returns $0$, it is incorrect, but nobody knows if that ever happens or not. Even with as many as $\sqrt{n}$ steps we can't prove a prime will always be found.

So, we have an algorithm that is correct but we have no proof that it runs in polynomial time, and an algorithm (the same one, but time-limited) that runs in polynomial time but we have no proof that it is correct. And like with the $P=NP$ problem, for this example it is also plausible that no such proofs exist.

$\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.