Liste des Groupes | Revenir à theory |
On 2024-06-06 13:11:34 +0000, olcott said:<Professor Sipser agreed>
On 6/6/2024 3:21 AM, Mikko wrote:That is no reason to say anything obviously false. If somethingOn 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
[00001e42][0011340d][00113411] 55 push ebp ; begin main
[00001e43][0011340d][00113411] 8bec mov ebp,esp
[00001e45][00113409][00000000] 6a00 push +00
[00001e47][00113405][00001e42] 68421e0000 push 00001e42 ; push main
[00001e4c][00113401][00001e51] e831f5ffff call 00001382 ; call HH
New slave_stack at:14de41
[00001e42][0015de35][0015de39] 55 push ebp ; begin main
[00001e43][0015de35][0015de39] 8bec mov ebp,esp
[00001e45][0015de31][00000000] 6a00 push +00
[00001e47][0015de2d][00001e42] 68421e0000 push 00001e42 ; push main
[00001e4c][0015de29][00001e51] e831f5ffff call 00001382 ; call HH
Local Halt Decider: Infinite Recursion Detected Simulation Stopped
>
[00001e51][00103375][00000000] 83c408 add esp,+08
[00001e54][00103371][00000000] 50 push eax
[00001e55][0010336d][00000743] 6843070000 push 00000743
[00001e5a][0010336d][00000743] e843e9ffff call 000007a2
Input_Halts = 0
[00001e5f][00103375][00000000] 83c408 add esp,+08
[00001e62][00103375][00000000] eb79 jmp 00001edd
[00001edd][00103375][00000000] 33c0 xor eax,eax
[00001edf][00103379][00000018] 5d pop ebp
[00001ee0][0010337d][00000000] c3 ret ; end main
Number of Instructions Executed(12311) == 184 Pages
>
So main() does halt at its final state at [00001ee0] which proves
that the directly executed HH(main,(ptr)0) called by main() halts
and returns 0;
No, it only proves that HH halts. What it returns requires a different
proof.
>
Your example was too difficult for you to correctly understand.
Here is a simpler example.
is too difficult then you may point out the difficult part and
ask what it means. Parhaps there is just some presentational
problems but some things really are difficult to understand. Most
things discussed here are not very difficult but sometines poorly
presented.
*THE MOST IMPORTANT ASPECT OF MY PROOF*If it is important you must carfully cehck that it is presented
*THE MOST IMPORTANT ASPECT OF MY PROOF*
*THE MOST IMPORTANT ASPECT OF MY PROOF*
>
Try any show how this DD can be correctly simulated by any HH
such that this DD reaches past its machine address [00001dbe]
>
_DD()
[00001e12] 55 push ebp
[00001e13] 8bec mov ebp,esp
[00001e15] 51 push ecx
[00001e16] 8b4508 mov eax,[ebp+08]
[00001e19] 50 push eax ; push DD
[00001e1a] 8b4d08 mov ecx,[ebp+08]
[00001e1d] 51 push ecx ; push DD
[00001e1e] e85ff5ffff call 00001382 ; call HH
>
*Mike Terry would admit it if he would pay attention*
*He is not a liar*
>
*This unequivocally proves the behavior of DD correctly simulated by HH*
https://liarparadox.org/DD_correctly_simulated_by_HH_is_Proven.pdf
so that what is understood is what you want say.
Les messages affichés proviennent d'usenet.