Can you see that the Linz Halting Problem proof contains a fatal flaw?

Question

Applying a Simulating Halt Decider to the Linz Halting Problem Proof

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.

My reviewers cannot show that any of the extra features added to the UTM change the behavior of the simulated input for the first N steps of simulation:

• Watching the behavior doesn't change it.
• Matching non-halting behavior patterns doesn't change it
• Even aborting the simulation after N steps doesn't change the first N steps.

Because of all 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)

When we see (after 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.

---

A simulating halt decider (SHD) is merely an ordinary universal Turing machine (UTM) with two additional features:
(a) Watches the behavior of its simulated input.
(b) Matches non-halting behavior patterns.

Because a SHD is a UTM we can know that N steps of correct simulation of an input by this SHD do derive the actual behavior specified by this input to this SHD for these N steps.

When these N steps correctly match a correct non-halting behavior pattern then we have conclusive proof that this input does specify non-halting behavior to this SHD. When the SHD rejects its input on this basis it is merely reporting a verified fact.

A simulating halt decider correctly predicts whether or not its correctly simulated input can possibly reach its own final state and halt. It does this by correctly recognizing several non-halting behavior patterns in a finite number of steps of correct simulation. Inputs that do terminate are simply simulated until they complete.

The Linz text indicates that Ĥ is defined on the basis of prepending and appending states to the original Linz H, (assumed halt decider) thus is named embedded_H.

(q0) is prepended to H to copy the ⟨Ĥ⟩ input of Ĥ. The transition from (qa) to (qb) is the conventional infinite loop appended to the (qy) accept state of embedded_H. ⊢* indicates an arbitrary number of moves.

The Linz term “move” means a state transition and its corresponding tape head action {move_left, move_right, read, write}. Ĥ is applied to its own machine description ⟨Ĥ⟩.

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

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

This process continues to repeat until embedded_H recognizes the repeating pattern and aborts its simulation of ⟨Ĥ⟩ ⟨Ĥ⟩. embedded_H can see the same repeating pattern that we see.

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

Every "rebuttal" simply ignores this key fact

⟨Ĥ⟩ ⟨Ĥ⟩ correctly simulated by embedded_H cannot possibly reach its own simulated final state of ⟨Ĥ.qn⟩ and halt in any finite number of steps of correct simulation.

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

Answer 1

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

Answer 2

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.