| Deutsch English Français Italiano |
|
<v3sci6$1gra7$4@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: olcott <polcott333@gmail.com>
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: <v3sci6$1gra7$4@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>
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: <v3rriu$1e603$1@dont-email.me>
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: <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
========== REMAINDER OF ARTICLE TRUNCATED ==========