How do we know H(P,P)==0 is the correct halt status for the input to H? (H1 copy of H)

[olcott]

To prove that H(P,P)==0 is correct we create an exact
copy of H and change P to Call this exact copy: H1.

H can see that H1 aborts the simulation of its input
and returns 1 indicating that its input halts.

When H had to rely on itself to abort the simulation
of P(P) is correctly reports that its input never halts.

void P(u32 x)
{
if (H1(x, x))
HERE: goto HERE;
}


int main()
{
Output("Input_Halts = ", H((u32)P, (u32)P));
}

_P()
[00000e52](01) 55 push ebp
[00000e53](02) 8bec mov ebp,esp
[00000e55](03) 8b4508 mov eax,[ebp+08]
[00000e58](01) 50 push eax
[00000e59](03) 8b4d08 mov ecx,[ebp+08]
[00000e5c](01) 51 push ecx
[00000e5d](05) e8b0fcffff call 00000b12 // call H1
[00000e62](03) 83c408 add esp,+08
[00000e65](02) 85c0 test eax,eax
[00000e67](02) 7402 jz 00000e6b
[00000e69](02) ebfe jmp 00000e69
[00000e6b](01) 5d pop ebp
[00000e6c](01) c3 ret
Size in bytes:(0027) [00000e6c]

_main()
[00000e72](01) 55 push ebp
[00000e73](02) 8bec mov ebp,esp
[00000e75](05) 68520e0000 push 00000e52
[00000e7a](05) 68520e0000 push 00000e52
[00000e7f](05) e84efeffff call 00000cd2 // call H
[00000e84](03) 83c408 add esp,+08
[00000e87](01) 50 push eax
[00000e88](05) 6823030000 push 00000323
[00000e8d](05) e8c0f4ffff call 00000352
[00000e92](03) 83c408 add esp,+08
[00000e95](02) 33c0 xor eax,eax
[00000e97](01) 5d pop ebp
[00000e98](01) c3 ret
Size in bytes:(0039) [00000e98]

machine stack stack machine assembly
address address data code language
======== ======== ======== ========= =============
...[00000e72][00101a94][00000000] 55 push ebp
...[00000e73][00101a94][00000000] 8bec mov ebp,esp
...[00000e75][00101a90][00000e52] 68520e0000 push 00000e52
...[00000e7a][00101a8c][00000e52] 68520e0000 push 00000e52
...[00000e7f][00101a88][00000e84] e84efeffff call 00000cd2 // call H

Begin Local Halt Decider Simulation at Machine Address:e52
...[00000e52][00211b34][00211b38] 55 push ebp
...[00000e53][00211b34][00211b38] 8bec mov ebp,esp
...[00000e55][00211b34][00211b38] 8b4508 mov eax,[ebp+08]
...[00000e58][00211b30][00000e52] 50 push eax
...[00000e59][00211b30][00000e52] 8b4d08 mov ecx,[ebp+08]
...[00000e5c][00211b2c][00000e52] 51 push ecx
...[00000e5d][00211b28][00000e62] e8b0fcffff call 00000b12 // call H1

Begin Local Halt Decider Simulation at Machine Address:e52
...[00000e52][0025c55c][0025c560] 55 push ebp
...[00000e53][0025c55c][0025c560] 8bec mov ebp,esp
...[00000e55][0025c55c][0025c560] 8b4508 mov eax,[ebp+08]
...[00000e58][0025c558][00000e52] 50 push eax
...[00000e59][0025c558][00000e52] 8b4d08 mov ecx,[ebp+08]
...[00000e5c][0025c554][00000e52] 51 push ecx
...[00000e5d][0025c550][00000e62] e8b0fcffff call 00000b12 // call H1
...[00000e52][002a6f84][002a6f88] 55 push ebp
...[00000e53][002a6f84][002a6f88] 8bec mov ebp,esp
...[00000e55][002a6f84][002a6f88] 8b4508 mov eax,[ebp+08]
...[00000e58][002a6f80][00000e52] 50 push eax
...[00000e59][002a6f80][00000e52] 8b4d08 mov ecx,[ebp+08]
...[00000e5c][002a6f7c][00000e52] 51 push ecx
...[00000e5d][002a6f78][00000e62] e8b0fcffff call 00000b12 // call H1
Local Halt Decider: Infinite Recursion Detected Simulation Stopped

...[00000e62][00211b34][00211b38] 83c408 add esp,+08
...[00000e65][00211b34][00211b38] 85c0 test eax,eax
...[00000e67][00211b34][00211b38] 7402 jz 00000e6b
...[00000e6b][00211b38][00000d8f] 5d pop ebp
...[00000e6c][00211b3c][00000e52] c3 ret
...[00000e84][00101a94][00000000] 83c408 add esp,+08
...[00000e87][00101a90][00000001] 50 push eax
...[00000e88][00101a8c][00000323] 6823030000 push 00000323
---[00000e8d][00101a8c][00000323] e8c0f4ffff call 00000352
Input_Halts = 1
...[00000e92][00101a94][00000000] 83c408 add esp,+08
...[00000e95][00101a94][00000000] 33c0 xor eax,eax
...[00000e97][00101a98][00100000] 5d pop ebp
...[00000e98][00101a9c][00000004] c3 ret
Number_of_User_Instructions(1)
Number of Instructions Executed(617658)



--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein