What do we know about restricted versions of the halting problem

Question

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

Answer 1

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.

Answer 2

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