Re: Proof that H(D,D) meets its abort criteria --Categorically Exhaustive Reasoning--

On 3/15/2024 6:37 PM, Mike Terry wrote:

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

 *It can be construed that way, yet that is not it*

 

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