Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Mikko <mikko.levanto@iki.fi>
Newsgroups: comp.theory
Subject: Re: Proof that executed HH(DD,DD) and simulated HH(DD,DD) simulate DD correctly -- Mike Terry
Date: Fri, 7 Jun 2024 08:49:13 +0300
Organization: -
Lines: 280
Message-ID: <v3u70p$1usbl$1@dont-email.me>
References: <v3neft$game$1@dont-email.me> <v3nfc4$gatu$1@dont-email.me> <v3ngcu$gc4a$2@dont-email.me> <v3p5te$sr75$1@dont-email.me> <v3pqdr$1003g$1@dont-email.me> <v3rriu$1e603$1@dont-email.me> <v3sci6$1gra7$4@dont-email.me> <v3sied$1i3na$1@dont-email.me> <v3sj9e$1hufb$2@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Fri, 07 Jun 2024 07:49:14 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="6ffc97c8aed538b65f79c8ced6ee8603";
	logging-data="2060661"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18JhiZZz2E6juBv695ZyXcz"
User-Agent: Unison/2.2
Cancel-Lock: sha1:OC3mWO6JxITxQZUxFneun1gedxQ=
Bytes: 14517

On 2024-06-06 15:06:22 +0000, olcott said:

> On 6/6/2024 9:51 AM, Mikko wrote:
>> On 2024-06-06 13:11:34 +0000, olcott said:
>> 
>>> On 6/6/2024 3:21 AM, Mikko wrote:
>>>> On 2024-06-05 13:49:47 +0000, olcott said:
>>>> 
>>>>> On 6/5/2024 2:59 AM, Mikko wrote:
>>>>>> On 2024-06-04 16:46:21 +0000, Fred. Zwarts said:
>>>>>> 
>>>>>>> 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);
>>>>>>>         }
>>>>>> 
>>>>>> That program does not tell what H says. You should instead say
>>>>>> 
>>>>>> int main()
>>>>>> {
>>>>>>  return H(main, 0);
>>>>>> }
>>>>>> 
>>>>>> so that the result is returned to the operating systems. Many operating
>>>>>> systems tell the value returned by main or they can be asked about it.
>>>>>> 
>>>>> 
>>>>> *I was surprised that this worked correctly: here are the details*
>>>>> 
>>>>> int main()
>>>>> {
>>>>>    Output("Input_Halts = ", HH(main,(ptr)0));
>>>>> }
>>>>> 
>>>>>   machine   stack     stack     machine    assembly
>>>>>   address   address   data      code       language
>>>>>   ========  ========  ========  =========  =============
>>>>> [00001e42][00103375][00000000] 55         push ebp      ; begin main
>>>>> [00001e43][00103375][00000000] 8bec       mov ebp,esp
>>>>> [00001e45][00103371][00000000] 6a00       push +00
>>>>> [00001e47][0010336d][00001e42] 68421e0000 push 00001e42 ; push main
>>>>> [00001e4c][00103369][00001e51] e831f5ffff call 00001382 ; call HH
>>>>> New slave_stack at:103419
>>>>> 
>>>>> Begin Local Halt Decider Simulation   Execution Trace Stored at:113421
========== REMAINDER OF ARTICLE TRUNCATED ==========