• Concise refutation of halting problem proofs

    From olcott@21:1/5 to All on Thu Nov 4 10:47:53 2021
    XPost: comp.theory, sci.logic, alt.philosophy

    This tiny little proof totally proves that the counter-examples of all
    of the conventional halting problem proofs do not prove that the halting problem cannot be solved.

    This is the simplest example of the classic halting problem input that
    "proves" that the halting problem cannot be solved. https://en.wikipedia.org/wiki/Halting_problem

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

    This is the assembly language of the above function after it has been translated by the Microsoft C compiler.

    _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 the
    input to H(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.




    Strachey, C 1965.  An impossible program The Computer Journal, Volume 7,
    Issue 4, January 1965, Page 313, https://doi.org/10.1093/comjnl/7.4.313

    Linz, Peter 1990. An Introduction to Formal Languages and Automata. Lexington/Toronto: D. C. Heath and Company. (318-320)

    Halting problem undecidability and infinitely nested simulation
    May 2021 PL Olcott

    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)
  • From olcott@21:1/5 to Ben Bacarisse on Sat Nov 6 07:21:40 2021
    XPost: comp.theory, sci.logic, sci.math

    On 11/5/2021 6:49 PM, Ben Bacarisse wrote:
    olcott <NoOne@NoWhere.com> writes:

    As soon as we verify that the correct pure simulation of the input to
    H(P,0) never reaches the last address of P at c50 we know that the
    input to H(P,P) never halts thus the correctly halt status of
    H(P,P)==0;

    But P(P) halts, so H(P,P) == 0 is the wrong result.

    When the correct pure simulation of the actual input to the halt decider
    never halts then the halt decider is necessarily correct when it reports
    that its input never halts.

    Disagreeing with a logical tautology is a break from reality.

    A correct pure simulation is not verified on the basis of any mere
    assumptions. As long as the first seven x86 instructions of the source
    code of P are executed in order and the seventh instruction causes this
    cycle to repeat then we know that H(P,P) performed a correct pure
    simulation of its input for the entire 14 steps of this simulation.

    Saying the the pure simulation is not correct on any other basis is a
    break from reality.

    If both P(P) halts and the input to H(P,P) never halts are established
    facts (and they are) then it must be the case that P(P) and H(P,P) are
    not computationally equivalent to each other.




    An H this is wrong
    about this key case is not interesting, unlike your H from Dec 2018:

    "Everyone has claimed that H on input pair (Ĥ, Ĥ) meeting the Linz specs
    does not exist. I now have a fully encoded pair of Turing Machines H / Ĥ
    proving them wrong."[1]

    Three years of progressively walking back that claim and you are left
    with some C function H that is wrong about H(Ĥ, Ĥ). No one thinks such
    an H does not exist. It's trivially obvious that an H that does /not/
    meet Linz's spec (for the (Ĥ, Ĥ) case) exists. They are ten-a-penny.

    [1] Message-ID: <JbydneYGrrpProjBnZ2dnUU7-X3NnZ2d@giganews.com>



    --
    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)
  • From olcott@21:1/5 to Malcolm McLean on Sat Nov 6 09:00:03 2021
    XPost: comp.theory, sci.logic, sci.math

    On 11/6/2021 7:53 AM, Malcolm McLean wrote:
    On Saturday, 6 November 2021 at 12:21:49 UTC, olcott wrote:
    On 11/5/2021 6:49 PM, Ben Bacarisse wrote:
    olcott <No...@NoWhere.com> writes:

    As soon as we verify that the correct pure simulation of the input to
    H(P,0) never reaches the last address of P at c50 we know that the
    input to H(P,P) never halts thus the correctly halt status of
    H(P,P)==0;

    But P(P) halts, so H(P,P) == 0 is the wrong result.
    When the correct pure simulation of the actual input to the halt decider
    never halts then the halt decider is necessarily correct when it reports
    that its input never halts.

    Disagreeing with a logical tautology is a break from reality.
    A correct pure simulation is not verified on the basis of any mere
    assumptions. As long as the first seven x86 instructions of the source
    code of P are executed in order and the seventh instruction causes this
    cycle to repeat then we know that H(P,P) performed a correct pure
    simulation of its input for the entire 14 steps of this simulation.

    The first seven steps are indeed simulated. But the next seven steps are simulated by the copy of H that is called from P.

    Conclusively proving that the correct pure simulation of the input to
    H(P,P) never halts, thus H(P,P)==0 is correct.

    So they shouldn't appear
    in the instruction trace. If we simulate "push ebp" we don't actually push ebp to the stack. We create a virtual stack in memory and push a value to
    it.




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