• Concise refutation of halting problem proofs V6 [ pure function ]

    From olcott@21:1/5 to Mr Flibble on Wed Nov 10 19:25:18 2021
    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)