Refuting the Peter Linz Halting Problem Proof V4
-
- Posts: 1514
- Joined: Mon Jul 25, 2016 6:55 pm
Refuting the Peter Linz Halting Problem Proof V4
When a halt decider bases its halt status decision on the behavior of its simulated input then all of the conventional halting problem counter example inputs would be determined to be non-halting.
A copy of Linz H is embedded at Ĥ.qx as a simulating halt decider (SHD).
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qy ∞
If the pure simulation of ⟨Ĥ⟩ ⟨Ĥ⟩ by embedded_H would reach its final state.
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
If the pure simulation of ⟨Ĥ⟩ ⟨Ĥ⟩ by embedded_H would never reach its final state.
By these two principles this proof is validated
(1) A halt decider (because it is a decider) must report on the behavior specified by its finite string input. A decider computes the mapping from its input finite strings to an accept or reject state.
(2) The behavior specified by this input is the actual behavior of this input when it is correctly simulated by its simulating halt decider (SHD) that contains a full UTM.
The key point that that everyone (including Peter Linz) has an impossibly difficult time with is that embedded_H can correctly transition to Ĥ.qn indicting that its input does not halt.
Everyone (including Peter Linz) incorrectly believes that this is contradictory.
Everyone assumes the the behavior of the executed Ĥ applied ⟨Ĥ⟩ must be the same as the input ⟨Ĥ⟩ ⟨Ĥ⟩ simulated by embedded_H or it is wrong.
We can easily verify that the correct behavior of Ĥ applied ⟨Ĥ⟩ is not the same as the correct behavior as the input ⟨Ĥ⟩ ⟨Ĥ⟩ simulated by embedded_H.
No one ever bothers to do this because of their deep religious conviction that they must either be the same or be incorrect.
Halting problem undecidability and infinitely nested simulation (V4)
https://www.researchgate.net/publicatio ... ulation_V4
A copy of Linz H is embedded at Ĥ.qx as a simulating halt decider (SHD).
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qy ∞
If the pure simulation of ⟨Ĥ⟩ ⟨Ĥ⟩ by embedded_H would reach its final state.
Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
If the pure simulation of ⟨Ĥ⟩ ⟨Ĥ⟩ by embedded_H would never reach its final state.
By these two principles this proof is validated
(1) A halt decider (because it is a decider) must report on the behavior specified by its finite string input. A decider computes the mapping from its input finite strings to an accept or reject state.
(2) The behavior specified by this input is the actual behavior of this input when it is correctly simulated by its simulating halt decider (SHD) that contains a full UTM.
The key point that that everyone (including Peter Linz) has an impossibly difficult time with is that embedded_H can correctly transition to Ĥ.qn indicting that its input does not halt.
Everyone (including Peter Linz) incorrectly believes that this is contradictory.
Everyone assumes the the behavior of the executed Ĥ applied ⟨Ĥ⟩ must be the same as the input ⟨Ĥ⟩ ⟨Ĥ⟩ simulated by embedded_H or it is wrong.
We can easily verify that the correct behavior of Ĥ applied ⟨Ĥ⟩ is not the same as the correct behavior as the input ⟨Ĥ⟩ ⟨Ĥ⟩ simulated by embedded_H.
No one ever bothers to do this because of their deep religious conviction that they must either be the same or be incorrect.
Halting problem undecidability and infinitely nested simulation (V4)
https://www.researchgate.net/publicatio ... ulation_V4
Re: Refuting the Peter Linz Halting Problem Proof V4
Pete, even to those of us who have some passing familiarity with the general nature of the halting problem, your post is fairly impenetrable. Are you able to express the question in more conceptual terms?
Re: Refuting the Peter Linz Halting Problem Proof V4
Dude. How much more of your time are you going to waste on this before you die? You are going down the wrong rabbit hole!
The halting problem can be conceptualised trivially as follows:
1. Rank all models of computation in terms of their expressive power.
2. By definition: a more powerful/expressive model of computation can solve the halting problem for a less powerful/expressive model of computation.
3. NO computational model can solve the halting problem for itself; or for models of computation with equivalent expressive power.
Direct example. Infinite Time Turing Machines (ITTMs) can solve the halting problem for classic Turing Machines (TMs), however ITTMs cannot solve the halting problem for other ITTMs.
It follows by definition that Infinite Time Turing Machines are more powerful models of computation than classic Turing Machines!
And it follows further that IF you are solving the halting problem for any particular model of computation then you are necessarily working with a more powerful model of computation. Your working model cannot solve the halting problem for itself! Which, of course, is a trivial implication of Turing's result that the halting problem is not solvable IN GENERAL, but it is solvable IN PARTICULAR.
I implore you! I beg you! I highly recommend to you that you read this book. You really really need this in order to understand the difference between Type 1 vs Type 2 computability
If you are too lazy to buy/read books at least start with some high level background on nLab.. Yes, you are going to have to cover some ground on topos theory, because you need to understand what the Kneene-Vesley topos is.
-
- Posts: 1514
- Joined: Mon Jul 25, 2016 6:55 pm
Re: Refuting the Peter Linz Halting Problem Proof V4
I will soon update this paper: https://www.researchgate.net/publicatio ... ulation_V5
H does correctly compute the mapping from its x86 finite string input parameters of the machine code of P to its own final reject state on the basis of the actual behavior actually specified by its input.
Th above paper already shows this. I will increase its clarity.
H does correctly compute the mapping from its x86 finite string input parameters of the machine code of P to its own final reject state on the basis of the actual behavior actually specified by its input.
Th above paper already shows this. I will increase its clarity.
Code: Select all
#include <stdint.h>
#define u32 uint32_t
void P(u32 x)
{
if (H(x, x))
HERE: goto HERE;
return;
}
int main()
{
Output("Input_Halts = ", H((u32)P, (u32)P));
}
Re: Refuting the Peter Linz Halting Problem Proof V4
The x86 instruction-set is just one model of computation. It is an assembly language - it contains no inherent semantic distinction between code and data ergo it's equivalent in expressive power to the untyped lambda calculus which can exhibit non-terminating behavior such as never-satisfiable conditional jumps leading to infinite loops. That is sufficient to fuck with any "halting decider" you write in C.PeteOlcott wrote: ↑Sun May 08, 2022 7:12 pm I will soon update this paper: https://www.researchgate.net/publicatio ... ulation_V5
H does correctly compute the mapping from its x86 finite string input parameters of the machine code of P to its own final reject state on the basis of the actual behavior actually specified by its input.
Th above paper already shows this. I will increase its clarity.
#include <stdint.h>
#define u32 uint32_t
void P(u32 x)
{
if (H(x, x))
HERE: goto HERE;
return;
}
int main()
{
Output("Input_Halts = ", H((u32)P, (u32)P));
}
Have you never read Dijkstra's GOTO considered harmful?
https://en.wikipedia.org/wiki/Considered_harmful
It's the differentiator between structured and non-structured programming.
Structured programs can NOT become Turing-complete.
Unstructured programs can become Turing-complete.
https://en.wikipedia.org/wiki/Non-struc ... rogramming
Last edited by Skepdick on Sun May 08, 2022 7:29 pm, edited 1 time in total.
-
- Posts: 1514
- Joined: Mon Jul 25, 2016 6:55 pm
Re: Refuting the Peter Linz Halting Problem Proof V4
The fact that the halt decider contains conditional jumps has no effect what-so-ever on the fact that the correctly simulated input to H(P,P) never reaches its own final state (thus never halts) whether or not H aborts its simulation.Skepdick wrote: ↑Sun May 08, 2022 7:20 pm The x86 instruction-set is just one model of computation.
The assembly language contains conditional jumps. That is sufficient to fuck with any "halting decider" you write in C.
Have you never read Dijkstra's GOTO considered harmful?
https://en.wikipedia.org/wiki/Considered_harmful
The same proof applies the the Linz ⟨Ĥ⟩ ⟨Ĥ⟩.
Yes I have read that many times.
Re: Refuting the Peter Linz Halting Problem Proof V4
Yes, it does!PeteOlcott wrote: ↑Sun May 08, 2022 7:28 pm The fact that the halt decider contains conditional jumps has no effect...
It's precisely what distinguishes structured from non-structured programs.
Conditional jumps are an enabler for non-halting behavior.
https://en.wikipedia.org/wiki/Non-struc ... rogramming
Languages without conditional jumps are NOT Turing complete a.k.a total. Provably terminating etc. etc. etc.
Here's an program for you... Prove that it halts.
Code: Select all
from random import choice
def roll_dice():
return choice([True, False])
def loop():
print("loop")
loop() if roll_dice() else halt()
def halt():
print("halt")
exit(0)
loop()
Code: Select all
➜ ~ python halt.py
loop
loop
halt
➜ ~ python halt.py
loop
loop
loop
loop
loop
loop
loop
halt
➜ ~ python halt.py
loop
loop
halt
https://en.wikipedia.org/wiki/Satisfiability
-
- Posts: 1514
- Joined: Mon Jul 25, 2016 6:55 pm
Re: Refuting the Peter Linz Halting Problem Proof V4
That clearly seems to be dishonest trimming.Skepdick wrote: ↑Sun May 08, 2022 7:30 pmYes, it does!PeteOlcott wrote: ↑Sun May 08, 2022 7:28 pm The fact that the halt decider contains conditional jumps has no effect...
It's precisely what distinguishes structured from non-structured programs.
Conditional jumps are an enabler for non-halting behavior.
The fact that the halt decider contains conditional jumps has no effect
what-so-ever on the fact that the correctly simulated input to H(P,P) never reaches its own final state (thus never halts) whether or not H aborts its simulation.
Last edited by PeteOlcott on Sun May 08, 2022 8:00 pm, edited 2 times in total.
Re: Refuting the Peter Linz Halting Problem Proof V4
Halt and abort are different names for the exact same state!PeteOlcott wrote: ↑Sun May 08, 2022 7:59 pm what-so-ever on the fact that the correctly simulated input to H(P,P) never reaches its own final state (thus never halts) whether or not H aborts its simulation.
Turing machines don't differentiate between errors and halts. Effect systems do.
https://en.wikipedia.org/wiki/Effect_system
In a language that you would understand: Turing machines don't have a notion of exception handling! Strictly speaking neither does C, but you can hack around it with setjmp and longjmp! GOTO statements!
https://stackoverflow.com/questions/105 ... ments-in-c
Re: Refuting the Peter Linz Halting Problem Proof V4
To explain it to you in a language that you might understand... If you are using Infinite Time Turing Machines as a computational model then halting events are equivalent to programming with timeouts.PeteOlcott wrote: ↑Sun May 08, 2022 7:59 pm That clearly seems to be dishonest trimming.
The fact that the halt decider contains conditional jumps has no effect
what-so-ever on the fact that the correctly simulated input to H(P,P) never reaches its own final state (thus never halts) whether or not H aborts its simulation.
A termination-proof either terminates within N units of time, or it doesnt.
If a termination-proof fails to terminate in N units of time that's no evidence that it wouldn't terminate after N+1 units of time.
If a termination-proof fails to terminate in N+1 units of time that's no evidence that it wouldn't terminate after N+2 units of time.
And if it fails to terminate within N^N units of time that's no proof that it wouldn't terminate after N^N + 1 units of time.
All of the above jazz amounts to this trivial bash script.
sleep for a random interval between 1 and 10 seconds. Timeout after 5. Tell us whether the program timed out or terminated.
Code: Select all
➜ ~ timeout 5 /bin/sleep $(shuf -i 1-10 -n 1) && echo "Terminated" || echo "Timed out"
Timed out
➜ ~ timeout 5 /bin/sleep $(shuf -i 1-10 -n 1) && echo "Termination" || echo "Timeout"
Termination
➜ ~ timeout 5 /bin/sleep $(shuf -i 1-10 -n 1) && echo "Termination" || echo "Timeout"
Timeout
Last edited by Skepdick on Sun May 08, 2022 8:46 pm, edited 1 time in total.
-
- Posts: 1514
- Joined: Mon Jul 25, 2016 6:55 pm
Re: Refuting the Peter Linz Halting Problem Proof V4
That is false: computation that halts … the Turing machine will halt whenever it enters a final state.Skepdick wrote: ↑Sun May 08, 2022 8:00 pmHalt and abort are different names for the exact same state!PeteOlcott wrote: ↑Sun May 08, 2022 7:59 pm what-so-ever on the fact that the correctly simulated input to H(P,P) never reaches its own final state (thus never halts) whether or not H aborts its simulation.
Linz, Peter 1990. An Introduction to Formal Languages and Automata. Lexington/Toronto: D. C. Heath and Company. (234)
Re: Refuting the Peter Linz Halting Problem Proof V4
Abort.PeteOlcott wrote: ↑Sun May 08, 2022 8:45 pm That is false: computation that halts … the Turing machine will halt whenever it enters a final state. (Linz234)
Linz, Peter 1990. An Introduction to Formal Languages and Automata. Lexington/Toronto: D. C. Heath and Company. (317-320)
Terminate.
Stop.
Exit.
Blow up.
Execution complete.
Work done.
Terminal object.
Final state.
ALL of those are different names for halting!
-
- Posts: 1514
- Joined: Mon Jul 25, 2016 6:55 pm
Re: Refuting the Peter Linz Halting Problem Proof V4
For Turing machines "halt" means to terminate normally reaching its last instruction.Skepdick wrote: ↑Sun May 08, 2022 8:47 pmAbort.PeteOlcott wrote: ↑Sun May 08, 2022 8:45 pm That is false: computation that halts … the Turing machine will halt whenever it enters a final state. (Linz234)
Linz, Peter 1990. An Introduction to Formal Languages and Automata. Lexington/Toronto: D. C. Heath and Company. (317-320)
Terminate.
Stop.
Exit.
Blow up.
Execution complete.
Work done.
Terminal object.
Final state.
ALL of those are different names for halting!
If you insist on disagreeing with definitions the dialogue cannot continue.
Re: Refuting the Peter Linz Halting Problem Proof V4
If you cannot comprehend the existing definition you are the reason the conversation is going off the rails.PeteOlcott wrote: ↑Sun May 08, 2022 8:52 pm For Turing machines "halt" means to terminate normally reaching its last instruction.
If you insist on disagreeing with definitions the dialogue cannot continue.
Turing machines cannot differentiate between "normal" and "non-normal" termination.
Computer programs have exit codes.
Turing machines don't.
You cannot express the following logic on a Turing machine. You need an effect system!
Code: Select all
timeout $(shuf -i 1-10 -n 1) sleep $(shuf -i 1-10 -n 1) \
&& echo "Termination"
|| echo "Timeout"
Code: Select all
➜ ~ for i in {1..10};do
for> timeout $(shuf -i 1-10 -n 1) sleep $(shuf -i 1-10 -n 1) && echo "Termination" || echo "Timeout";
for> done
Termination
Termination
Timeout
Termination
Termination
Termination
Timeout
Timeout
Termination
Timeout
-
- Posts: 1514
- Joined: Mon Jul 25, 2016 6:55 pm
Re: Refuting the Peter Linz Halting Problem Proof V4
Skepdick wrote: ↑Sun May 08, 2022 8:54 pmIf you cannot comprehend the existing definition you are the reason the conversation is going off the rails.PeteOlcott wrote: ↑Sun May 08, 2022 8:52 pm For Turing machines "halt" means to terminate normally reaching its last instruction.
If you insist on disagreeing with definitions the dialogue cannot continue.
Turing machines cannot differentiate between "normal" and "non-normal" termination.
Eventually, the whole process may terminate, which we achieve in a Turing machine by putting it into a halt state. A Turing machine is said to halt whenever it reaches a configuration for which δ is not defined; this is possible because δ is a partial function. In fact, we will assume that no transitions are defined for any final state, so the Turing machine will halt whenever it enters a final state. (Linz-1990:234)