Sujet : Re: Proof that executed HH(DD,DD) and simulated HH(DD,DD) simulate DD correctly -- Mike Terry
De : mikko.levanto (at) *nospam* iki.fi (Mikko)
Groupes : comp.theoryDate : 08. Jun 2024, 07:43:55
Autres entêtes
Organisation : -
Message-ID : <v40r2r$2g592$1@dont-email.me>
References : 1 2 3 4 5 6 7 8 9 10 11
User-Agent : Unison/2.2
On 2024-06-07 13:49:09 +0000, olcott said:
On 6/7/2024 12:49 AM, Mikko wrote:
On 2024-06-06 15:06:22 +0000, olcott said:
<Professor Sipser agreed>
If simulating halt decider H correctly simulates its input D
until H correctly determines that its simulated D would never
stop running unless aborted then
H can abort its simulation of D and correctly report that D
specifies a non-halting sequence of configurations.
</Professor Sipser agreed>
// Simplified Linz Ĥ (Linz:1990:319)
// Strachey(1965) CPL translated to C
void P(u32 x)
{
if (H(x, x))
HERE: goto HERE;
}
People here that are experts in the C programming language know that
*P correctly simulated by H cannot possibly stop running unless aborted*
yet lie about this or to try to get away with the strawman deception
CHANGE-THE-SUBJECT fake rebuttal.
People here who have recently followed these discussions know that "P
correctly simulated by H cannot possibly stop running unless aborted"
does not confirm or contradict anything Linz and Strachey have said.
When P correctly simulated by H meets this criteria
If simulating halt decider H correctly simulates its input P
until H correctly determines that its simulated P would never
stop running unless aborted then
Still unproven whther P ever meets those criteria, in particular
the last "correctly".
H can abort its simulation of P and correctly report that P
specifies a non-halting sequence of configurations.
My first paper in simulating halt deciders has all of the details
including showing the execution trace of P correctly simulated
by H proves a repeating state thus meets the above criteria:
Begin Local Halt Decider Simulation at Machine Address:c36
machine stack stack machine assembly
address address data code language
======== ======== ======== ========= =============
[00000c36][002117ca][002117ce] 55 push ebp
[00000c37][002117ca][002117ce] 8bec mov ebp,esp
[00000c39][002117ca][002117ce] 8b4508 mov eax,[ebp+08]
[00000c3c][002117c6][00000c36] 50 push eax // push P
[00000c3d][002117c6][00000c36] 8b4d08 mov ecx,[ebp+08]
[00000c40][002117c2][00000c36] 51 push ecx // push P
[00000c41][002117be][00000c46] e820fdffff call 00000966 // call H(P,P)
[00000c36][0025c1f2][0025c1f6] 55 push ebp
[00000c37][0025c1f2][0025c1f6] 8bec mov ebp,esp
[00000c39][0025c1f2][0025c1f6] 8b4508 mov eax,[ebp+08]
[00000c3c][0025c1ee][00000c36] 50 push eax // push P
[00000c3d][0025c1ee][00000c36] 8b4d08 mov ecx,[ebp+08]
[00000c40][0025c1ea][00000c36] 51 push ecx // push P
[00000c41][0025c1e6][00000c46] e820fdffff call 00000966 // call H(P,P)
Local Halt Decider: Infinite Recursion Detected Simulation Stopped
*Halting problem undecidability and infinitely nested simulation*
https://www.researchgate.net/publication/351947980_Halting_problem_undecidability_and_infinitely_nested_simulation
-- Mikko