// Simplified Linz Ĥ (Linz:1990:319)
// Strachey(1965) CPL translated to C
void P(u32 x)
{ if (H(x, x))
HERE: goto HERE;
}

_P()
[00000c36](01) 55 push ebp
[00000c37](02) 8bec mov ebp,esp
[00000c39](03) 8b4508 mov eax,[ebp+08] // 2nd Param
[00000c3c](01) 50 push eax
[00000c3d](03) 8b4d08 mov ecx,[ebp+08] // 1st Param
[00000c40](01) 51 push ecx
[00000c41](05) e820fdffff call 00000966 // call H
[00000c46](03) 83c408 add esp,+08
[00000c49](02) 85c0 test eax,eax
[00000c4b](02) 7402 jz 00000c4f
[00000c4d](02) ebfe jmp 00000c4d
[00000c4f](01) 5d pop ebp
[00000c50](01) c3 ret
Size in bytes:(0027) [00000c50]

Begin Local Halt Decider Simulation at Machine Address:c36

machine stack stack machine assembly
address address data code language
======== ======== ======== ========= =============
[00000c36][002117ca][002117ce] 55 push ebp
[00000c37][002117ca][002117ce] 8bec mov ebp,esp
[00000c39][002117ca][002117ce] 8b4508 mov eax,[ebp+08]
[00000c3c][002117c6][00000c36] 50 push eax // push P
[00000c3d][002117c6][00000c36] 8b4d08 mov ecx,[ebp+08]
[00000c40][002117c2][00000c36] 51 push ecx // push P
[00000c41][002117be][00000c46] e820fdffff call 00000966 // call H(P,P)

Because P calls H(P,P) P specifies infinitely nested simulation to every
simulating halt decider H.

This has been verified with the execution trace of a correct pure
simulation of P.

Whether or not H aborts its simulation P never reaches its final state
therefore the simulated P never halts.

If the simulated P never halts then H(P,P)==0 is always correct for
every simulating halt decider H.

To refute the claim that the direct execution of P(P) halts thus its
simulation is incorrect H(P,P) directly executes its input instead of
simulating it. The result is the infinitely nested simulation becomes
infinite recursion.

In no case does the following directly executed P ever reach its final
state of c50.

// call void P(I);
int H(u32 P, u32 I)
{ if (!Halts(P,I)
return 0;
((void(*)(int))P)(I);
return 1;
}

int main()
{ H((u32)P, (u32)P);
}

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

On 11/10/2021 8:36 AM, Malcolm McLean wrote:
> On Wednesday, 10 November 2021 at 13:37:01 UTC, Ben Bacarisse wrote:
>>
>> I, for one, am fed up with trying to explain ever more silly
>> consequences of the initial assumption about H. The proof is simple and
>> the contradiction entailed is obvious.
>>
> There seems to be an oscillating between a pure simulator and a halt
> decider. Then recently there's been a distinction between a decider which
> simulates its input and one which executes its input directly.
>
> But the core problem remains that the halt decider returns "false" for a
> machine / program which halts. I haven't see any real advance on that, and
> as you say, it become repetitive pointing it out.

Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn

If the input to Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ never halts then the transition to ⊢* Ĥ.qn
is necessarily correct no matter what Ĥ ⟨Ĥ⟩ does. A halt decider is only
accountable for correctly deciding the halt status of its actual input.

>>
>> Indeed. So tell PO that there is no string <H^>. If there were, there
>> wold be a TM H^ halts if it does not and does not halt if it does.
>>
> There might be a assumption that H is a correct halt decider built into
> PO's argument somewhere, but I haven't actually found it. However I
> haven't been paying such close attention.
>

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

On 11/10/2021 9:44 AM, Ben Bacarisse wrote:
> olcott <NoOne@NoWhere.com> writes:
>
>> In this Linz machine:
>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
>
> Remember to add that this must be the case if, and only if, Ĥ applied to
> ⟨Ĥ⟩ does not halt. Then it all becomes clear to the average reader.
>

If the actual input to Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ would never halt then the transition
to ⊢* Ĥ.qn is necessarily correct no matter what Ĥ ⟨Ĥ⟩ does. A halt
decider is only accountable for correctly deciding the halt status of
its actual input.

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

On 11/10/2021 2:18 PM, Andy Walker wrote:
> On 10/11/2021 13:36, Ben Bacarisse wrote:
>> His removal of the key condition on H^ is crucial to his attempt to keep
>> the discussion going.
>
>     Disagree.  What is crucial to the attempt to keep the
> discussion going is the fact that every man and his dog [other
> sexes and animals are available] feels the need to reply.
>

It can be objectively verified that the correct pure simulation
of the input to H(P,P) never halts. (pages 3-4 of the new paper).

It is known on the basis of logical necessity that when-so-ever
the correctly simulated input to a halt decider never halts
that this halt decider would always be correct when it reports
that its input never halts.

All of the current rebuttals are entirely based on denying this
logical necessity.

Halting problem undecidability and infinitely nested simulation (V2)
https://www.researchgate.net/publication/356105750_Halting_problem_undecidability_and_infinitely_nested_simulation_V2

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

On 11/10/2021 2:49 PM, Ben Bacarisse wrote:
> olcott <NoOne@NoWhere.com> writes:
>
>> On 11/10/2021 1:20 PM, Ben Bacarisse wrote:
>>> olcott <NoOne@NoWhere.com> writes:
>>>
>>>> On 11/10/2021 11:02 AM, Ben Bacarisse wrote:
>>>>> olcott <NoOne@NoWhere.com> writes:
>>>>>
>>>>>> On 11/10/2021 9:44 AM, Ben Bacarisse wrote:
>>>>>>> olcott <NoOne@NoWhere.com> writes:
>>>>>>>
>>>>>>>> In this Linz machine:
>>>>>>>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
>>>>>>> Remember to add that this must be the case if, and only if, Ĥ applied to
>>>>>>> ⟨Ĥ⟩ does not halt. Then it all becomes clear to the average reader.
>>>>>>
>>>>>> If the actual input to Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ would never halt
>>>>> Inputs don't halt or not halt. You've been told this many times. You
>>>>> also know how to say what you are trying to say correctly, but I think
>>>>> you want to avoid being clear.
>>>>> Anyway, just make sure you keep the correct condition: if, and only if,
>>>>> Ĥ applied to ⟨Ĥ⟩ does not halt. Any other "facts" care to add are
>>>>> immaterial since the correct condition shows that there are not such
>>>>> TMs.
>>>>>
>>>>>> then the transition to ⊢* Ĥ.qn is necessarily correct no matter what Ĥ
>>>>>> ⟨Ĥ⟩ does.
>>>>> What Ĥ ⟨Ĥ⟩ does is what makes the line above apply or not -- it's there
>>>>> in the part you deliberately keep omitting. Ignoring (and not stating)
>>>>> what Ĥ ⟨Ĥ⟩ does is central to why you are wrong.
>>>>>
>>>>>> A halt
>>>>>> decider is only accountable for correctly deciding the halt status of
>>>>>> its actual input.
>>>>>
>>>>> There is no halt decider present in the line you keep misquoting. There
>>>>> is a "half-decider" at Ĥ.qx and we know what it does. You just keep
>>>>> omitting the key statements so that you can add some waffle instead.
>>>>
>>>> If the pure simulation of the actual input to Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ would never
>>>> reach a final state of Ĥ then the transition to ⊢* Ĥ.qn is necessarily
>>>> correct no matter what Ĥ ⟨Ĥ⟩ does. A halt decider is only accountable
>>>> for correctly deciding the halt status of its actual input.
>>>
>>> As I say, you can add any waffle you like provided you keep the correct
>>> condition in place. You can prove that for every TM H that behaves as
>>> Linz specifies, the string ⟨Ĥ⟩ is even. And you can prove that it's odd
>>> as well. You can prove anything from a contradiction.
>>
>> If it is necessarily true that input to Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ never halts when
>> it is correctly simulated then it is necessarily correct for Ĥ.qx to
>> transition to Ĥ.qn on this input.
>
> You don't seem to be listening. You certainly don't have anything
> pertinent to say.
>

If an X is a Y then Z is always correct when it reports that an X is a Y.

If the correctly simulated input to any halt decider never halts then it
is always correct for this halt decider to report that this input never
halts.

>> You don't seem to be able to comprehend the concept of logical
>> necessity or that disagreeing with logical necessity is woefully
>> foolish.
>
> I think it's rather foolish of you to think I might care about your
> opinion of me. In case you have forgotten, I don't. I happy to stand
> by my posts and let others decide who is being logical.
>

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein

On 11/10/2021 8:08 PM, Ben Bacarisse wrote:
> Richard Damon <Richard@Damon-Family.org> writes:
>
>> On 11/10/21 8:36 AM, Ben Bacarisse wrote:
>>> Richard Damon <Richard@Damon-Family.org> writes:
>>>
>>>> On 11/10/21 6:35 AM, Ben Bacarisse wrote:
>>>>> olcott <NoOne@NoWhere.com> writes:
>>>>>
>>>>>> Here is the same thing using Peter Linz notation:
>>>>> Oh dear, back to talking about Turing machines...
>>>>>
>>>>>> In this Linz machine:
>>>>>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
>>>>>> it is true that the correct pure simulation of the
>>>>>> input to Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩
>>>>> There is no string ⟨Ĥ⟩, so there is nothing that can be simulated. You
>>>>> keep removing the clause that defines Ĥ's behaviour:
>>>>> Ĥ.q0 ⟨Ĥ⟩ ⊢* Ĥ.qx ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn
>>>>> if (and only if) Ĥ applied to ⟨Ĥ⟩ does not halt.
>>>>> With that clause put back, you (well, other people at least) can see
>>>>> that no TM can behave like this.
>>>>
>>>> But, if you step back a bit and ask about the H^ based on a machine H
>>>> that CLAIMS to meet the requirements, then you can have a H^ and a
>>>> <H^>.
>>> I disagree (though it's largely philosophical at this point). From the
>>> claim that H meets Linz's spec we can deduce all sort of things. One of
>>> which is that there is no string <H^>. But can also deduce any other
>>> contradiction you like.
>>> And that's the trouble. Anything PO says about such an H^ is validly
>>> entailed by the assumption. He can even claim that 1 == 0 follows from
>>> "Linz's specs", and he'd be right. At some stage you have to point out
>>> the contradictions and force PO to abandon the initial assumption.
>>>
>>> I, for one, am fed up with trying to explain ever more silly
>>> consequences of the initial assumption about H. The proof is simple and
>>> the contradiction entailed is obvious.
>>
>> The difference is that PO HAS an H, so H does exist, and we can thus
>> build a H^ from. (This assumes we can convert is 'C Program' into some
>> sort of Turing Machine).
>
> Not in this sub-thread. He starts: "In this Linz machine:" and then
> gives the line he say not yet understood. He calls everything H, but
> when it's Linz's we must assume what Linz assumes.
>
> When H refers to his code, it's wrong for the reasons you and André and
> I have been saying. If it's Linz H, it does not exist (or the class of
> TMs referred to by H is empty).
>
> Anyway, I'm butting out. If I've written out the proof using TMs more
> than once, and the world has told him that his C code is wrong by
> definition, but there is no way he will ever see any of this. It's not
> that he's stupid, it's just that he's invested a significant proportion
> of his life, and most of his self-esteem, in this ill thought out idea.
> The mind will play extraordinary tricks in that sort of situation.
>

Within the definition of the x86 language H(P,P)==0 is a necessary
consequence for every simulating halt decider H.

// Simplified Linz Ĥ (Linz:1990:319)
// Strachey(1965) CPL translated to C
void P(u32 x)
{ if (H(x, x))
HERE: goto HERE;
}

int main()
{ Output("Input_Halts = ", H((u32)P, (u32)P));
}

_P()
[00000c36](01) 55 push ebp
[00000c37](02) 8bec mov ebp,esp
[00000c39](03) 8b4508 mov eax,[ebp+08] // 2nd Param
[00000c3c](01) 50 push eax
[00000c3d](03) 8b4d08 mov ecx,[ebp+08] // 1st Param
[00000c40](01) 51 push ecx
[00000c41](05) e820fdffff call 00000966 // call H
[00000c46](03) 83c408 add esp,+08
[00000c49](02) 85c0 test eax,eax
[00000c4b](02) 7402 jz 00000c4f
[00000c4d](02) ebfe jmp 00000c4d
[00000c4f](01) 5d pop ebp
[00000c50](01) c3 ret
Size in bytes:(0027) [00000c50]

Within the definition of the x86 language H(P,P)==0 is a necessary
consequence for every simulating halt decider H.

>>> Indeed. So tell PO that there is no string <H^>. If there were, there
>>> wold be a TM H^ halts if it does not and does not halt if it does.
>>
>> Except that you can create an machine H that you can (incorrectly)
>> claim to meet the requirements, and thus a machine H^ can be created
>> and thus the string <H^> exists.
>
> If he starts "my H" then yes, but he started "this Linz machine". Of
> course calling everything H is just another silly thing he does, but
> there is "Linz's H" which does not exist, and "his H" which does not
> meet Linz's specification.
>

Everyone simply leaps to the conclusion that I must be wrong yet can't
point to a single error in the actual inference steps that prove my
point. Perhaps this simply means that everyone here is mostly clueless
about the x86 language.

Flibble seems to understand me quite well. He even understood the last
required step to convert my H into a pure function so well that he
presented it before I did.

[Olcott wrong about infinite recursion] comp.theory
On 11/10/2021 3:53 PM, Mr Flibble wrote:
> Olcott is barking up the wrong tree re infinite recursion: there
> is only a need to detect a single recursive call into the halt decider
> and signal an exception. Why? Because infinite recursion is valid
> program behavior.
>
> /Flibble

Halting problem undecidability and infinitely nested simulation (V2)

https://www.researchgate.net/publication/356105750_Halting_problem_undecidability_and_infinitely_nested_simulation_V2

--
Copyright 2021 Pete Olcott

"Great spirits have always encountered violent opposition from mediocre
minds." Einstein