XPost: comp.theory, sci.logic, sci.math

Within the definition of the x86 language H(P,P)==0 is a necessary
consequence for every simulating halt decider H.

// 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 = ", H((u32)P, (u32)P));
}

_P()
[00000c36](01) 55 push ebp
[00000c37](02) 8bec mov ebp,esp
[00000c39](03) 8b4508 mov eax,[ebp+08] // 2nd Param
[00000c3c](01) 50 push eax
[00000c3d](03) 8b4d08 mov ecx,[ebp+08] // 1st Param
[00000c40](01) 51 push ecx
[00000c41](05) e820fdffff call 00000966 // call H
[00000c46](03) 83c408 add esp,+08
[00000c49](02) 85c0 test eax,eax
[00000c4b](02) 7402 jz 00000c4f
[00000c4d](02) ebfe jmp 00000c4d
[00000c4f](01) 5d pop ebp
[00000c50](01) c3 ret
Size in bytes:(0027) [00000c50]

machine stack stack machine assembly
address address data code language
======== ======== ======== ========= ============= [00000c56][0010172a][00000000] 55 push ebp [00000c57][0010172a][00000000] 8bec mov ebp,esp [00000c59][00101726][00000c36] 68360c0000 push 00000c36 // push P [00000c5e][00101722][00000c36] 68360c0000 push 00000c36 // push P [00000c63][0010171e][00000c68] e8fefcffff call 00000966 // call H(P,P)

Begin Local Halt Decider Simulation at Machine Address:c36 [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)

As Flibble pointed out the first time that the simulated P calls H(P,P)
would seem to indicate infinite recursion because the currently running
H is being called again with identical parameters.

Flibble's comment caused me to accept the truth these words that I had previously written: (Before his comment I was not quite sure)

Because H knows that it is a simulating halt decider it can
know that the first time that its input calls itself with
the same parameters this would be infinitely nested simulation.

[Olcott wrong about infinite recursion] comp.theory
On 11/10/2021 3:53 PM, Mr Flibble wrote:

Olcott is barking up the wrong tree re infinite recursion: there
is only a need to detect a single recursive call into the halt decider
and signal an exception. Why? Because infinite recursion is valid
program behavior.

/Flibble

This halt deciding criteria can also be equally applied when P is
invoking H with a copy of its input. The only difference is that
string_compare is invoked instead of integer compare.

Because the call is aborted before the next level simulation is
initiated there is no need for static local data, thus this H is a pure function. https://en.wikipedia.org/wiki/Pure_function

H uses the NumParams system to provide the number of parameters required
by any function of the COFF object file. H finds that the NumParams("H")
is 2. H then compares the top two elements pf P's stack its own
parameters. If it has a match then its [abort and decide not halting]
criteria have been met.

There is no need to maintain any static data across nested simulations
because no nested simulation are ever created.




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