Ĥ.qx(⟨Ĥ⟩,⟨Ĥ⟩) == Ĥ.qn [ succinct ]

[olcott]

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