Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail From: olcott Newsgroups: comp.theory Subject: Re: Proof that executed HH(DD,DD) and simulated HH(DD,DD) simulate DD correctly -- Mike Terry Date: Thu, 6 Jun 2024 08:11:34 -0500 Organization: A noiseless patient Spider Lines: 248 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Thu, 06 Jun 2024 15:11:35 +0200 (CEST) Injection-Info: dont-email.me; posting-host="4cb2a3366a4bdb85a28904f6e3988fec"; logging-data="1600839"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1+Vxmgyj/fP1T9XivdVUJS9" User-Agent: Mozilla Thunderbird Cancel-Lock: sha1:okF0ZgzVeH/7dPwxZvnZjn5skYs= Content-Language: en-US In-Reply-To: Bytes: 12286 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: >>>>> >>>>> *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 ========== REMAINDER OF ARTICLE TRUNCATED ==========