On 8/2/2021 9:01 AM, Charlie-Boo wrote:
> wiki: "a primitive recursive function is a function that can be computed by a computer program [for which] an upper bound [on] the number of iterations of every loop can be determined before entering the loop."
>
> About both the wording and the technical soundness of its intent:
>
> 1. You can perform calculations equivalent to "entering the loop" so that's inconsequential.
>
> 2. You can always simulate that loop to see the actual number of iterations. Is that ok even though it doesn't terminate if applied to a program that doesn't meet this criteria?
>
> 3. Since it calculates a total function it halts and you can prove everything about it because you can simulate its complete execution.
>
> 4. Is this actually equivalent to "provably halts" but then that is equivalent to "halts" since halt <=> provably halts?
>
> C-B
>

Provably halting is simply a pure simulation that reaches a final state.
Proving never halting is proving that the final state can never be
reached. Below is proof that P(P) halts and the input to H(P,P) never
halts.

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) 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.

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.

Once we fully understand all of the above we can see from the execution
trace of H(P,P):

(1) The execution trace is correct because it corresponds to the x86
source-code of P.

(2) The execution trace of the simulation of P(P) cannot possibly ever
reach its final state whether or not this simulation is aborted.

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

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

void P()
{ if(PSR_Decider((u32)P, (u32)P)==0)
if(H1((u32)P, (u32)P))
HERE: goto HERE;
}

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

(a) Whether or not H aborts its simulation of this input the input to
H(P,P) cannot possibly ever reach its final state (proved by the x86
execution trace shown below).

(b) Because input to H(P,P) cannot possibly ever reach its final state
we know that it never halts.

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

(d) P reaches its final state.

_Simulate()
[00000ce2](01) 55 push ebp
[00000ce3](02) 8bec mov ebp,esp
[00000ce5](03) 8b450c mov eax,[ebp+0c]
[00000ce8](01) 50 push eax
[00000ce9](03) ff5508 call dword [ebp+08]
[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
[00000d09](03) 8b4d08 mov ecx,[ebp+08]
[00000d0c](01) 51 push ecx
[00000d0d](05) e870feffff call 00000b82
[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
[00000d2a](05) 68020d0000 push 00000d02
[00000d2f](05) e8aeffffff call 00000ce2
[00000d34](03) 83c408 add esp,+08
[00000d37](01) 50 push eax
[00000d38](05) 6823030000 push 00000323
[00000d3d](05) e810f6ffff call 00000352
[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
....[00000d2a][00101849][00000d02] 68020d0000 push 00000d02
....[00000d2f][00101845][00000d34] e8aeffffff call 00000ce2
....[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

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
....[00000d09][002118ed][00000d02] 8b4d08 mov ecx,[ebp+08]
....[00000d0c][002118e9][00000d02] 51 push ecx
....[00000d0d][002118e5][00000d12] e870feffff call 00000b82
....[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
....[00000d09][0025c315][00000d02] 8b4d08 mov ecx,[ebp+08]
....[00000d0c][0025c311][00000d02] 51 push ecx
....[00000d0d][0025c30d][00000d12] e870feffff call 00000b82
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
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)

--
Copyright 2021 Pete Olcott

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