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:51:44 +0300
Organization: -
Lines: 42
Message-ID: <102gvs0$3d4cf$1@dont-email.me>
References: <102erpt$2ohps$5@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:51:45 +0200 (CEST)
Injection-Info: dont-email.me; posting-host="c40a1205e8a6c6978bf722a4c5e06e48";
	logging-data="3576207"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX186yGQFgovFzMEb7S9CiYUe"
User-Agent: Unison/2.2
Cancel-Lock: sha1:l3kRSW6Lw8Sa3GJAHy/loLMWqUE=

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.

> 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. What
cannot be stated cearly and unambiguoulsy cannot be a verified
fact.

-- 
Mikko