• Re: Proof that H(D,D) meets its abort criteria --philosophical foundati

    From immibis@21:1/5 to olcott on Sun Mar 17 02:13:42 2024
    On 17/03/24 01:41, olcott wrote:
    On 3/16/2024 7:23 PM, immibis wrote:
    On 16/03/24 23:47, olcott wrote:
    On 3/16/2024 5:03 PM, immibis wrote:
    On 16/03/24 00:37, Mike Terry wrote:
    On 15/03/2024 18:45, immibis wrote:
    On 15/03/24 19:39, olcott wrote:
    On 3/15/2024 1:38 PM, immibis wrote:
    On 15/03/24 18:52, olcott wrote:
    On 3/15/2024 12:36 PM, Richard Damon wrote:
    On 3/15/24 9:20 AM, olcott wrote:
    Best selling author of Theory of Computation textbooks:
    *Introduction To The Theory Of Computation 3RD, by sipser* >>>>>>>>>>> https://www.amazon.com/Introduction-Theory-Computation-Sipser/dp/8131525295/

    Date 10/13/2022 11:29:23 AM
    *MIT Professor Michael Sipser agreed this verbatim paragraph >>>>>>>>>>> is correct*
    (He has neither reviewed nor agreed to anything else in this >>>>>>>>>>> paper)
    (a) If simulating halt decider H correctly simulates its >>>>>>>>>>> input D until H correctly determines that its simulated D >>>>>>>>>>> would never stop running unless aborted then
    (b) H can abort its simulation of D and correctly report that >>>>>>>>>>> D specifies a non-halting sequence of configurations.

    *When we apply the abort criteria* (elaborated above)
    Will you halt if you never abort your simulation?
    *Then H(D,D) is proven to meet this criteria*

    *Proof that H(D,D) meets its abort criteria*

    int D(int (*x)())
    {
       int Halt_Status = H(x, x);
       if (Halt_Status)
         HERE: goto HERE;
       return Halt_Status;
    }

    int main()
    {
       Output("Input_Halts = ", H(D,D));
    }

      machine   stack     stack     machine    assembly >>>>>>>>>>>   address   address   data      code       language
      ========  ========  ========  =========  ============= >>>>>>>>>>> [00001d22][00102fc9][00000000] 55         push ebp      ;
    begin main()
    [00001d23][00102fc9][00000000] 8bec       mov ebp,esp >>>>>>>>>>> [00001d25][00102fc5][00001cf2] 68f21c0000 push 00001cf2 ; >>>>>>>>>>> push DD
    [00001d2a][00102fc1][00001cf2] 68f21c0000 push 00001cf2 ; push D >>>>>>>>>>> [00001d2f][00102fbd][00001d34] e8eef7ffff call 00001522 ; >>>>>>>>>>> call H(D,D)

    H: Begin Simulation   Execution Trace Stored at:113075 >>>>>>>>>>> Address_of_H:1522
    [00001cf2][00113061][00113065] 55         push ebp       ;
    enter D(D)
    [00001cf3][00113061][00113065] 8bec       mov ebp,esp >>>>>>>>>>> [00001cf5][0011305d][00103031] 51         push ecx >>>>>>>>>>> [00001cf6][0011305d][00103031] 8b4508     mov eax,[ebp+08] >>>>>>>>>>> [00001cf9][00113059][00001cf2] 50         push eax       ;
    push D
    [00001cfa][00113059][00001cf2] 8b4d08     mov ecx,[ebp+08] >>>>>>>>>>> [00001cfd][00113055][00001cf2] 51         push ecx       ;
    push D
    [00001cfe][00113051][00001d03] e81ff8ffff call 00001522  ; >>>>>>>>>>> call H(D,D)
    H: Recursive Simulation Detected Simulation Stopped
                               H(D,D) returns 0 to main()

    *That was proof that H(D,D) meets its abort criteria*
    H(D,D) correctly determines that itself is being called with >>>>>>>>>>> its same inputs and there are no conditional branch
    instructions between the invocation of D(D) and its call to >>>>>>>>>>> H(D,D).



    Except that D calling H(D,D) does NOT prove the required (a), >>>>>>>>>> since the simulated D WILL stop running because *ITS* H will >>>>>>>>>> abort *ITS* simulation and returm 0 so that simulated D will >>>>>>>>>> halt.
    You keep saying that H(D,D) never really needs to abort the
    simulation of its input because after H(D,D) has aborted the >>>>>>>>> simulation of this input it no longer needs to be aborted.

    You keep thinking there is more than one H(D,D) and then when
    it's convenient for you you think there is only one H(D,D). Why >>>>>>>> is that?

    The first H(D,D) to see that the abort criteria has been met
    (the outermost one) must abort the simulation of its input or
    none of them ever abort.


    that's wrong. They all abort, so if we prevent the first one from
    aborting, the second one will abort. If we prevent the first and
    second ones from aborting, the third one will abort.

    Correct - but PO has the wrong understanding of "prevent".

    Correct understanding:  We're discussing a (putative) HD H
    examining an input (P,I) representing some /fixed/ computation.
    When we talk about "preventing" H from doing xxxxx (such as
    aborting a simulation) we mean how an amended version H2 (like H
    but without xxxxx) behaves in examining that /same input/ (P,I).

    PO understanding:  When PO reads "prevent H from doing xxxxx" he
    thinks we change the C code of H to H' (which /in PO's x86utm/
    system entails also changing D to D'), and then restart everything
    so we are looking at H' deciding (D',D') - a totally different
    input.  He then notes that D'(D') doesn't halt, so concludes
    (outer) H is right to decide non-halting on the ground that D'(D')
    runs forever. Same PO thinking applies to all his duffer
    "conditionals" in his phrases like "what H /would/ do...", and
    "halts /only/ because...".

    Things that reinforce PO's wrong thinking:
    -  His x86utm.exe design confuses the distinction between code and
    data.
        H and D are both CODE (like TMs) when called from main(), but >>>>> when passed as
        parameters to H or D, and when simulated, they are logically DATA. >>>>>     Perhaps if PO had designed x86utm "properly" and not confused >>>>> these notions
        in his x86utm design, he would have realised that discussing
    alternative H
        behaviours was purely a CODE matter, and the input (P,I), being >>>>> DATA, does not
        magically change as a result of any H coding change...
    -  Since PO does not physically embed H logic into C function D() , >>>>> and instead just
        calls H, PO probably fails to consider that changing H is also >>>>> changing D.  Also
        the fact that as parameters in halt7.c they appear just as "H" >>>>> and "D" obscuring the
        fact that D is not just the code in D but also includes all the >>>>> H code.

    With PO's choices for x86utm design, we can't just simply evaluate
    PO's duffer conditionals by updating H, recompiling and rerunning
    [since that would be changing code AND INPUT DATA].  A couple of
    ways to do it "properly" within PO's current design:
    -  keep H and D unchanged, but implement the updated H as H2.  Then >>>>> we can examine H2(D,D),
        while the input (D,D) being examined is not changed.  As with >>>>> PO's H1(D,D), H2 will see
        the simulated D(D) terminate.
    -  Examine H(D,D) (no code changes) but under a debugger.  When
    [outer] H goes to abort,
        use the debugger to jump H over the abort and let things continue. >>>>>     That's a bit fiddly, as the program being debugged is x86utm, >>>>> not H, but I gave it a
        go to settle this argument once and for all.  :)  As we all >>>>> would expect,
        H goes on to examine the full D(D) simulation instead of
    aborting, AND OBSERVES
        THAT D(D) HALTS.
        So now it's confirmed!  What H "would" do if it didn't abort >>>>> its simulation of D(D)
        is "continue simulating until it see D(D) halt".  So H has not >>>>> "correctly seen
        that its input would not halt unless aborted".  (PO won't
    understand though.)


    Mike.


    It's a shame that Olcott didn't read your fantastic response beyond
    the part where you said he was wrong.

    *The rest of his post is anchored in this counter-factual assumption*

    On 3/15/2024 6:37 PM, Mike Terry wrote:
    On 15/03/2024 18:45, immibis wrote:>> that's wrong. They all
    abort, so if we prevent the first one from
    aborting, the second one will abort. If we prevent the first and
    second ones from aborting, the third one will abort.
    ;
    Correct - but PO has the wrong understanding of "prevent".

    *This is self-evidently true to all those that understand it*
    There cannot possibly exist any H(D,D) that is called by
    D where H(D,D) simulates its input and D(D) stops running
    and H never aborts its simulation.

    It proves that even if my idea of "prevent" may be different than
    Mike's that mine is not incorrect.

    The computer science notion of the term "prevent" seems to have
    (damned if you do and damned if you don't) pathology in its system
    of reasoning. H(D,D) is wrong to abort and wrong to not abort
    its simulation.

    The software engineering notion of the term "prevent" does not
    have this same pathology. There are two sets of possible behaviors
    by H(D,D) one aborts its simulation and D(D) stops running and the
    other does not abort its simulation and D(D) never stops running.


    So, as I said, it's a shame you didn't read it beyond the part where
    he said you were wrong.

    I did and he simply carried on with the same different frame-of-
    reference that never actually refutes what I am saying.

    One could construe that everything that H(D,D) can possibly do
    regarding abort criteria is necessarily incorrect when one does
    this from a pathological frame-of-reference.

    I say that this pathological frame-of-reference is incorrect
    at the level of its philosophical foundations.


    You obviously either didn't read any of it or didn't understand any of it.

    --- SoupGate-Win32 v1.05
    * Origin: fsxNet Usenet Gateway (21:1/5)