Is halts-if-valid decideable?

Question

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.

Answer 1

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