• Re: Complete proof that H(P,P)==0 is correct for every simulating halt

    From olcott@21:1/5 to Richard Damon on Thu Nov 4 10:19:48 2021
    XPost: comp.theory, sci.logic

    On 11/4/2021 5:59 AM, Richard Damon wrote:
    On 11/4/21 12:50 AM, olcott wrote:
    On 11/3/2021 6:21 PM, Ben Bacarisse wrote:
    olcott <NoOne@NoWhere.com> writes:

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

    But H(P,P) == 0 is not correct if P(P) halts and you have told us that
    both are the case (for the specific H you are touting).  That false is
    the wrong return for inputs that represent halting computations comes
    from the definition of the problem you claim to be addressing.


    I provided all of the details to prove that I am correct and you
    simply ignored and erased them. This is apparently because you
    realized that my proof is irrefutable thus realize any attempt at
    rebuttal could only seem foolish. Alternatively you are clueless about
    the x86 language.


    Except that you 'proof' is totally baseless since it is built on false assumptions.

    _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]

    Begin Local Halt Decider Simulation at Machine Address:c36

    machine stack stack machine assembly
    address address data code language
    ======== ======== ======== ========= ============= [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)

    [00000c36][0025c1f2][0025c1f6] 55 push ebp [00000c37][0025c1f2][0025c1f6] 8bec mov ebp,esp [00000c39][0025c1f2][0025c1f6] 8b4508 mov eax,[ebp+08] [00000c3c][0025c1ee][00000c36] 50 push eax // push P [00000c3d][0025c1ee][00000c36] 8b4d08 mov ecx,[ebp+08] [00000c40][0025c1ea][00000c36] 51 push ecx // push P [00000c41][0025c1e6][00000c46] e820fdffff call 00000966 // call H(P,P)

    Verified facts:
    (1) The above 14 simulated lines are a correct pure simulation of P(P)
    for every possible encoding of simulating halt decider H.

    (2) The above 14 simulated lines conclusively prove that the pure
    simulation of the input to H(P,P) would never reach its final state of
    c50 for every possible encoding of simulating halt decider H.

    (1) and (2) conclusively prove that H(P,P) meets this criteria:

    2021-11-03 Halt Deciding Criteria
    It is impossible for any halt decider to be incorrect when the correct
    pure simulation of its input never halts and it reports not halting.


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