*This is the outline of the complete refutation*
*of the only rebuttal that anyone has left*
(a) The complete and correct x86 emulation of the input to H(P,P) by H
never reaches the "ret" instruction of P.
(b) The direct execution of P(P) does reach its "ret" instruction.
The above two are proven to be verified facts entirely on the basis of
the semantics of the x86 language.
A halt decider must compute the mapping from its inputs to an accept or
reject state on the basis of the actual behavior that is actually
specified by these inputs.
P(P) is provably not the actual behavior of the actual input.
void P(u32 x)
{
if (H(x, x))
HERE: goto HERE;
return;
}
int main()
{
Output("Input_Halts = ", H1((u32)P, (u32)P));
}
_P()
[0000163a](01) 55 push ebp
[0000163b](02) 8bec mov ebp,esp
[0000163d](03) 8b4508 mov eax,[ebp+08]
[00001640](01) 50 push eax
[00001641](03) 8b4d08 mov ecx,[ebp+08]
[00001644](01) 51 push ecx
[00001645](05) e8f0fdffff call 0000143a // call H
[0000164a](03) 83c408 add esp,+08
[0000164d](02) 85c0 test eax,eax
[0000164f](02) 7402 jz 00001653
[00001651](02) ebfe jmp 00001651
[00001653](01) 5d pop ebp
[00001654](01) c3 ret
Size in bytes:(0027) [00001654]
_main()
[0000165a](01) 55 push ebp
[0000165b](02) 8bec mov ebp,esp
[0000165d](05) 683a160000 push 0000163a // push P
[00001662](05) 683a160000 push 0000163a // push P
[00001667](05) e8cef9ffff call 0000103a // call H1
[0000166c](03) 83c408 add esp,+08
[0000166f](01) 50 push eax // push return value
[00001670](05) 689b040000 push 0000049b // "Input_Halts = "
[00001675](05) e870eeffff call 000004ea // call Output
[0000167a](03) 83c408 add esp,+08
[0000167d](02) 33c0 xor eax,eax
[0000167f](01) 5d pop ebp
[00001680](01) c3 ret
Size in bytes:(0039) [00001680]
machine stack stack machine assembly
address address data code language
======== ======== ======== ========= =============
[0000165a][001026a9][00000000] 55 push ebp
[0000165b][001026a9][00000000] 8bec mov ebp,esp
[0000165d][001026a5][0000163a] 683a160000 push 0000163a // push P
[00001662][001026a1][0000163a] 683a160000 push 0000163a // push P
[00001667][0010269d][0000166c] e8cef9ffff call 0000103a // call H1
H1: Begin Simulation Execution Trace Stored at:21275d
Address_of_H1:103a
[0000163a][00212749][0021274d] 55 push ebp
[0000163b][00212749][0021274d] 8bec mov ebp,esp
[0000163d][00212749][0021274d] 8b4508 mov eax,[ebp+08]
[00001640][00212745][0000163a] 50 push eax // push P
[00001641][00212745][0000163a] 8b4d08 mov ecx,[ebp+08]
[00001644][00212741][0000163a] 51 push ecx // push P
[00001645][0021273d][0000164a] e8f0fdffff call 0000143a // call H
H: Begin Simulation Execution Trace Stored at:2285c5
Address_of_H:143a
[0000163a][002285b1][002285b5] 55 push ebp
[0000163b][002285b1][002285b5] 8bec mov ebp,esp
[0000163d][002285b1][002285b5] 8b4508 mov eax,[ebp+08]
[00001640][002285ad][0000163a] 50 push eax // push P
[00001641][002285ad][0000163a] 8b4d08 mov ecx,[ebp+08]
[00001644][002285a9][0000163a] 51 push ecx // push P
[00001645][002285a5][0000164a] e8f0fdffff call 0000143a // call H
H: Infinitely Recursive Simulation Detected Simulation Stopped
[0000164a][00212749][0021274d] 83c408 add esp,+08
[0000164d][00212749][0021274d] 85c0 test eax,eax
[0000164f][00212749][0021274d] 7402 jz 00001653
[00001653][0021274d][0000111e] 5d pop ebp
[00001654][00212751][0000163a] c3 ret
H1: End Simulation Input Terminated Normally
[0000166c][001026a9][00000000] 83c408 add esp,+08
[0000166f][001026a5][00000001] 50 push eax // return value
[00001670][001026a1][0000049b] 689b040000 push 0000049b // "Input_Halts = "
[00001675][001026a1][0000049b] e870eeffff call 000004ea // call Output
Input_Halts = 1
[0000167a][001026a9][00000000] 83c408 add esp,+08
[0000167d][001026a9][00000000] 33c0 xor eax,eax
[0000167f][001026ad][00100000] 5d pop ebp
[00001680][001026b1][00000004] c3 ret
Number of Instructions Executed(409590) == 6113 Pages