16
$\begingroup$

(UPDATE: a better formed question is posed here as the comments for the accepted answer below show that this question is not well-defined)


The classical proof of the impossibility of the halting problem depends on demonstrating a contradiction when trying to apply the halting detection algorithm to itself as input. See background below for more information.

The contradiction demonstrated applies because of a self-referential paradox (like the sentence "This sentence is not true"). But if we strictly prohibited such self-references (i.e. accepted the fact that such self-references are not decidable to halt), what result are we left with ? Is the halting problem for the remaining set of non-self-referencing machines are decidable to halt or not ?

The questions is:

If we consider a subset of all possible Turing machines, which are not self-referencing (i.e. does not take them selves as input), what do we know about the halting problem for this subset ?

UPDATE

Maybe a better reformulation of what I am after is a better understanding of what defines a decidable set. I was trying to isolate the classical undecidability proof because it doesn't add any information about the undecidability except for the cases where you run HALT on itself.

Background: Assuming towards a contradiction that there is a Turing machine $Q$ that can decide on input $M$ which is an encoding for a Turing machine and $X$, whether or not $M(X)$ halts. Then consider a Turing machine $K$ that takes $M$ and $X$ and uses $Q$ to decide whether $M(X)$ halts or not, and then does the opposite, i.e. $K$ halts if $M(X)$ doesn't halt, and doesn't halt if $M(X)$ halts. Then $K(K)$ demonstrates a contradiction, as $K$ should halt if it doesn't halt, and doesn't halt when it halts.

Motivation: A colleague is working on formal verification of software systems (esp. when the system is already proven at source code level and we want to reprove it for its compiled version, to neutralize compiler issues), and in his case he cares about a special set of embedded control programs for which we know for sure they wouldn't be self-referencing. One aspect of verification he wants to carry out is whether it is guaranteed that the compiled program will halt if the input source code is proven to terminate.

UPDATE

Based on the comments below I clarify the meaning of non-self-referencing Turing machines.

The goal is to define it as the set that does not lead to the contradiction posed in the proof (cf. "Background" above). It might be defined as follows:

Assuming that there is a Turing machine $Q$ that decides the halting problem for a set of Turing machine $S$, then $S$ is non-self-referencing with respect to $Q$ if it excludes all machines that invokes $Q$ on $S$ (directly or indirectly). (Clearly that means that $Q$ can't be a member of $S$.)

To clarify about what is meant by invoking $Q$ on $S$ indirectly:

Invoking $Q$ on $S$ is denoted by a Turing machine $Q$ with a set of states and a certain possible initial inputs on the tape (corresponding to any member of $S$), with the head initially at the beginning of that input. A machine $W$ invokes $Q$ on $S$ "indirectly" if there is a (finite) sequence of steps that $W$ would take to make its configuration "homomorphic" to the initial configuration of $Q(S)$.

UPDATE 2

From an answer below arguing that there are infinitely many Turing machines doing the same task, and so $Q$ is not unique, we change the definition above by saying that $Q$ is not a single Turing machine, but the (infinite) set of all machines computing the same function (HALT), where HALT is the function that decides whather a Turing machine halts on a particular input.

UPDATE 3

The definition of Turing Machine homomorphism:

A TM A is homomorphic to TM B if the transition graph of A is homomorphic to that of B, in the standard sense of homomorphisms of graphs with labeled nodes AND edges. A transition graph (V,E) of a TM is such that V=states, E=transition arcs between states. Each arc is labeled with the (S,W,D), S=symbol read off the tape and W=the symbol to be written to it, and D=the direction the head show move to.

$\endgroup$
  • 5
    $\begingroup$ "the remaining set of non-self-referencing" Before I can sensibly discuss this set, I'd like a definition of "self-reference". However, I think that will be a tricky thing to define? $\endgroup$ – Sam Nead Nov 9 '10 at 15:53
  • 1
    $\begingroup$ There are studies of provably halting programs (this class does not include all halting programs, though). Basically they are a pair of a program and a proof that it halts. For example, if I am not mistaken, Agda only allows programs which halt. I think that people working on logic and programming languages have more to say on this. $\endgroup$ – Tsuyoshi Ito Nov 9 '10 at 16:17
  • 1
    $\begingroup$ @M. Alaggan. Now I'd want a definition of "invokes $Q$ on $S$ indirectly," which I suspect to be as difficult to define as the original "self-reference" :) $\endgroup$ – Rob Simmons Nov 9 '10 at 16:51
  • 2
    $\begingroup$ This raises an interesting question: Are all uncomputability (undecidability) proofs traceable to Cantor's diagonalization method? Is there any undecidability proof that does not rely directly or indirectly on the diagonalization method? $\endgroup$ – Mohammad Al-Turkistany Nov 9 '10 at 16:52
  • 2
    $\begingroup$ Possibly related questions: is there a complexity theory analogue of rices theorem in computability theory?, MO: completeness easiest hardest problems. $\endgroup$ – Kaveh Nov 10 '10 at 8:53
9
$\begingroup$

I think it'll take a bit more work to get to a "well-defined" question. In particular, this is problematic:

Invoking Q on S is denoted by a Turing machine Q with a set of states and a certain possible initial inputs on the tape (corresponding to any member of S), with the head initially at the beginning of that input. A machine W invokes Q on S "indirectly" if there is a (finite) sequence of steps that W would take to make its configuration "homomorphic" to the initial configuration of Q(S).

One problem is that there are infinitely many Turing machines which compute the same function. In the standard diagonalization argument, I can just replace the Q subroutine with another decider for HALT, since there are infinitely many of them. Or a function that is computably equivalent to HALT. So it's not entirely clear to me how to define your notion of "indirect invocation".

A different question might be: for what sets of Turing machines is the halting problem decidable? Here there are an abundance of answers: resource restricted TMs (e.g. use only f(n) space, where f is some specific computable function), TMs that are operationally restricted in some particular way (e.g. read head only moves one way), etc. But, another interesting question is whether membership in that restricted set is decidable, or whether you have to restrict yourself to "promise problems", where you only guarantee a correct answer on some "promised" subset of inputs, but don't verify membership.

$\endgroup$
  • $\begingroup$ Okay, nice, so let's try this: Let H be the (infinite) set of all Turing machines computably equivalent to HALT, then replace my $Q$ with $H$. $\endgroup$ – M. Alaggan Nov 9 '10 at 22:01
  • $\begingroup$ It's not quite that simple. Your definition is paradoxical now, since you are looking for a computable HALT. But if this is computable, any computable function is computably equivalent to it. But if your input set contained semi-computable problems (TMs), you'd have a contradiction since deciding the halting problem for such a TM would give you a decision procedure for that problem. $\endgroup$ – Mark Reitblatt Nov 9 '10 at 22:18
  • $\begingroup$ 1) Wouldn't an uncomputable HALT mean undecidability ? I was assuming such a computable HALT exists, hoping for contradiction. 2) I am not familiar with the concept that all computable functions are computably equivalent to each others, I was quoting you, and meaning that it is a function that solves the HALT problem. Apparently λx.1 is computable but it doesn't decide HALT. Correct me if I am wrong please. About the semi-computable problems, HALT may take infinite number of steps, that would still not lead to a the contradiction in the original proof that HALT is not decidable. $\endgroup$ – M. Alaggan Nov 9 '10 at 22:50
  • $\begingroup$ 1) Right. But the problem is trying to define your notion of "non-self-referencing". Either it's a weak restriction, which allows diagonalization as I argued, or it's a strong restriction which eliminates everything. 2) It's simple. "Computably equivalent" roughly means there is a computable mapping from one to the other that preserves answers. But if I can compute an answer, I can cheat and make the mapping trivial. 3) If the TM deciding HALT doesn't itself terminate, it's not a decider for HALT. $\endgroup$ – Mark Reitblatt Nov 9 '10 at 22:55
  • $\begingroup$ Something else that is a bit confusing is the conflation of TM with the decision problem computed by them. It's not normal to talk about a TM being computationally equivalent to one another. Rather, the functions computed by them can be equivalent (or equal). The problem is that trying to say a TM doesn't simulate another TM is hard to define in general, without giving something concrete to separate the functions computed by them. For example, a Log-space TM can't simulate a TM solving an EXP-space problem. $\endgroup$ – Mark Reitblatt Nov 9 '10 at 23:06
9
$\begingroup$

If I understand your motivation correctly, it's seems like this is a "compiler correctness" issue more than a "restricted halting problem" issue. You have a property (termination) that you've proven for some source level program Prog that you want to then extend to the compiled code to get the same property of compiled(Prog). But the compiler can (in general) do arbitrarily goofy things like implement a turing-complete runtime (say the JVM), compile your terminating program into a JVM bytecode and then dump out an executable that starts the JVM and feeds it your compiled bytecode.

In practice it's probably quite possible to utilize the implicit knowledge you have about how your compiler works to implement a some verification procedure that pretty much proves compiled programs correct given correct source programs (indeed, a lot of automatic verification tools for programs are utilizing implicit knowledge of the algorithm-to-code "compiler" in the brains of programmers). However, in general you're probably looking at a problem of compiler correctness. As I understand it, there are two classic ways of doing so.

One option is to have a compiler that takes as input the program Prog and the proof terminates(Prog) and outputs compiled(Prog) and terminates(compiled(Prog)) - the latter is a proof that can then be double-checked independently of the compiler. The classic paper on this is Necula and Lee's The design and implementation of a certifying compiler, I believe.

Alternatively, you can prove a fact about the function compiles() - that whenever compiles() is giving a terminating input it produces a terminating output. An accessible introduction to this way of thinking about compiler correctness is Xavier Leroy's CACM article, Formal verification of a realistic compiler.

(P.S. I hope this answer is helpful - I recognize it's a bit divergent from the question you asked, so let me know if I'm way off-base and/or repeating something you already know.)

$\endgroup$
  • $\begingroup$ Thanks for the great answer. This would definitly be useful for my colleague. However I (independently from my colleague) am more interested on the theoretical implications on the proof of the halting problem, that if we got rid of the case that showed the contradiction, then what else do we know about the decidability of the halting problem ? $\endgroup$ – M. Alaggan Nov 9 '10 at 16:40

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.