Deutsch English Français Italiano |
<v3u70p$1usbl$1@dont-email.me> View for Bookmarking (what is this?) Look up another Usenet article |
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 ==========