Path: ...!news.mixmin.net!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: "Fred. Zwarts" <F.Zwarts@HetNet.nl>
Newsgroups: comp.theory,sci.logic
Subject: Re: Proof that executed HH(DD,DD) and simulated HH(DD,DD) simulate DD
 correctly -- Mike Terry
Date: Tue, 4 Jun 2024 18:46:21 +0200
Organization: A noiseless patient Spider
Lines: 155
Message-ID: <v3ngcu$gc4a$2@dont-email.me>
References: <v3neft$game$1@dont-email.me> <v3nfc4$gatu$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Tue, 04 Jun 2024 18:46:23 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="582df39bb1a7d9f05afabcda0481a71a";
	logging-data="536714"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+Unyx6eXICeSEJml8NRiWN"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:zK7v8uxHVdUbxn0Z8DwhL077RlU=
In-Reply-To: <v3nfc4$gatu$1@dont-email.me>
Content-Language: en-GB
Bytes: 7984

Op 04.jun.2024 om 18:28 schreef olcott:
> Heh Mike Terry, please study this to see your mistaken
> conclusion of this post:
> 
> On 5/30/2024 3:51 PM, Mike Terry wrote:
>  > On 30/05/2024 17:55, olcott wrote:
> http://al.howardknight.net/?STYPE=msgid&MSGI=%3CS8CcnRadHexfe8X7nZ2dnZfqnPqdnZ2d%40brightview.co.uk%3E+
> Message-ID: <S8CcnRadHexfe8X7nZ2dnZfqnPqdnZ2d@brightview.co.uk>
> 
> *Here is your mistaken conclusion*
> On 5/30/2024 3:51 PM, Mike Terry wrote:
>  > On 30/05/2024 17:55, olcott wrote:
>  >> That HH is not a pure function does not show that
>  >> the simulation is incorrect because:
>  >
>  > It shows that the simulation is "rubbish" and any
>  > trace produced by it can just be ignored.
>  >
>  > Err, that's it.
>  >
>  > Mike.
> 
> Proof that executed HH(DD,DD) and simulated HH(DD,DD) simulate DD
> correctly. This proof requires expert knowledge of the C programming
> language and the x86 programming language.
> 
> With this expertise it is easy to confirm that both the directly
> executed HH(DD,DD) and the simulated executed HH(DD,DD) simulate the
> steps of DD exactly the way that the x86 machine language specifies.
> 
> *New Paragraph inserted*
> We can see that the pair of execution traces derived by the executed
> HH(DD,DD) and the simulated HH(DD,DD) (shown below) exactly match
> the x86 machine code of DD, (also shown below) thus are proven to be
> correct.
> 
> If one also has expertise on the mapping from the C source code to the
> x86 assembly language then one also confirms that the x86 version of
> DD is exactly what the C source-code specifies.
> 
> 01   int DD(int (*x)())
> 02   {
> 03     int Halt_Status = HH(x, x);
> 04     if (Halt_Status)
> 05         HERE: goto HERE;
> 06     return Halt_Status;
> 07   }
> 08
> 09   int main()
> 10   {
> 11     Output("Input_Halts = ", HH(DD,DD));
> 12   }
> 
> _DD()
> [00001db2] 55         push ebp
> [00001db3] 8bec       mov ebp,esp
> [00001db5] 51         push ecx
> [00001db6] 8b4508     mov eax,[ebp+08]
> [00001db9] 50         push eax        ; push DD
> [00001dba] 8b4d08     mov ecx,[ebp+08]
> [00001dbd] 51         push ecx        ; push DD
> [00001dbe] e8bff5ffff call 00001382   ; call HH
> [00001dc3] 83c408     add esp,+08
> [00001dc6] 8945fc     mov [ebp-04],eax
> [00001dc9] 837dfc00   cmp dword [ebp-04],+00
> [00001dcd] 7402       jz 00001dd1
> [00001dcf] ebfe       jmp 00001dcf
> [00001dd1] 8b45fc     mov eax,[ebp-04]
> [00001dd4] 8be5       mov esp,ebp
> [00001dd6] 5d         pop ebp
> [00001dd7] c3         ret
> Size in bytes:(0038) [00001dd7]
> 
>   machine   stack     stack     machine    assembly
>   address   address   data      code       language
>   ========  ========  ========  =========  =============
> [00001de2][00103292][00000000] 55         push ebp
> [00001de3][00103292][00000000] 8bec       mov ebp,esp
> [00001de5][0010328e][00001db2] 68b21d0000 push 00001db2 ; push DD
> [00001dea][0010328a][00001db2] 68b21d0000 push 00001db2 ; push DD
> [00001def][00103286][00001df4] e88ef5ffff call 00001382 ; call HH
> New slave_stack at:103336
> 
> Begin Local Halt Decider Simulation   Execution Trace Stored at:11333e
> [00001db2][0011332a][0011332e] 55         push ebp         ; DD line 01
> [00001db3][0011332a][0011332e] 8bec       mov ebp,esp      ; DD line 02
> [00001db5][00113326][001032fa] 51         push ecx         ; DD line 03
> [00001db6][00113326][001032fa] 8b4508     mov eax,[ebp+08] ; DD line 04
> [00001db9][00113322][00001db2] 50         push eax         ; push DD
> [00001dba][00113322][00001db2] 8b4d08     mov ecx,[ebp+08] ; DD line 06
> [00001dbd][0011331e][00001db2] 51         push ecx         ; push DD
> [00001dbe][0011331a][00001dc3] e8bff5ffff call 00001382    ; call HH
> New slave_stack at:14dd5e
> [00001db2][0015dd52][0015dd56] 55         push ebp         ; DD line 01
> [00001db3][0015dd52][0015dd56] 8bec       mov ebp,esp      ; DD line 02
> [00001db5][0015dd4e][0014dd22] 51         push ecx         ; DD line 03
> [00001db6][0015dd4e][0014dd22] 8b4508     mov eax,[ebp+08] ; DD line 04
> [00001db9][0015dd4a][00001db2] 50         push eax         ; push DD
> [00001dba][0015dd4a][00001db2] 8b4d08     mov ecx,[ebp+08] ; DD line 06
> [00001dbd][0015dd46][00001db2] 51         push ecx         ; push DD
> [00001dbe][0015dd42][00001dc3] e8bff5ffff call 00001382    ; call HH
> Local Halt Decider: Infinite Recursion Detected Simulation Stopped
> 
> [00001df4][00103292][00000000] 83c408     add esp,+08
> [00001df7][0010328e][00000000] 50         push eax
> [00001df8][0010328a][00000743] 6843070000 push 00000743
> [00001dfd][0010328a][00000743] e8a0e9ffff call 000007a2
> Input_Halts = 0
> [00001e02][00103292][00000000] 83c408     add esp,+08
> [00001e05][00103292][00000000] eb79       jmp 00001e80
> [00001e80][00103292][00000000] 33c0       xor eax,eax
> [00001e82][00103296][00000018] 5d         pop ebp
> [00001e83][0010329a][00000000] c3         ret
> Number of Instructions Executed(16829) == 251 Pages
> 

This is a perfect example of a false negative. It is explained by the 
following:

Olcott defends a simulating halt decider H. The problem with it is, that 
it introduces another halting problem: The H itself does not halt when 
simulated by itself. This causes false negatives: many functions are now 
diagnosed by H to be non-halting only by the mere fact that they call H, 
even if their direct execution does halt.

We see in olcott's example above that the simulation of H invokes a 
recursive simulation of H.

H even diagnoses itself to be non-halting, which is illustrated in the 
following example (where the D that contradicts H is eliminated):

        typedef int (*ptr)();  // ptr is pointer to int function in C

        int H(ptr p, ptr i);

        int main()
        {
          H(main, 0);
        }

The program main does nothing but calling H. H is required to halt, so 
main itself should also halt. Nevertheless H reports that main does not 
halt.

Of the infinite set of H that simulate at least one step, none of them, 
when simulated by H, reaches its final state. So, it follows that H 
determines non-halting behaviour of H.

This illustrates that a simulating halt-decider is a bad idea, because 
the decider itself does not halt when simulated by itself and therefore 
its results are often false negatives.