• Airtight proof that H(P,P)==0 is correct

    From olcott@21:1/5 to All on Mon Aug 30 09:35:13 2021
    XPost: comp.theory, comp.software-eng, sci.logic

    My point is fully proven on the basis of two other points:
    (1) Verified as true entirely on the basis of the meaning of its words:
    A simulating halt decider correctly decides that any input that never
    halts unless the simulating halt decider aborts its simulation of this
    input is an input that never halts.

    (2) It can be verified that the input to H(P,P) never halts unless H
    aborts it. This is verified on the basis that the execution trace of P
    meets this criteria:

    where H = X() and P = Y()

    Infinite recursion detection criteria:
    If the execution trace of function X() called by function Y() shows:
    (a) Function X() is called twice in sequence from the same machine
    address of Y().
    (b) With the same parameters to X().
    (c) With no conditional branch or indexed jump instructions in Y().
    (d) With no function call returns from X().
    then the function call from Y() to X() is infinitely recursive.

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

    _main()
    [00000c56](01) 55 push ebp
    [00000c57](02) 8bec mov ebp,esp
    [00000c59](05) 68360c0000 push 00000c36 // push P
    [00000c5e](05) 68360c0000 push 00000c36 // push P
    [00000c63](05) e8fefcffff call 00000966 // call H(P,P)
    [00000c68](03) 83c408 add esp,+08
    [00000c6b](01) 50 push eax
    [00000c6c](05) 6857030000 push 00000357
    [00000c71](05) e810f7ffff call 00000386
    [00000c76](03) 83c408 add esp,+08
    [00000c79](02) 33c0 xor eax,eax
    [00000c7b](01) 5d pop ebp
    [00000c7c](01) c3 ret
    Size in bytes:(0039) [00000c7c]

    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)

    [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)
    Local Halt Decider: Infinite Recursion Detected Simulation Stopped

    Infinite recursion detection criteria:
    (a) P calls H twice in sequence from the same machine address.
    (b) with the same parameters (P,P) to H.
    (c) With no conditional branch or indexed jump instructions in the
    execution trace of P.
    (d) We know that there are no return instructions in H because we know
    that H is in pure simulation mode.

    This conclusively proves that P never halts unless H aborts its
    simulation of P:

    [00000c68][0010172a][00000000] 83c408 add esp,+08 [00000c6b][00101726][00000000] 50 push eax [00000c6c][00101722][00000357] 6857030000 push 00000357 [00000c71][00101722][00000357] e810f7ffff call 00000386
    Input_Halts = 0
    [00000c76][0010172a][00000000] 83c408 add esp,+08 [00000c79][0010172a][00000000] 33c0 xor eax,eax [00000c7b][0010172e][00100000] 5d pop ebp [00000c7c][00101732][00000068] c3 ret
    Number_of_User_Instructions(27)
    Number of Instructions Executed(23721)

    I will not tolerate changing the subject away from:
    (a) How we know (1) is true.
    (b) How we know (2) is true.
    (c) How we know (1) and (2) entails H(P,P)==0 is correct

    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 All on Mon Aug 30 12:15:38 2021
    XPost: comp.theory, comp.software-eng, sci.logic

    On 8/30/2021 11:25 AM, André G. Isaak wrote:
    On 2021-08-30 08:35, olcott wrote:
    My point is fully proven on the basis of two other points:
    (1) Verified as true entirely on the basis of the meaning of its words:

    Claiming that something is 'verified as true entirely on the basis of
    the meaning of its words' isn't a valid substitute for a proof.


    That all cats are animals and all animals are living things is a
    perfectly sound deductive proof that all cats are living things.

    That you fail to comprehend that proofs can be entirely based on the
    meaning of words is merely your error based on an incorrectly narrow
    minded focus.

    A simulating halt decider correctly decides that any input that never
    halts unless the simulating halt decider aborts its simulation of this
    input is an input that never halts.

    (2) It can be verified that the input to H(P,P) never halts unless H
    aborts it. This is verified on the basis that the execution trace of P
    meets this criteria:

    where H = X() and P = Y()

    Infinite recursion detection criteria:
    If the execution trace of function X() called by function Y() shows:
    (a) Function X() is called twice in sequence from the same machine
    address of Y().
    (b) With the same parameters to X().
    (c) With no conditional branch or indexed jump instructions in Y().
    (d) With no function call returns from X().
    then the function call from Y() to X() is infinitely recursive.

    First off, you simply state the above criteria without actually offering
    any *proof* that these criteria actually work.


    They above criteria have been extensively reviewed and critiqued,
    none-the-less for the point at hand it is quite obvious to every honest
    person that has a sufficient understanding of x86 assembly language that
    the simulation of P on input P by H never halts while H is in pure
    simulation mode.

    And second, even if these criteria are valid, your trace *doesn't*
    actually meet these criteria because you deliberately omit portions of
    the code from your trace (i.e. everything that happens starting at
    address 966).


    This is explained on pages 3-4 of my updated paper. That people continue
    to ignore sound reasoning is no actual rebuttal at all.

    https://www.researchgate.net/publication/351947980_Halting_problem_undecidability_and_infinitely_nested_simulation

    The claim that 'it can be verified that the input to H(P, P) never halts unless H aborts it.' Is not verified at all, since it can easily shown
    to be false by simply observing the fact that P(P) does, in fact, halt.


    Yet again you twist my words. This is the straw-man error. See pages 3-4
    of my paper.

    You try to get around this by claiming that when you call H(P, P) the
    input magically changes to some *other* computation which isn't
    equivalent to P(P) and that this *other* computation is non-halting, but
    even if such a claim made sense, it means your H is answering about the *wrong* computation.


    int main() { P(P); } will not be discussed on this thread.
    I will no longer tolerate dishonest dodges away from the the point.

    And from your recent posts in a different thread, it appears you are
    also claiming that it is not possible to even ask your H about the real
    P(P), which is the case we're really concerned about.


    int main() { P(P); } will not be discussed on this thread.
    I will no longer tolerate dishonest dodges away from the the point.

    If your H can't even be asked about the real P(P), then it isn't even answering the question a halt decider is supposed to answer. So what's
    the point of your H?

    André


    The only thing that will be discussed on this thread is the
    [Airtight proof that H(P,P)==0 is correct] on the basis that (1) and (2)
    are true. Everything else will be construed as a dishonest dodge.

    (1) Verified as true entirely on the basis of the meaning of its words:
    A simulating halt decider correctly decides that any input that never
    halts unless the simulating halt decider aborts its simulation of this
    input is an input that never halts.

    (2) It can be verified that the input to H(P,P) never halts unless H
    aborts it. This is verified on the basis that the execution trace of P
    meets this criteria:

    --
    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 Mon Aug 30 21:45:53 2021
    XPost: comp.theory, comp.software-eng, sci.logic

    On 8/30/2021 9:29 PM, Ben Bacarisse wrote:
    olcott <NoOne@NoWhere.com> writes:

    On 8/30/2021 11:01 AM, Malcolm McLean wrote:
    On Monday, 30 August 2021 at 15:35:22 UTC+1, olcott wrote:
    My point is fully proven on the basis of two other points:
    (1) Verified as true entirely on the basis of the meaning of its words: >>>> A simulating halt decider correctly decides that any input that never
    halts unless the simulating halt decider aborts its simulation of this >>>> input is an input that never halts.

    (2) It can be verified that the input to H(P,P) never halts unless H
    aborts it. This is verified on the basis that the execution trace of P >>>> meets this criteria:

    The sounds reasonable. But there are two Hes. The halt decider, and the
    copy of H in H_Hat. In your set up, these are physically the same piece
    of machine code. That isn't fatal. But it does mean that we have to be
    careful about what we mean by "unless H aborts it".
    If we ran UTM<H_Hat><H_Hat> insread of H<H_Hat><H_Hat> what would
    happen?

    He won't answer that! Not because he does not know the answer but
    because he does.


    Ĥ applied to ⟨Ĥ⟩ is
    exactly analogous to int main() { P((u32)P); }

    Ĥ.qx applied to ⟨Ĥ⟩ ⟨Ĥ⟩ is exactly analogous to
    H(P,P) called from main() { P((u32)P); }

    When we know that { H(P,P)==0 is correct } is a necessary consequence of
    its two premises and we know that its two premises are true then
    {H(P,P)==0 is correct} is true by logical necessity.

    Everything besides:
    (a) The logical necessity relationship between {H(P,P)==0 is correct}
    and its two premises.

    (b) The truth of these two premises

    is totally 100% perfectly and utterly irrelevant to the truth of:
    {H(P,P)==0 is correct}.

    I am not referring to H_Hat any more. H/P is much more concise and
    mathematical.

    Translation: "I get burned every time I talk about Turing machines so
    I'll stick with some C code and a function I won't publish".



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