Re: HHH(DD) does correctly reject its input as non-halting --- VERIFIED FACT

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