-1
$\begingroup$

I have a suspicion that Turing's famous proof that the halting problem is undecidable may not prove exactly what people assume that it proves.

It may only prove that it is possible to limit the interface of a program such that it can't give you the most useful information about its inputs.

This counterargument is motivated by the idea that the human brain may be Turing-equivalent, if we're allowed to ignore issues of unlimited storage and execution time. It's also motivated by the observation that if Turing himself was Turing-equivalent he had a lot more to say about the question of halting than he would have if he were constrained by a boolean return interface.

If we have a program g(), and Turing is attempting to decide whether g() halts or not, and if we don't limit Turing's output vocabulary to a single boolean, and g() calls Turing on itself in a sneaky attempt to generate a paradox, Turing's output might be: "I see what you're doing, g(). I pwn you." Or more likely he might output a peer-reviewed journal article and (nowadays) a TED talk.

To return to the land of artificially constrained vocabulary, a more difficult problem than the original halting problem might be to add just one more possible outcome:

Given a program g(), and a program halts_if_valid() that inspects g() and g()'s inputs and can return one of HALTS, DOESNT, or INVALID, can we prove that halts_if_valid() isn't decideable?

I think a proof that relies on something like the original proof doesn't offer much.

// If halts_if_valid() returns INVALID, it can possibly exist as a valid program.
g() {
  if(halts_if_valid(g) == HALTS) loop_forever();
}

My limited ability with formal proofs doesn't offer me an immediately useful approach to tackling the decidability of halts_if_valid.

So my questions are:

Has anybody done any research on the decidability of the halts-if-valid problem or something similar? And is there anything in the literature that addresses the idea that Turing's proof may be more about limited interface vocabulary than the essence of the decidability of the halting problem?

I assume I'm not the first one to ask these questions; they seem like obvious quiestions to ask. However, I haven't found anything exactly like them by googling, so I'm probably not googling the right terms.

And, to be clear, my assumption is that halts-if-valid is still undecidable. Certainly in the general case (where we have infinite storage and execution time), but also in many or all practically-interesting finite cases. For instance, the case of finite programs that can't modify their own code. Or even the slightly more constrained set of finite programs that can't modify their own code and aren't interpreters. (That would be a fun set to formally specify.)

It would be a highly useful program if it could exist, and therefore it probably can't. I'm just unhappy with a proof that hinges entirely on an overconstrained vocabulary.

$\endgroup$
  • $\begingroup$ Waht does "invalid" mean? $\endgroup$ – orlp Jun 25 at 16:34
  • $\begingroup$ In this case, anything other than HALTS or DOESNT. Yes, I know, I'm not being formal, but hopefully that doesn't obscure the question. It definitly includes: The program has a logical paradox. $\endgroup$ – a10101010 Jun 25 at 16:49
  • $\begingroup$ Valid, on the other hand, would mean, either HALTs or DOESNT, with the implication that it can run. But presented with g(), halts_if_valid would wisely refuse to try to run it. $\endgroup$ – a10101010 Jun 25 at 16:58
  • 4
    $\begingroup$ "I have a suspicion that Turing's famous proof that the halting problem is undecidable may not prove exactly what people assume that it proves." -- If you start a post with "I think decades of TCS experts are wrong", be very careful about having read and understood as much as possible before you hit the "ask" button. (Also, who are "people"?) $\endgroup$ – Raphael Jun 25 at 17:01
  • 1
    $\begingroup$ It's easy to tell that you didn't do that because a) there's no maths in your post (any refutal of a mathematical argument will have to be mathematical) and b) you seem to have completely missed that in the mathematical world of computability, there are no invalid inputs. And with good reason: a validity check can always be folded into the (partial) function being computed; it doesn't add anything interesting to the model. $\endgroup$ – Raphael Jun 25 at 17:03
2
$\begingroup$

A stronger result than Turing's halting problem is Rice's theorem: the determination of any nontrivial property of programs is undecidable.

To be precise, that's a semantic property, i.e. any property of programs determined by their behavior and independent of exactly how the program is expressed: the property has to have the same value for any two programs that have the same behavior. For example, “this program halts” is a semantic property, but “this program begins with p” is not a semantic property so Rice's theorem wouldn't apply to it. “Non-trivial” excludes properties that are true for every single program, or false for every single program.

It doesn't matter what set of answers you use for any variant of the Halting problem, as long as the possible number of answers is finite (e.g. YES/NO/INVALID) you can consider that as three properties ($P \in \text{YES}$, $P \in \text{NO}$, $P \in \text{INVALID}$) and its undecidable to be able to determine which one of these is correct for all possible $P$.

$\endgroup$
  • $\begingroup$ Thank you! This is probably the answer I need. $\endgroup$ – a10101010 Jun 25 at 18:16
  • $\begingroup$ "the determination of any nontrivial property of programs is undecidable" -- this simplification is misleading here. Rice's theorem does by no means say something about "any non-trivial property of programs", but only about a very special class of properties. (cc @a10101010 ) $\endgroup$ – Raphael Jun 25 at 20:25
  • $\begingroup$ @Raphael Could you elaborate? I'm not aware of any restrictions that form a very special class of properties. $\endgroup$ – orlp Jun 25 at 20:26
  • $\begingroup$ The formal statement of Rice's theorem is not very long, I'm sure you can find it. If not, see here. $\endgroup$ – Raphael Jun 25 at 20:46

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.