Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail From: "Fred. Zwarts" Newsgroups: comp.theory,sci.logic Subject: Re: Proof that executed HH(DD,DD) and simulated HH(DD,DD) simulate DD correctly Date: Tue, 4 Jun 2024 18:23:15 +0200 Organization: A noiseless patient Spider Lines: 123 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Injection-Date: Tue, 04 Jun 2024 18:23:17 +0200 (CEST) Injection-Info: dont-email.me; posting-host="582df39bb1a7d9f05afabcda0481a71a"; logging-data="536714"; mail-complaints-to="abuse@eternal-september.org"; posting-account="U2FsdGVkX1/ZtKXYW24Hp2i8JqxUqQRr" User-Agent: Mozilla Thunderbird Cancel-Lock: sha1:4cMxArZ1hRBhGUYTI1WsBIIy9HU= In-Reply-To: Content-Language: en-GB Bytes: 6776 Op 04.jun.2024 om 18:13 schreef olcott: > 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. > > 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 It is clearly a false negative. 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 cause 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. 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.