Re: Proof that H(D,D) meets its abort criteria

On 3/15/24 10:23 AM, olcott wrote:

On 3/15/2024 12:07 PM, immibis wrote:

On 15/03/24 17:20, olcott wrote:

Best selling author of Theory of Computation textbooks:
*Introduction To The Theory Of Computation 3RD, by sipser*
https://www.amazon.com/Introduction-Theory-Computation-Sipser/dp/8131525295/
>
Date 10/13/2022 11:29:23 AM
*MIT Professor Michael Sipser agreed this verbatim paragraph is correct*
(He has neither reviewed nor agreed to anything else in this paper)
(a) 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
(b) H can abort its simulation of D and correctly report that D specifies a non-halting sequence of configurations.
>
*When we apply the abort criteria* (elaborated above)
Will you halt if you never abort your simulation?
*Then H(D,D) is proven to meet this criteria*
>
*Proof that H(D,D) meets its abort criteria*
>
int D(int (*x)())
{
   int Halt_Status = H(x, x);
   if (Halt_Status)
     HERE: goto HERE;
   return Halt_Status;
}
>
int main()
{
   Output("Input_Halts = ", H(D,D));
}
>
  machine   stack     stack     machine    assembly
  address   address   data      code       language
  ========  ========  ========  =========  =============
[00001d22][00102fc9][00000000] 55         push ebp      ; begin main()
[00001d23][00102fc9][00000000] 8bec       mov ebp,esp
[00001d25][00102fc5][00001cf2] 68f21c0000 push 00001cf2 ; push DD
[00001d2a][00102fc1][00001cf2] 68f21c0000 push 00001cf2 ; push D
[00001d2f][00102fbd][00001d34] e8eef7ffff call 00001522 ; call H(D,D)
>
H: Begin Simulation   Execution Trace Stored at:113075
Address_of_H:1522
[00001cf2][00113061][00113065] 55         push ebp       ; enter D(D)
[00001cf3][00113061][00113065] 8bec       mov ebp,esp
[00001cf5][0011305d][00103031] 51         push ecx
[00001cf6][0011305d][00103031] 8b4508     mov eax,[ebp+08]
[00001cf9][00113059][00001cf2] 50         push eax       ; push D
[00001cfa][00113059][00001cf2] 8b4d08     mov ecx,[ebp+08]
[00001cfd][00113055][00001cf2] 51         push ecx       ; push D
[00001cfe][00113051][00001d03] e81ff8ffff call 00001522  ; call H(D,D)
H: Recursive Simulation Detected Simulation Stopped
                           H(D,D) returns 0 to main()
>
*That was proof that H(D,D) meets its abort criteria*
H(D,D) correctly determines that itself is being called with its same inputs and there are no conditional branch instructions between the invocation of D(D) and its call to H(D,D).
>
>

>
There are conditional branch instructions inside H(D,D). This is obvious. Why do you keep lying?

 (a) 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
 It is true that D(D) would never stop running unless the
outermost H(D,D) aborts its simulation thus meeting the
above criteria.
 

Nope, not if D is claimed to be the equivalent of Linz H^.
If you are willing to DISAVOW any posssible conntection to that we can discuss that version, but then you are admitting this is just a time wasting change of topic.
The issue becomes a definition of identity.
IF we are in an equivalency to Linz H/H^, then the H that D calls is a seperate identity to the H that is simulating that D.
Thus, the outer H doesn't NEED to abort, as replacing it (not CHANGING it, as your structure doesn't allow changing it will keeping D defined the same as Linz H^) with a version that doesn't abort then we see that D will call H(D,D) which will simulate that input until it sees it call H(D,D) and then abort and return.
Thus the outer H, although it DOES abort, doesn't abort due to having proven a NEED to abort for the input it has been given (which also happens to abort and return)