XPost: comp.theory, comp.software-eng, sci.math.symbolic

The x86utm operating system was created so that the halting problem
could be examined concretely in the high level language of C. H is a
function written in C that analyzes the x86 machine language execution
trace of other functions written in C. H recognizes simple cases of
infinite recursion and infinite loops. The conventional halting problem
proof counter-example template is shown to simply be an input that does
not halt.

H simulates its input with an x86 emulator until it determines that its
input would never halt. As soon as H recognizes that its input would
never halt it stops simulating this input and returns 0. For inputs that
do halt H acts exactly as if it was an x86 emulator and simply runs its
input to completion and then returns 1.

In computability theory, the halting problem is the problem
of determining, from a description of an arbitrary computer
program and an input, whether the program will finish running,
or continue to run forever.
https://en.wikipedia.org/wiki/Halting_problem

Simulating partial halt decider H correctly decides that P(P) never
halts (V2)

int Simulate(u32 P, u32 I)
{
((int(*)(int))P)(I);
return 1;
}

// Simplified Linz Ĥ (Linz:1990:319)
// Strachey(1965) CPL translated to C
void P(u32 x)
{
if (H(x, x))
HERE: goto HERE;
}

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

_Simulate()
[00000ce2](01) 55 push ebp
[00000ce3](02) 8bec mov ebp,esp
[00000ce5](03) 8b450c mov eax,[ebp+0c]
[00000ce8](01) 50 push eax // push 2nd Param [00000ce9](03) ff5508 call dword [ebp+08] // call 1st Param [00000cec](03) 83c404 add esp,+04
[00000cef](05) b801000000 mov eax,00000001
[00000cf4](01) 5d pop ebp
[00000cf5](01) c3 ret
Size in bytes:(0020) [00000cf5]

_P()
[00000d02](01) 55 push ebp
[00000d03](02) 8bec mov ebp,esp
[00000d05](03) 8b4508 mov eax,[ebp+08]
[00000d08](01) 50 push eax // push 2nd Param
[00000d09](03) 8b4d08 mov ecx,[ebp+08]
[00000d0c](01) 51 push ecx // push 1st Param
[00000d0d](05) e870feffff call 00000b82 // call H
[00000d12](03) 83c408 add esp,+08
[00000d15](02) 85c0 test eax,eax
[00000d17](02) 7402 jz 00000d1b
[00000d19](02) ebfe jmp 00000d19
[00000d1b](01) 5d pop ebp
[00000d1c](01) c3 ret
Size in bytes:(0027) [00000d1c]

_main()
[00000d22](01) 55 push ebp
[00000d23](02) 8bec mov ebp,esp
[00000d25](05) 68020d0000 push 00000d02 // push P
[00000d2a](05) 68020d0000 push 00000d02 // push P
[00000d2f](05) e8aeffffff call 00000ce2 // call Simulate
[00000d34](03) 83c408 add esp,+08
[00000d37](01) 50 push eax
[00000d38](05) 6823030000 push 00000323
[00000d3d](05) e810f6ffff call 00000352 // call Output
[00000d42](03) 83c408 add esp,+08
[00000d45](02) 33c0 xor eax,eax
[00000d47](01) 5d pop ebp
[00000d48](01) c3 ret
Size in bytes:(0039) [00000d48]

machine stack stack machine assembly
address address data code language
======== ======== ======== ========= ============= ...[00000d22][00101851][00000000] 55 push ebp ...[00000d23][00101851][00000000] 8bec mov ebp,esp ...[00000d25][0010184d][00000d02] 68020d0000 push 00000d02 // push P ...[00000d2a][00101849][00000d02] 68020d0000 push 00000d02 // push P ...[00000d2f][00101845][00000d34] e8aeffffff call 00000ce2 // call
Simulate
...[00000ce2][00101841][00101851] 55 push ebp ...[00000ce3][00101841][00101851] 8bec mov ebp,esp ...[00000ce5][00101841][00101851] 8b450c mov eax,[ebp+0c] ...[00000ce8][0010183d][00000d02] 50 push eax
Calling:_P()
...[00000ce9][00101839][00000cec] ff5508 call dword [ebp+08] ...[00000d02][00101835][00101841] 55 push ebp ...[00000d03][00101835][00101841] 8bec mov ebp,esp ...[00000d05][00101835][00101841] 8b4508 mov eax,[ebp+08] ...[00000d08][00101831][00000d02] 50 push eax ...[00000d09][00101831][00000d02] 8b4d08 mov ecx,[ebp+08] ...[00000d0c][0010182d][00000d02] 51 push ecx ...[00000d0d][00101829][00000d12] e870feffff call 00000b82 // call H

Begin Local Halt Decider Simulation at Machine Address:d02 ...[00000d02][002118f1][002118f5] 55 push ebp ...[00000d03][002118f1][002118f5] 8bec mov ebp,esp ...[00000d05][002118f1][002118f5] 8b4508 mov eax,[ebp+08] ...[00000d08][002118ed][00000d02] 50 push eax // push P ...[00000d09][002118ed][00000d02] 8b4d08 mov ecx,[ebp+08] ...[00000d0c][002118e9][00000d02] 51 push ecx // push P ...[00000d0d][002118e5][00000d12] e870feffff call 00000b82 // call H ...[00000d02][0025c319][0025c31d] 55 push ebp ...[00000d03][0025c319][0025c31d] 8bec mov ebp,esp ...[00000d05][0025c319][0025c31d] 8b4508 mov eax,[ebp+08] ...[00000d08][0025c315][00000d02] 50 push eax // push P ...[00000d09][0025c315][00000d02] 8b4d08 mov ecx,[ebp+08] ...[00000d0c][0025c311][00000d02] 51 push ecx // push P ...[00000d0d][0025c30d][00000d12] e870feffff call 00000b82 // call H
Local Halt Decider: Infinite Recursion Detected Simulation Stopped

...[00000d12][00101835][00101841] 83c408 add esp,+08 ...[00000d15][00101835][00101841] 85c0 test eax,eax ...[00000d17][00101835][00101841] 7402 jz 00000d1b ...[00000d1b][00101839][00000cec] 5d pop ebp ...[00000d1c][0010183d][00000d02] c3 ret ...[00000cec][00101841][00101851] 83c404 add esp,+04 ...[00000cef][00101841][00101851] b801000000 mov eax,00000001 ...[00000cf4][00101845][00000d34] 5d pop ebp ...[00000cf5][00101849][00000d02] c3 ret ...[00000d34][00101851][00000000] 83c408 add esp,+08 ...[00000d37][0010184d][00000001] 50 push eax ...[00000d38][00101849][00000323] 6823030000 push 00000323 ---[00000d3d][00101849][00000323] e810f6ffff call 00000352 // call Output Input_Halts = 1
...[00000d42][00101851][00000000] 83c408 add esp,+08 ...[00000d45][00101851][00000000] 33c0 xor eax,eax ...[00000d47][00101855][00100000] 5d pop ebp ...[00000d48][00101859][000000bc] c3 ret Number_of_User_Instructions(48)
Number of Instructions Executed(23742)

Because H only acts as a pure simulator of its input until after its
halt status decision has been made it has no behavior that can possibly
effect the behavior of its input. Because of this H screens out its own
address range in every execution trace that it examines. This is why we
never see any instructions of H in any execution trace after an input
calls H.

Halting is provable on the basis that a pure simulation reaches the
final state. P reaches its final state.

Never Halting is provable on the basis that the final state can never be reached.

(a) We know that the x86 execution trace of the simulation of P(P) is a
pure simulation by comparing it to the source-code of P. (also see the
first paragraph).

(b) We know that whether or not H aborts its simulation of its input to
H(P,P) that this input would never reach its final state (proved by the
x86 execution trace shown above).

Because there are no control flow instructions in the execution trace
that would escape the infinite recursion the execution trace proves that
a pure simulation of the above input would never reach its final state.

(c) Because input to H(P,P) would never reach its final state we know
that it never halts.

(d) Because it never halts we know that H(P,P) correctly returns 0
indicating that its input never halts.

If there is no error in (a)(b)(c)(d) then we know H(P,P)==0 is the
correct halt status.

There may be a very high tendency to reject this latter claim
out-of-hand without sufficient review through the human fallibility of
bias. If no error exists in steps (a)(b)(c)(d) then we know that
H(P,P)==0 is the correct halt status of the input to the input to H(P,P).

If P(P) halts and H(P,P)==0 is the correct halt status of the input to
the input to H(P,P) then we have a paradox rather than a contradiction.

The full paper is published here:

https://www.researchgate.net/publication/351947980_Halting_problem_undecidability_and_infinitely_nested_simulation

--
Copyright 2021 Pete Olcott

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

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)