Path: news.eternal-september.org!eternal-september.org!.POSTED!not-for-mail
From: Mikko <mikko.levanto@iki.fi>
Newsgroups: comp.theory
Subject: Re: HHH(DD) does correctly reject its input as non-halting --- VERIFIED FACT
Date: Fri, 13 Jun 2025 13:20:43 +0300
Organization: -
Lines: 41
Message-ID: <102gu1r$3cjca$1@dont-email.me>
References: <102es19$2ohps$6@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Fri, 13 Jun 2025 12:20:44 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="c40a1205e8a6c6978bf722a4c5e06e48";
	logging-data="3558794"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX18oTS2TALsOhj0nHdezS34K"
User-Agent: Unison/2.2
Cancel-Lock: sha1:O+sHcGhn7Tt0Nvs8mcOQNrOkQaY=

On 2025-06-12 15:34:01 +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 
> 
> 
> It *is* a verified fact DD correctly simulated by HHH cannot
> possibly reach its own "return" statement final halt state
> because the input to HHH(DD) specifies recursive simulation.

False. It is not the reursive simulation that prevents the reaching
the simulation of the "return" statement. Instead, previention is
a consequence of the discontinuation of the simulation that the
input specifies. The input also specifies that the final "return"
statement is executed after the discontination of the simulation.
At this point HHH is not faithful to the specification.

-- 
Mikko