XPost: comp.theory, comp.software-eng, sci.philosophy
On 8/1/2021 9:25 AM, Malcolm McLean wrote:
On Sunday, 1 August 2021 at 13:41:25 UTC+1, Ben Bacarisse wrote:
Malcolm McLean <malcolm.ar...@gmail.com> writes:
However the reasons PO's halt decider fails on H_Hat(H_Hat) have got
nothing to do with the invert step of Linz' proof. This is maybe interesting,
but in a small way, it's not a revolutionary result which will turn computer
science upside down. But it's maybe worth mentioning.
I don't follow. H_Hat(H_Hat) halts because H(H_Hat, H_Hat) == 0 making
that result the wrong one. If H(H_Hat, H_Hat) returned non-zero,
H_Hat(H_Hat) would not halt, making that the wrong result. Whilst I
don't like this sort of language, H fails on H_Hat(H_Hat) precisely
because of how H_Hat is constructed from H.
Consider this. H_Cap (similar to H_Hat but missing the invert step);
H_Cap(I)
{
return H(I, I):
}
Now if H is a "simulating halt decider" it must get this wrong. H is (skeleton
code)
H(I, I)
{
while(true)
{
Step(I, I);
if (tightloopdetected())
return Non_Halting;
else if (haltsofitsownaccord)
return Halting;
}
}
The question is how we write the function tightloopdetected(). If it returns true then H(H_Cap, H_Cap) the H(H_Cap, H_Cap) will terminate. If
it returns false, it wlll not. So H can never make the right decision for H_Cap(H_Cap).
Some errors were corrected and the rest was adapted to x86utm.
u32 HH(I, I)
{
HERE:
{
if (H(I, I) == 0)
return 0;
else
return 1;
}
goto HERE;
}
u32 H_Cap(I)
{
return HH(I, I);
}
int main()
{
Output("Input_Halts = ", H((u32)H_Cap, (u32)H_Cap));
}
Begin Local Halt Decider Simulation at Machine Address:d02 ...[00000d02][00211915][00211919] 55 push ebp ...[00000d03][00211915][00211919] 8bec mov ebp,esp ...[00000d05][00211915][00211919] 8b4508 mov eax,[ebp+08] ...[00000d08][00211911][00000d02] 50 push eax ...[00000d09][00211911][00000d02] 8b4d08 mov ecx,[ebp+08] ...[00000d0c][0021190d][00000d02] 51 push ecx ...[00000d0d][00211909][00000d12] e8c0ffffff call 00000cd2 ...[00000cd2][00211905][00211915] 55 push ebp ...[00000cd3][00211905][00211915] 8bec mov ebp,esp ...[00000cd5][00211905][00211915] 8b4508 mov eax,[ebp+08] ...[00000cd8][00211901][00000d02] 50 push eax ...[00000cd9][00211901][00000d02] 8b4d08 mov ecx,[ebp+08] ...[00000cdc][002118fd][00000d02] 51 push ecx ...[00000cdd][002118f9][00000ce2] e8e0fdffff call 00000ac2 ...[00000d02][0025c33d][0025c341] 55 push ebp ...[00000d03][0025c33d][0025c341] 8bec mov ebp,esp ...[00000d05][0025c33d][0025c341] 8b4508 mov eax,[ebp+08] ...[00000d08][0025c339][00000d02] 50 push eax ...[00000d09][0025c339][00000d02] 8b4d08 mov ecx,[ebp+08] ...[00000d0c][0025c335][00000d02] 51 push ecx ...[00000d0d][0025c331][00000d12] e8c0ffffff call 00000cd2
Local Halt Decider: Infinite Recursion Detected Simulation Stopped
Input_Halts = 0
Proving that the above code is decided correctly.
We've elimiated the "invert the result" step from Linz's proof. We have to insist that H is a "simulating halt decider" to achieve this. But that seems to be a reasonable condition. We know there are many properties of Turing machines that cannot be determined other than by stepping them.
--
Copyright 2021 Pete Olcott
"Great spirits have always encountered violent opposition from mediocre
minds." Einstein
--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)