6
$\begingroup$

Is partial correctness decidable? i.e., is there a general algorithm that for any pair of formal specification and encoded TM, returns true if and only if, when the TM halts, it meets the specification?

I feel that the answer is likely no because of how complex the problem sounds. If the answer is no, please provide a proof or proof sketch.

Improve this question
$\endgroup$

3 Answers 3

Reset to default
20
$\begingroup$

No, it is not decidable. Suppose the formal spec is "if the program halts, it must output 42". (This is a partial correctness requirement.) Suppose f() is any function that constitutes pure computation (it never outputs anything), and consider the following code:

y = f()
output 17

If f() halts, then this code violates the spec, otherwise this code obeys the spec. So determining whether this code satisfies partial correctness is as hard as determining whether f() halts. This is exactly the halting problem. Therefore, partial correctness is undecidable.

I've phrased this in terms of code, for ease of understanding, but you can convert this to an argument in terms of Turing machines if you prefer. The resulting argument can be made fully rigorous and formal.

Improve this answer
$\endgroup$
6
  • 1
    $\begingroup$ Thanks for your time. Let me argue. If f doesn't halt, the code in the answer also violates the spec because the spec says that outputs 42, and an algorithm that doesn't halt doesn't output anything. The partial correctness detector could return false and it would be right for that code, because whether f halts or not, if your code halted it would return 17 which is different than 42 and therefore would violate the spec. So the answer doesn't prove that partial correctness is not decidable. Does that make sense? Regards. $\endgroup$
    – Otakar Molnár López
    Commented Nov 23 at 22:34
  • $\begingroup$ I rephrased my question a little to avoid ambiguities in its interpretation. $\endgroup$
    – Otakar Molnár López
    Commented Nov 23 at 22:41
  • 5
    $\begingroup$ @OtakarMolnárLópez, I think you have a misunderstanding. I believe my answer is correct. I wonder if you might be forgetting that you asked about partial correctness. Code that never halts is partially correct, because the definition of partial correctness says "if the code halts, then ..." and that is vacuously true if the code doesn't halt. I've revised my answer to try to make it clearer. $\endgroup$
    – D.W. ♦
    Commented Nov 24 at 0:57
  • $\begingroup$ Thanks. That makes sense and helps me refine what I am looking for. Maybe what I am looking for is more like a relaxed halting problem solver that returns true (it halts) assuming some mathematical statements as true. For example, given a program that searches for a number that violates the Goldbach's Conjecture, prove that the program does halt and it finds a number violating the conjecture assuming the conjecture is false. But maybe those assumptions should be part of the input, i.e., given in a case by case basis. Anyway. Thanks! @D.W. $\endgroup$
    – Otakar Molnár López
    Commented Nov 25 at 16:16
  • $\begingroup$ @OtakarMolnárLópez, Got it. I have a suspicion that maybe the answer to that might depend on the particular conjecture and/or algorithm used by the solver. $\endgroup$
    – D.W. ♦
    Commented Nov 25 at 19:09
14
$\begingroup$

A well-known generalization of the undecidability of the Halting Problem is Rice's theorem, which says that "all non-trivial semantic properties of programs are undecidable".

Improve this answer
$\endgroup$
3
2
$\begingroup$

Let $M$ be any TM.

Define $N$ as the TM that, on input $n\in\mathbb N$, runs $M$ for $n$ steps on empty input. We make $N$ accept if $M$ halts within those steps, and reject otherwise.

Note that $N$ always halts, no matter what are $M$ and $n$, since it only simulates a finite number of steps.

Consider the spec "$N$ rejects all $n$".

The partial correctness of $N$ w.r.t. the spec states that whenever $N$ halts, it rejects. But $N$ always halts, so partial correctness is equivalent to $N$ always rejecting. That, in turn, is equivalent to $M$ diverging on the empty input.

Therefore, if we could decide partial correctness (on $N$), we could decide the diverging problem (on $M$), hence the halting problem as well. But we know that is not possible, so partial correctness is also undecidable.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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