Path: news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: "Fred. Zwarts" <F.Zwarts@HetNet.nl>
Newsgroups: comp.theory,sci.logic,comp.ai.philosophy
Subject: Re: HHH(DD) does correctly reject its input as non-halting ---
 VERIFIED FACT
Date: Sat, 14 Jun 2025 11:10:43 +0200
Organization: A noiseless patient Spider
Lines: 121
Message-ID: <102jeak$3avu$1@dont-email.me>
References: <102erpt$2ohps$5@dont-email.me> <102gvs0$3d4cf$1@dont-email.me>
 <102hhhn$3gqbm$5@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Sat, 14 Jun 2025 11:10:45 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="e6a1a9d2c4ec8df2ebbe13317fee6ee4";
	logging-data="109566"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1+NTAOZ7wwr8d6X9vLwkm3q"
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:MtqXoNlitOT6aOFWR+fUL88F6fc=
Content-Language: nl, en-GB
In-Reply-To: <102hhhn$3gqbm$5@dont-email.me>

Op 13.jun.2025 om 17:53 schreef olcott:
> On 6/13/2025 5:51 AM, Mikko wrote:
>> On 2025-06-12 15:30:05 +0000, olcott said:
>>
>>> int DD()
>>> {
>>>    int Halt_Status = HHH(DD);
>>>    if (Halt_Status)
>>>      HERE: goto HERE;
>>>    return Halt_Status;
>>> }
>>>
>>> It is a verified fact that DD() *is* one of the forms
>>> of the counter-example input as such an input would
>>> be encoded in C. Christopher Strachey wrote his in CPL.
>>>
>>> // rec routine P
>>> //   §L :if T[P] go to L
>>> //     Return §
>>> // https://academic.oup.com/comjnl/article/7/4/313/354243
>>> void Strachey_P()
>>> {
>>>    L: if (HHH(Strachey_P)) goto L;
>>>    return;
>>> }
>>>
>>> https://academic.oup.com/comjnl/article-abstract/7/4/313/354243? 
>>> redirectedFrom=fulltext
>>
>> Strachey only informally presents the idea of the proof. Formalism
>> and details needed in a rigorous proof is not shown.
>>
> 
> void DDD()
> {
>    HHH(DDD);
>    return;
> }
> 
> _DDD()
> [00002192] 55             push ebp
> [00002193] 8bec           mov ebp,esp
> [00002195] 6892210000     push 00002192
> [0000219a] e833f4ffff     call 000015d2  // call HHH
> [0000219f] 83c404         add esp,+04
> [000021a2] 5d             pop ebp
> [000021a3] c3             ret
> Size in bytes:(0018) [000021a3]
> 
> Exactly how would DDD correctly emulated by HHH
> reach its own "ret" instruction final halt state?

Indeed, HHH fails where other world-class simulators have no problem to 
simulate the program specified in the input.

> 
> The directly executed HHH emulates DDD that calls
> HHH(DDD) to emulate DDD again until this directly
> executed HHH sees the repeating pattern then aborts

A premature abort, because it assumes an infinite repeating pattern, 
where there is only a finite repeating pattern.

> its simulation of DDD causing every level of
> emulation to immediately stop.

And missing the most important part of the input, where the simulated 
HHH would abort and halt.
That HHH does not see that part does not change the fact that this 
behaviour is specified in the input.

> 
>>> It *is* a verified fact DD correctly simulated by HHH
>>> cannot possibly reach its own "return" statement
>>> final halt state.
>>
>> That "cannot possibly" is not a part of any verifiable fact as
>> it is not sufficiently well-defined for a verification. 
> 
> It is a self-evident truth that required actual comprehension
> to be complete proof.
> 
> 2 + 3 = 5 is another example of a self-evident truth.
> Some people could say "I doan beeve in nummers". That
> is not any rebuttal.

So, it is self evident that HHH fails.
Why do you repeat it?

> 
>> What
>> cannot be stated cearly and unambiguoulsy cannot be a verified
>> fact.
>>
> 
> HHH emulates DDD that calls HHH(DDD)
> that emulates DDD that calls HHH(DDD)
> that emulates DDD that calls HHH(DDD)
> that emulates DDD that calls HHH(DDD)...

This repeats only a finite number of times.
(Not even four times in the code specified in Halt7.c)

> 
> until the outer HHH sees the repeating
> pattern and 

prematurely

> aborts its own emulation thus

prematurely

> killing off every other emulation.

and failing to see the  specified behaviour of the simulated HHH doing 
an abort and halt.

> 
>