# What happens when the Linz halting problem proof is based on simulation of the input?

Applying a Simulating Halt Decider to the Linz Halting Problem Proof

Of course it is obvious that no halt decider H can possibly return a correct halt status for any input defined to do the opposite of whatever H reports. This is logically impossible.

It is pretty easy to see with this simplified syntax of the Linz Ĥ that ⟨Ĥ⟩ correctly simulated by an embedded_H (based on a UTM) cannot possibly reach its own simulated final state of ⟨Ĥ.qn⟩ and halt.

When Ĥ is applied to ⟨Ĥ⟩
Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qy ∞
Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn

(a) Ĥ copies its input ⟨Ĥ⟩
(b) Ĥ invokes embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩
(c) embedded_H simulates ⟨Ĥ⟩ ⟨Ĥ⟩
(d) simulated ⟨Ĥ⟩ copies its input ⟨Ĥ⟩
(e) simulated ⟨Ĥ⟩ invokes simulated embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩
(f) simulated embedded_H simulates ⟨Ĥ⟩ ⟨Ĥ⟩
(g) goto (d) with one more level of simulation


Linz, Peter 1990. An Introduction to Formal Languages and Automata. Lexington/Toronto: D. C. Heath and Company. (317-320)

• Comments are not for extended discussion; this conversation has been moved to chat. Commented Oct 13, 2022 at 7:39

This will come as no surprise to most people here, but Linz' proof does not appear to have a fatal flaw. I have prepared a machine checked formalization of the argument here. I didn't implement all the procedures needed to construct $$\hat H$$, but it doesn't seem Linz does either (at least in the quoted material), and only their specification really matters.

So, I think we can safely put this matter to bed. The computer itself believes Linz.

If you want to know where your 'refutation' fails, it's actually somewhat difficult to say, because there appear to be multiple points of confusion.

1. Your remarks about infinite regresses of simulation indicate a failure of the $$\sf Total$$ criterion, where the machine would fail to report an answer because ever more nested copies of the diagonal machine would be simulated. This means that the machine is not a decider on the prescribed inputs at all, so it fails to solve the halting problem in a trivial way.

2. You also seem to say that the machine notices this infinite regress, and instead reports that the diagonal machine doesn't halt because of it.1 This doesn't really make any sense, because if the regress is noticed and avoided, then presumably the regress is noticed during simulation as well, and the regress just doesn't happen...

3. But this aspect also doesn't matter, because it fails to notice that the diagonal machine is not attempting to cause such a regress at all. What it's trying to do is look at what the 'decider' reports and do the opposite. So, if your machine reports that the diagonal machine loops, then what it actually does is halt.

My research indicates that these points have already been explained numerous times, though, so I don't intend to elaborate on them any further. I mainly wanted to provide a relatively simple, machine checked, formal proof, so that there can be no further quibbling about whether the majority of people here are overlooking some flaw in the argument. They aren't.

1: Note that detecting simple self-references like this is also not that novel (in actual practice). The Glasgow Haskell Compiler (for example) has been turning code like:

let x = 1 + x in x


from an infinite loop into a reported exception for decades now.

• Comments are not for extended discussion; this conversation has been moved to chat. Commented Oct 26, 2022 at 16:25

Refutation of the Peter Linz Halting Problem proof

The following shows how Linz H ⟨Ĥ⟩ ⟨Ĥ⟩ gets the right answer because Linz Ĥ.H ⟨Ĥ⟩ ⟨Ĥ⟩ gets the wrong answer

H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* H.qy // Ĥ applied to ⟨Ĥ⟩ halts
H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* H.qn // Ĥ applied to ⟨Ĥ⟩ does not halt

Criterion Measure
H is assumed to be a simulating termination analyzer that aborts the simulation of any input that would cause its own non-termination and returns NO. Otherwise H always returns YES.

Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqy ∞ // Ĥ applied to ⟨Ĥ⟩ halts
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqn // Ĥ applied to ⟨Ĥ⟩ does not halt

Execution trace of Ĥ applied to ⟨Ĥ⟩
(a) Ĥ.q0 The input ⟨Ĥ⟩ is copied then transitions to Ĥ.H
(b) Ĥ.H applied ⟨Ĥ⟩ ⟨Ĥ⟩ (input and copy) simulates ⟨Ĥ⟩ applied to ⟨Ĥ⟩
(c) which begins at its own simulated ⟨Ĥ.q0⟩ to repeat the process
Same execution trace even when infinite loop is removed

It is true that Ĥ.H ⟨Ĥ⟩ ⟨Ĥ⟩ must transition to Ĥ.Hqn to prevent its own infinite execution. It is true that this makes Ĥ ⟨Ĥ⟩ halt. This entails that H ⟨Ĥ⟩ ⟨Ĥ⟩ would be correct to transition to H.qy.

When Ĥ.H ⟨Ĥ⟩ ⟨Ĥ⟩ and H ⟨Ĥ⟩ ⟨Ĥ⟩ correctly apply the above criteria then Ĥ.H ⟨Ĥ⟩ ⟨Ĥ⟩ would transition to Ĥ.Hqn and H ⟨Ĥ⟩ ⟨Ĥ⟩ would transition to H.qy

No one has refuted any of the above reasoning

When a simulating halt decider correctly simulates N steps of its input it derives the exact same N steps that a pure UTM would derive because it is itself a UTM with extra features.

Because of this we can know that the first N steps of ⟨Ĥ⟩ simulated by embedded_H are the actual behavior that ⟨Ĥ⟩ presents to embedded_H for these same N steps.

computation that halts… “the Turing machine will halt whenever it enters a final state” (Linz:1990:234)

Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qy ∞
Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn

When Ĥ is applied to ⟨Ĥ⟩
(Ĥ.q0) The input ⟨Ĥ⟩ is copied then transitions to embedded_H
embedded_H is applied to ⟨Ĥ⟩ ⟨Ĥ⟩ (input and copy)
which simulates ⟨Ĥ⟩ applied to ⟨Ĥ⟩
which begins at its own simulated ⟨Ĥ.q0⟩ to repeat the process.

When we see (after the above N steps) that ⟨Ĥ⟩ correctly simulated by embedded_H cannot possibly reach its simulated final state of ⟨Ĥ.qn⟩ in any finite number of steps of correct simulation then we have conclusive proof that ⟨Ĥ⟩ presents non-halting behavior to embedded_H.

Therefore when embedded_H aborts the simulation of its input and transitions to its own final state of Ĥ.qn it is merely reporting this verified fact.