Skip to main content
Computer Science

You are not logged in. Your edit will be placed in a queue until it is peer reviewed.

We welcome edits that make the post easier to understand and more valuable for readers. Because community members review edits, please try to make the post substantially better than how you found it, for example, by fixing grammar or adding additional resources and hyperlinks.

Required fields*

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$ Commented Nov 23, 2024 at 22:34
  • $\begingroup$ I rephrased my question a little to avoid ambiguities in its interpretation. $\endgroup$ Commented Nov 23, 2024 at 22:41
  • 6
    $\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$ Commented Nov 24, 2024 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$ Commented Nov 25, 2024 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$ Commented Nov 25, 2024 at 19:09