<p>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.</p>
<p>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.</p>
<p><strong>computation that halts…</strong> “the Turing machine will halt whenever it enters a final state” (Linz:1990:234)</p>
<p><strong>Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qy ∞</strong><br>
<strong>Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn</strong></p>
<p><a href="https://i.sstatic.net/rk1Il.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/rk1Il.png" alt="enter image description here" /></a></p>
<p><strong>When Ĥ is applied to ⟨Ĥ⟩</strong><br>
(Ĥ.q0) The input ⟨Ĥ⟩ is copied then transitions to embedded_H<br>
embedded_H is applied to ⟨Ĥ⟩ ⟨Ĥ⟩ (input and copy)<br>
which simulates ⟨Ĥ⟩ applied to ⟨Ĥ⟩ <br><strong>which begins at its own simulated ⟨Ĥ.q0⟩ to repeat the process.</strong></p>
<p>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.</p>
<p>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.</p>

CC BY-SA 4.0
2023-04-17T13:56:36.007Z
As it’s currently written, your answer is unclear. Please [edit] to add additional details that will help others understand how this addresses the question asked. You can find more information on how to write good answers [in the help center](/help/how-to-answer).
Community
CC BY-SA 4.0
2023-04-08T15:38:18.370Z
2023-04-17T15:54:50.823Z
2023-04-17T15:54:50.823Z
polcott
<p>This will come as no surprise to most people here, but Linz' proof does not appear to have a fatal flaw. <a href="https://github.com/dolio/turing/blob/trunk/src/Halting.agda" rel="noreferrer">I have prepared a machine checked formalization of the argument here</a>. I didn't implement all the procedures needed to construct <span class="math-container">$\hat H$</span>, but it doesn't seem Linz does either (at least in the quoted material), and only their specification really matters.</p>
<p>So, I think we can safely put this matter to bed. The computer itself believes Linz.</p>
<p>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.</p>
<ol>
<li><p>Your remarks about infinite regresses of simulation indicate a failure of the <span class="math-container">$\sf Total$</span> 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.</p>
</li>
<li><p>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.<sup>1</sup> 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...</p>
</li>
<li><p>But this aspect also <em>doesn't matter</em>, 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.</p>
</li>
</ol>
<p>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.</p>
<p>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:</p>
<pre><code>let x = 1 + x in x
</code></pre>
<p>from an infinite loop into a reported exception for decades now.</p>

CC BY-SA 4.0
2022-10-26T16:25:38.087Z
Comments are not for extended discussion; this conversation has been [moved to chat](https://chat.stackexchange.com/rooms/140163/discussion-on-answer-by-dan-doel-does-the-linz-halting-problem-proof-contain-a-f).
Lev Reyzin
CC BY-SA 4.0
2022-09-24T18:49:14.690Z
2022-09-24T18:49:14.690Z
Dan Doel
<p><strong>Refutation of the Peter Linz Halting Problem proof</strong></p>
<p>The following shows how Linz H ⟨Ĥ⟩ ⟨Ĥ⟩ gets the right answer because Linz Ĥ.H ⟨Ĥ⟩ ⟨Ĥ⟩ gets the wrong answer</p>
<p>H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* H.qy // Ĥ applied to ⟨Ĥ⟩ halts<br>
H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* H.qn // Ĥ applied to ⟨Ĥ⟩ does not halt</p>
<p><strong>Criterion Measure</strong><br>
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.</p>
<p>Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqy ∞ // Ĥ applied to ⟨Ĥ⟩ halts<br>
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.Hq0 ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.Hqn // Ĥ applied to ⟨Ĥ⟩ does not halt<br></p>
<p>Execution trace of Ĥ applied to ⟨Ĥ⟩<br>
(a) Ĥ.q0 The input ⟨Ĥ⟩ is copied then transitions to Ĥ.H<br>
(b) Ĥ.H applied ⟨Ĥ⟩ ⟨Ĥ⟩ (input and copy) simulates ⟨Ĥ⟩ applied to ⟨Ĥ⟩<br>
(c) which begins at its own simulated ⟨Ĥ.q0⟩ to repeat the process<br>
<strong>Same execution trace even when infinite loop is removed</strong></p>
<p>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.</p>
<p>When Ĥ.H ⟨Ĥ⟩ ⟨Ĥ⟩ and H ⟨Ĥ⟩ ⟨Ĥ⟩ correctly apply the above criteria then Ĥ.H
⟨Ĥ⟩ ⟨Ĥ⟩ would transition to Ĥ.Hqn and H ⟨Ĥ⟩ ⟨Ĥ⟩ would transition to H.qy</p>
<p><strong>No one has refuted any of the above reasoning</strong></p>

CC BY-SA 4.0
2024-03-06T01:05:51.863Z
2024-03-06T04:55:46.430Z
2024-03-06T04:55:46.430Z
polcott
<p><strong>Applying a Simulating Halt Decider to the Linz Halting Problem Proof</strong></p>
<p>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.</p>
<p>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.</p>
<pre><code>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
</code></pre>
<p><strong>Linz, Peter 1990.</strong> An Introduction to Formal Languages and Automata.
Lexington/Toronto: D. C. Heath and Company. (317-320)</p>
<p><a href="https://i.sstatic.net/8GKtQ.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/8GKtQ.png" alt="enter image description here" /></a></p>

CC BY-SA 4.0
2022-10-13T07:39:13.310Z
Comments are not for extended discussion; this conversation has been [moved to chat](https://chat.stackexchange.com/rooms/139837/discussion-on-question-by-polcott-does-the-linz-halting-problem-proof-contain-a).
Bjørn Kjos-Hanssen
<computability><decidability><undecidability>
What happens when the Linz halting problem proof is based on simulation of the input?
polcott
# What happens when the Linz halting problem proof is based on simulation of the input?

(Asked by: username_0 on 2022-09-21)

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)

**Tags:** computability, decidability, undecidability

> **Comments:**
> **username_1**: Comments are not for extended discussion; this conversation has been [moved to chat](https://chat.stackexchange.com/rooms/139837/discussion-on-question-by-username_0-does-the-linz-halting-problem-proof-contain-a).  

---

## 3 answers

### Answer by username_0 on 2023-04-08. Score: -3 | Accepted answer

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**

[![enter image description here](https://i.sstatic.net/rk1Il.png)](https://i.sstatic.net/rk1Il.png)

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

> **Comments:**
> **username_2**: As it’s currently written, your answer is unclear. Please [edit] to add additional details that will help others understand how this addresses the question asked. You can find more information on how to write good answers [in the help center](/help/how-to-answer).  

---

### Answer by username_3 on 2022-09-24. Score: 7

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.

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.

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

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:**
> **username_4**: Comments are not for extended discussion; this conversation has been [moved to chat](https://chat.stackexchange.com/rooms/140163/discussion-on-answer-by-dan-doel-does-the-linz-halting-problem-proof-contain-a-f).  

---

### Answer by username_0 on 2024-03-06. Score: -1

**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**


---

