<p>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 <b>Prog</b> that you want to then extend to the compiled code to get the same property of <b>compiled(Prog)</b>. 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.</p>

<p><i>In practice</i> 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, <i>in general</i> you're probably looking at a problem of compiler correctness. As I understand it, there are two classic ways of doing so. </p>

<p>One option is to have a compiler that takes as input the program <b>Prog</b> and the proof <b>terminates(Prog)</b> and outputs <b>compiled(Prog)</b> and <b>terminates(compiled(Prog))</b> - 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 <a href="http://portal.acm.org/citation.cfm?id=277752">The design and implementation of a certifying compiler</a>, I believe. </p>

<p>Alternatively, you can prove a fact about the function <b>compiles()</b> - that whenever <b>compiles()</b> 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, <a href="http://portal.acm.org/citation.cfm?id=1538788.1538814">Formal verification of a realistic compiler</a>.</p>

<p>(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.)</p>

CC BY-SA 2.5
2010-11-09T16:40:50.083Z
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 ?
Mohammad Alaggan
CC BY-SA 2.5
2010-11-09T16:29:49.080Z
2010-11-09T18:22:47.780Z
2010-11-09T18:22:47.780Z
Rob Simmons
<p>I think it'll take a bit more work to get to a "well-defined" question. In particular, this is problematic:</p>

<blockquote>
  <p>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).</p>
</blockquote>

<p>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".</p>

<p>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.</p>

CC BY-SA 2.5
2010-11-09T22:01:55.787Z
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$.
Mohammad Alaggan
CC BY-SA 2.5
2010-11-09T22:18:30.547Z
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.
Mark Reitblatt
CC BY-SA 2.5
2010-11-09T22:50:32.117Z
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.
Mohammad Alaggan
CC BY-SA 2.5
2010-11-09T22:55:41.090Z
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.
Mark Reitblatt
CC BY-SA 2.5
2010-11-09T23:06:59.797Z
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.
Mark Reitblatt
CC BY-SA 2.5
2010-11-09T23:09:47.240Z
1) By eliminate everything you mean that it proves the undecidability ? 2) The mapping would need the input, otherwise you'd not be able to map a constant function to HALT, however I was not meaning to use "comptuable equivalence", I was meaning that the two compute the same function (without mapping). 3) So you prove that HALT is undecidable just because such a machine will decide semi-computable functions ? So are semi-computable functions has a prove that they are not halting-decidable ?
Mohammad Alaggan
CC BY-SA 2.5
2010-11-09T23:14:24.947Z
Yes, that's what I meant.
Mohammad Alaggan
CC BY-SA 2.5
2010-11-09T23:29:39.650Z
1) I mean you restrict the input class to be empty

2) You need to map into a non-trivial set (neither empty nor universal). If you only restrict them from computing the same function, then I can compute a function that varies in one place and use that instead.

3) Well, I don't think that your HALT is well-defined. I was just pointing out that the set of input TMs would have to ones whose halting set (by definition) was a decidable set. Which is trivial since it's basically parroting the definition.
Mark Reitblatt
CC BY-SA 2.5
2010-11-09T23:33:06.420Z
The definition limits the input TMs to those who do not call HALT. They may call other undecidable machines. Unless the only undecidable machine is HALT, then I am not sure if this is trivial or parroting the definition as you said.
Mohammad Alaggan
CC BY-SA 2.5
2010-11-09T23:47:21.340Z
1) I don't see why being a strong restriction (aka not being a weak trivial restriction) restricts the input class to be empty. Why it is either this or that, there's nothing in the middle ? 2) I am not sure I got what you mean (aim to) by that.
Mohammad Alaggan
CC BY-SA 2.5
2010-11-10T00:21:46.590Z
If you only restrict the input TMs to those that do not directly simulate Q (assuming this is well-defined), that is still undecidable.

You seem fairly confused about TMs. A TM isn't "undecidable" or "decidable". Languages are. A TM can be a "decider" for a decidable language (in which case it halts). Or it can be a recognizer for a semi-decidable language. 

No, HALT is far from the only undecidable language. In fact, there are uncountably many undecidable languages.
Mark Reitblatt
CC BY-SA 2.5
2010-11-10T00:26:37.403Z
1) That wasn't meant to be a rigorous claim.

2) My claim that all decidable languages have a computable mapping from one to the other isn't strictly true. It fails for the trivial cases of the empty language and the universal language (contains everything).
Mark Reitblatt
CC BY-SA 2.5
2010-11-10T00:32:42.367Z
1) Okay. 2) Thanks for the information.
Mohammad Alaggan
CC BY-SA 2.5
2010-11-10T00:36:44.520Z
By "calling other undecidable machines" I also didn't mean it in the rigorous way. I was replying to your claim that "the set of input TMs would have to be ones whose halting set (by definition) was a decidable set" by saying that it isn't necessarily the case. My whole point is that the original proof for the undecidability for the halting problem only demonstrates the impossiblity of having a TM that decides whether HALT itself halts or not, but not to other cases.
Mohammad Alaggan
CC BY-SA 2.5
2010-11-10T00:47:02.667Z
Say you have a class of TM H and a TM Q which decides the halting problem on H: Q(C,x) = 1 iff C halts on x. Then the TM you get by fixing C in Q: R(x) = Q(C,x) is a decider for the halting set of C. So every member of H must have a decidable halting set. This is almost direct since you wanted class where the halting problem was decidable...
Mark Reitblatt
CC BY-SA 2.5
2010-11-10T00:50:18.360Z
2) Just a clarification: that is a theorem. If L, L' are non-trivial computable sets, then L is Turing equivalent to L'.
Mark Reitblatt
CC BY-SA 2.5
2010-11-10T01:02:47.553Z
You are just assuming there is such a Q for H. This was an assumption towards a contradiction in the classical undecidability proof. Now since we fail to get the contradiction by the self-referencing method, this is just an un-discharged assumption. So it is still open of whether such a TM Q exists or not, for the class H which is non-self-referencing.
Mohammad Alaggan
CC BY-SA 2.5
2010-11-10T01:04:15.853Z
2) I would be interested in references for this theorem. Thanks.
Mohammad Alaggan
CC BY-SA 2.5
2010-11-10T01:16:00.537Z
No, I am saying that for any class H with a decidable halting problem that holds. H is a quantified variable.

Your "class H which is non-self-referencing" is not well-defined.
Mark Reitblatt
CC BY-SA 2.5
2010-11-10T01:27:19.963Z
2) It follows directly from the definition of Turing reduction. You can use Soare's recursion theory text as a reference. Or the wikipedia page on Turing reduction points it out as well.
Mark Reitblatt
CC BY-SA 2.5
2010-11-10T01:31:25.753Z
Okay, so recapping what I got so far, and correct me if I am wrong, is that you say that any class H with a decidable halting problem that holds, has each input TM that is in H would has to be one whose halting set is a decidable set. And you claim that my H, which is not well-defined, has TMs whose halting set is undecidable (e.g. TMs for semi-computable functions). Did I get you right ?
Mohammad Alaggan
CC BY-SA 2.5
2010-11-10T02:30:47.860Z
The first part is correct. The second part isn't. H isn't well-defined. I can't say anything about it. 

The whole semi-decidable diversion earlier was pointing out that if you were hoping H would be "interesting" in the sense of including TM's that recognize an undecidable set, then you were going to be disappointed.
Mark Reitblatt
CC BY-SA 2.5
2010-11-10T02:44:52.747Z
Okay. About H, check the latest update in the question (update 3), I hope that it is well defined now. For the last part of your comment, well, that wasn't what I was hoping for, I am sorry if I unintentionally mislead you. 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.
Mohammad Alaggan
CC BY-SA 2.5
2010-11-10T02:57:02.657Z
That still doesn't fix thing. You give a definition of homomorphism on TM, but your definition of H uses something else:
"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)."

Either the transition graph of TM A is homomorphic to TM B, or it isn't. No sequence of steps will change that.

Furthermore, I don't think your "TM homomorphism" does much. You can construct two equivalent TMs that aren't homomorphic.
Mark Reitblatt
CC BY-SA 2.5
2010-11-10T12:07:00.913Z
For the first point, they are already homomorphic, and in a finite number of steps, W will be in the state D, where D is the initial state of Q. For the second point, that's why I replaced Q with the infinite set of all Turing machines computing HALT. This doesn't mean that W will be homomorphic to an infinite number of machines (that's impossible because it has only finite number of states), it just means that Q is a quantified variable.
Mohammad Alaggan
CC BY-SA 2.5
2010-11-10T16:19:09.947Z
That's still not sufficient. For any TM t and any computable problem P, I can give you a TM t' such that t is homomorphic to t' and t computes P. You basically take a TM that computes P, and just embed an unreachable copy of t into it to get t'.
Mark Reitblatt
CC BY-SA 2.5
2010-11-10T17:57:40.180Z
One of the conditions was that that homomorphic embedded copy be reachable with finite number of steps.
Mohammad Alaggan
CC BY-SA 2.5
2010-11-10T18:44:33.687Z
I don't know. It feels like we're just playing a game of whack-a-mole here. It'd be nice if you could come up with a simple definition and restatement of what you want, and edit your question to have that instead of 4+ updates scattered around. So far, all of this has been just trying to make your question well-posed and non-trivial. But the statement has changed so many time that I'm starting to get confused about where we are.
Mark Reitblatt
CC BY-SA 2.5
2010-11-10T19:01:47.310Z
I'll pose a new (different) question instead. Here it is http://cstheory.stackexchange.com/questions/2853/are-there-any-proofs-the-undecidability-of-the-halting-problem-that-does-not-depe
Mohammad Alaggan
CC BY-SA 2.5
2010-11-10T19:02:39.730Z
@Mark: Thanks a lot for your patient and fruitful discussion, I appreciate it!
Mohammad Alaggan
CC BY-SA 2.5
2010-11-10T19:14:20.577Z
No problem. I know how frustrating it can be when you have an "obvious" intuitive statement, but it turns out to be intractably difficult to formalize.
Mark Reitblatt
CC BY-SA 2.5
2010-11-09T20:25:38.237Z
2010-11-09T20:25:38.237Z
Mark Reitblatt
<p>(<strong>UPDATE</strong>: a better formed question is posed <a href="https://cstheory.stackexchange.com/questions/2853/are-there-any-proofs-the-undecidability-of-the-halting-problem-that-does-not-depe">here</a> as the comments for the accepted answer below show that this question is not well-defined)</p>

<hr>

<p>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.</p>

<p>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 ?</p>

<p><strong>The questions is:</strong></p>

<blockquote>
  <p>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 ?</p>
</blockquote>

<p><strong>UPDATE</strong></p>

<blockquote>
  <p>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.</p>
</blockquote>

<p><strong>Background:</strong>
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. </p>

<p><strong>Motivation:</strong>
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.</p>

<p><strong>UPDATE</strong></p>

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

<p>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:</p>

<p>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$.)</p>

<p>To clarify about what is meant by invoking $Q$ on $S$ indirectly:</p>

<p>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)$.</p>

<p><strong>UPDATE 2</strong></p>

<p>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.</p>

<p><strong>UPDATE 3</strong></p>

<p>The definition of Turing Machine homomorphism:</p>

<p>A TM A is homomorphic to TM B if the transition graph of A is homomorphic to that of B, in the <strong>standard</strong> 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.</p>

CC BY-SA 2.5
2010-11-09T15:53:45.773Z
"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?
Sam Nead
CC BY-SA 2.5
2010-11-09T16:05:44.670Z
Indeed it would be tricky. The goal is to define it as the set that does not lead to the contradiction posed in the proof. I would try a shot: 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). Does that sound plausible enough ?
Mohammad Alaggan
CC BY-SA 2.5
2010-11-09T16:17:15.907Z
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](http://wiki.portal.chalmers.se/agda/pmwiki.php) only allows programs which halt.  I think that people working on logic and programming languages have more to say on this.
Tsuyoshi Ito
CC BY-SA 2.5
2010-11-09T16:21:56.667Z
@Tsuyoshi: Thanks for the information, and the link. I am actually more interested on the theoretical results of which classes are known to be halting-decidable (I am not talking either on proving a particular algorithm). The programming language motivation is my colleague's, not mine.
Mohammad Alaggan
CC BY-SA 2.5
2010-11-09T16:33:07.487Z
Wouldn't that break the diagonalization method used to prove the undecidability of the Halting problem?
Mohammad Al-Turkistany
CC BY-SA 2.5
2010-11-09T16:51:30.807Z
@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" :)
Rob Simmons
CC BY-SA 2.5
2010-11-09T16:52:06.557Z
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?
Mohammad Al-Turkistany
CC BY-SA 2.5
2010-11-09T17:01:20.097Z
@Rob Simmons: 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$ invoking $Q$ on $S$ "indirectly" means that there is a (finite) sequence of steps that $W$ would take to make its configuration "homomorphic" to the initial configuration of $Q(S)$.
Mohammad Alaggan
CC BY-SA 2.5
2010-11-09T17:12:54.067Z
@turkistany: The proof provided in the background (in the question), I don't think it depends on the diagonalization method, or am I wrong ?
Mohammad Alaggan
CC BY-SA 2.5
2010-11-09T17:21:23.620Z
@M. Alaggan, If we disallow self-reference, then we can't exclude the existence of always-halting Turing machine $Q$.
Mohammad Al-Turkistany
CC BY-SA 2.5
2010-11-09T17:25:27.330Z
@turkistany: I am not sure I got what you mean, can you elaborate more ?
Mohammad Alaggan
CC BY-SA 2.5
2010-11-09T17:39:06.123Z
A diagonalization proof relies on deriving a contradiction which  leads to the conclusion that TM $Q$ does not exist. If you disallow self-reference then there is no contradiction and you can't exclude the existence of $Q$.
Mohammad Al-Turkistany
CC BY-SA 2.5
2010-11-09T18:41:59.610Z
What is the significance of always-halting Turing machine $Q$?  What problems does this present?
Matt Groff
CC BY-SA 2.5
2010-11-09T18:51:54.637Z
@Matt Groff: turkistany is not speaking of any machine $Q$, he is speaking about $Q$ which decides the halting problem on the set $S$ of non-self-referencing turing machines. If $Q$ always halts, that means that the halding problem for $S$ is decidable.
Mohammad Alaggan
CC BY-SA 2.5
2010-11-09T22:59:59.857Z
@Philip: The problem is that the machine to be tested for halting, doesn't necessarily get executed. Only its discription will be analysed. In this case, it might be buried deep in the discription, and on several recursive levels as well, it might not be always possible to compute if a given description will eventually call itself. However in the exposition above we are not considering the computability of this property, but taking it for granted and reasoning about the resulting sets.
Mohammad Alaggan
CC BY-SA 2.5
2010-11-09T23:26:07.870Z
It's a nice idea. But, yes as you said, it is also may be called by "merging" its states with the current machine, so that the new machine has the machine it calls "coded into" its state transition table. This why I said "homomorphic".
Mohammad Alaggan
CC BY-SA 2.5
2010-11-10T00:50:49.610Z
Some of the discussion at http://cstheory.stackexchange.com/questions/2823/is-one-definition-of-the-word-paradox-something-that-can-be-used-to-prove-the-h seems relevant to your question.
András Salamon
CC BY-SA 2.5
2010-11-10T02:14:51.547Z
I read the your “definition” of “non-self-referencing”.  I cannot call it a definition because you have not defined what it means for a configuration of one Turing machine to be “homomorphic” to a configuration of another Turing machine.  Usually, a homomorphism is defined as a mapping between the set of configurations of one machine to the set of configurations of another machine, and you cannot speak of a homomorphism between two configurations alone.  I doubt that there is any way to define “non-self-referencing Turing machines” while keeping the halting problem still nontrivial.
Tsuyoshi Ito
CC BY-SA 2.5
2010-11-10T02:37:24.603Z
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, labeled with the symbol read off the tape and the symbol written to it, and the direction the head show move to.
Mohammad Alaggan
CC BY-SA 2.5
2010-11-10T03:12:55.740Z
My criticism still applies.  I know what a homomorphism means in the standard sense, but you are speaking of a configuration being homomorphic to another configuration without referring to the whole configuration graphs.  But I am not sure if it matters.  Anyway I do not think that I can answer anything that pleases you (primarily because I do not know much).
Tsuyoshi Ito
CC BY-SA 2.5
2010-11-10T08:53:38.010Z
Possibly related questions: [is there a complexity theory analogue of rices theorem in computability theory?](http://cstheory.stackexchange.com/questions/668/is-there-a-complexity-theory-analogue-of-rices-theorem-in-computability-theory), [MO: completeness easiest hardest problems](https://mathoverflow.net/questions/29550/completeness-easiest-hardest-problems/31804).
Kaveh
<computability><lo.logic>
What do we know about restricted versions of the halting problem
Mohammad Alaggan
# What do we know about restricted versions of the halting problem

(Asked by: username_0 on 2010-11-09)

(**UPDATE**: a better formed question is posed [here](https://cstheory.stackexchange.com/questions/2853/are-there-any-proofs-the-undecidability-of-the-halting-problem-that-does-not-depe) 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.

**Tags:** computability, lo.logic
> **Comments:**
> **username_1**: "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?  
> **username_0**: Indeed it would be tricky. The goal is to define it as the set that does not lead to the contradiction posed in the proof. I would try a shot: 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). Does that sound plausible enough ?  
> **username_2**: 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](http://wiki.portal.chalmers.se/agda/pmwiki.php) only allows programs which halt.  I think that people working on logic and programming languages have more to say on this.  
> **username_0**: @Tsuyoshi: Thanks for the information, and the link. I am actually more interested on the theoretical results of which classes are known to be halting-decidable (I am not talking either on proving a particular algorithm). The programming language motivation is my colleague's, not mine.  
> **username_3**: Wouldn't that break the diagonalization method used to prove the undecidability of the Halting problem?  
> **username_4**: @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" :)  
> **username_3**: 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?  
> **username_0**: @Rob Simmons: 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$ invoking $Q$ on $S$ "indirectly" means that there is a (finite) sequence of steps that $W$ would take to make its configuration "homomorphic" to the initial configuration of $Q(S)$.  
> **username_0**: @turkistany: The proof provided in the background (in the question), I don't think it depends on the diagonalization method, or am I wrong ?  
> **username_3**: @M. Alaggan, If we disallow self-reference, then we can't exclude the existence of always-halting Turing machine $Q$.  
> **username_0**: @turkistany: I am not sure I got what you mean, can you elaborate more ?  
> **username_3**: A diagonalization proof relies on deriving a contradiction which  leads to the conclusion that TM $Q$ does not exist. If you disallow self-reference then there is no contradiction and you can't exclude the existence of $Q$.  
> **username_5**: What is the significance of always-halting Turing machine $Q$?  What problems does this present?  
> **username_0**: @Matt Groff: turkistany is not speaking of any machine $Q$, he is speaking about $Q$ which decides the halting problem on the set $S$ of non-self-referencing turing machines. If $Q$ always halts, that means that the halding problem for $S$ is decidable.  
> **username_0**: @Philip: The problem is that the machine to be tested for halting, doesn't necessarily get executed. Only its discription will be analysed. In this case, it might be buried deep in the discription, and on several recursive levels as well, it might not be always possible to compute if a given description will eventually call itself. However in the exposition above we are not considering the computability of this property, but taking it for granted and reasoning about the resulting sets.  
> **username_0**: It's a nice idea. But, yes as you said, it is also may be called by "merging" its states with the current machine, so that the new machine has the machine it calls "coded into" its state transition table. This why I said "homomorphic".  
> **username_6**: Some of the discussion at http://cstheory.stackexchange.com/questions/2823/is-one-definition-of-the-word-paradox-something-that-can-be-used-to-prove-the-h seems relevant to your question.  
> **username_2**: I read the your “definition” of “non-self-referencing”.  I cannot call it a definition because you have not defined what it means for a configuration of one Turing machine to be “homomorphic” to a configuration of another Turing machine.  Usually, a homomorphism is defined as a mapping between the set of configurations of one machine to the set of configurations of another machine, and you cannot speak of a homomorphism between two configurations alone.  I doubt that there is any way to define “non-self-referencing Turing machines” while keeping the halting problem still nontrivial.  
> **username_0**: 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, labeled with the symbol read off the tape and the symbol written to it, and the direction the head show move to.  
> **username_2**: My criticism still applies.  I know what a homomorphism means in the standard sense, but you are speaking of a configuration being homomorphic to another configuration without referring to the whole configuration graphs.  But I am not sure if it matters.  Anyway I do not think that I can answer anything that pleases you (primarily because I do not know much).  
> **username_7**: Possibly related questions: [is there a complexity theory analogue of rices theorem in computability theory?](http://cstheory.stackexchange.com/questions/668/is-there-a-complexity-theory-analogue-of-rices-theorem-in-computability-theory), [MO: completeness easiest hardest problems](https://mathoverflow.net/questions/29550/completeness-easiest-hardest-problems/31804).  

---

## 2 answers

### Answer by username_8 on 2010-11-09. Score: 9 | Accepted answer

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.

> **Comments:**
> **username_0**: 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$.  
> **username_8**: 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.  
> **username_0**: 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.  
> **username_8**: 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.  
> **username_8**: 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.  
> **username_0**: 1) By eliminate everything you mean that it proves the undecidability ? 2) The mapping would need the input, otherwise you'd not be able to map a constant function to HALT, however I was not meaning to use "comptuable equivalence", I was meaning that the two compute the same function (without mapping). 3) So you prove that HALT is undecidable just because such a machine will decide semi-computable functions ? So are semi-computable functions has a prove that they are not halting-decidable ?  
> **username_0**: Yes, that's what I meant.  
> **username_8**: 1) I mean you restrict the input class to be empty  2) You need to map into a non-trivial set (neither empty nor universal). If you only restrict them from computing the same function, then I can compute a function that varies in one place and use that instead.  3) Well, I don't think that your HALT is well-defined. I was just pointing out that the set of input TMs would have to ones whose halting set (by definition) was a decidable set. Which is trivial since it's basically parroting the definition.  
> **username_0**: The definition limits the input TMs to those who do not call HALT. They may call other undecidable machines. Unless the only undecidable machine is HALT, then I am not sure if this is trivial or parroting the definition as you said.  
> **username_0**: 1) I don't see why being a strong restriction (aka not being a weak trivial restriction) restricts the input class to be empty. Why it is either this or that, there's nothing in the middle ? 2) I am not sure I got what you mean (aim to) by that.  
> **username_8**: If you only restrict the input TMs to those that do not directly simulate Q (assuming this is well-defined), that is still undecidable.  You seem fairly confused about TMs. A TM isn't "undecidable" or "decidable". Languages are. A TM can be a "decider" for a decidable language (in which case it halts). Or it can be a recognizer for a semi-decidable language.   No, HALT is far from the only undecidable language. In fact, there are uncountably many undecidable languages.  
> **username_8**: 1) That wasn't meant to be a rigorous claim.  2) My claim that all decidable languages have a computable mapping from one to the other isn't strictly true. It fails for the trivial cases of the empty language and the universal language (contains everything).  
> **username_0**: 1) Okay. 2) Thanks for the information.  
> **username_0**: By "calling other undecidable machines" I also didn't mean it in the rigorous way. I was replying to your claim that "the set of input TMs would have to be ones whose halting set (by definition) was a decidable set" by saying that it isn't necessarily the case. My whole point is that the original proof for the undecidability for the halting problem only demonstrates the impossiblity of having a TM that decides whether HALT itself halts or not, but not to other cases.  
> **username_8**: Say you have a class of TM H and a TM Q which decides the halting problem on H: Q(C,x) = 1 iff C halts on x. Then the TM you get by fixing C in Q: R(x) = Q(C,x) is a decider for the halting set of C. So every member of H must have a decidable halting set. This is almost direct since you wanted class where the halting problem was decidable...  
> **username_8**: 2) Just a clarification: that is a theorem. If L, L' are non-trivial computable sets, then L is Turing equivalent to L'.  
> **username_0**: You are just assuming there is such a Q for H. This was an assumption towards a contradiction in the classical undecidability proof. Now since we fail to get the contradiction by the self-referencing method, this is just an un-discharged assumption. So it is still open of whether such a TM Q exists or not, for the class H which is non-self-referencing.  
> **username_0**: 2) I would be interested in references for this theorem. Thanks.  
> **username_8**: No, I am saying that for any class H with a decidable halting problem that holds. H is a quantified variable.  Your "class H which is non-self-referencing" is not well-defined.  
> **username_8**: 2) It follows directly from the definition of Turing reduction. You can use Soare's recursion theory text as a reference. Or the wikipedia page on Turing reduction points it out as well.  
> **username_0**: Okay, so recapping what I got so far, and correct me if I am wrong, is that you say that any class H with a decidable halting problem that holds, has each input TM that is in H would has to be one whose halting set is a decidable set. And you claim that my H, which is not well-defined, has TMs whose halting set is undecidable (e.g. TMs for semi-computable functions). Did I get you right ?  
> **username_8**: The first part is correct. The second part isn't. H isn't well-defined. I can't say anything about it.   The whole semi-decidable diversion earlier was pointing out that if you were hoping H would be "interesting" in the sense of including TM's that recognize an undecidable set, then you were going to be disappointed.  
> **username_0**: Okay. About H, check the latest update in the question (update 3), I hope that it is well defined now. For the last part of your comment, well, that wasn't what I was hoping for, I am sorry if I unintentionally mislead you. 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.  
> **username_8**: That still doesn't fix thing. You give a definition of homomorphism on TM, but your definition of H uses something else: "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)."  Either the transition graph of TM A is homomorphic to TM B, or it isn't. No sequence of steps will change that.  Furthermore, I don't think your "TM homomorphism" does much. You can construct two equivalent TMs that aren't homomorphic.  
> **username_0**: For the first point, they are already homomorphic, and in a finite number of steps, W will be in the state D, where D is the initial state of Q. For the second point, that's why I replaced Q with the infinite set of all Turing machines computing HALT. This doesn't mean that W will be homomorphic to an infinite number of machines (that's impossible because it has only finite number of states), it just means that Q is a quantified variable.  
> **username_8**: That's still not sufficient. For any TM t and any computable problem P, I can give you a TM t' such that t is homomorphic to t' and t computes P. You basically take a TM that computes P, and just embed an unreachable copy of t into it to get t'.  
> **username_0**: One of the conditions was that that homomorphic embedded copy be reachable with finite number of steps.  
> **username_8**: I don't know. It feels like we're just playing a game of whack-a-mole here. It'd be nice if you could come up with a simple definition and restatement of what you want, and edit your question to have that instead of 4+ updates scattered around. So far, all of this has been just trying to make your question well-posed and non-trivial. But the statement has changed so many time that I'm starting to get confused about where we are.  
> **username_0**: I'll pose a new (different) question instead. Here it is http://cstheory.stackexchange.com/questions/2853/are-there-any-proofs-the-undecidability-of-the-halting-problem-that-does-not-depe  
> **username_0**: @Mark: Thanks a lot for your patient and fruitful discussion, I appreciate it!  
> **username_8**: No problem. I know how frustrating it can be when you have an "obvious" intuitive statement, but it turns out to be intractably difficult to formalize.  

---

### Answer by username_4 on 2010-11-09. Score: 11

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](http://portal.acm.org/citation.cfm?id=277752), 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](http://portal.acm.org/citation.cfm?id=1538788.1538814).

(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.)

> **Comments:**
> **username_0**: 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 ?  

---

