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

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?
 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
its simulation of DDD causing every level of
emulation to immediately stop.
 

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.
 

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)...
 until the outer HHH sees the repeating
pattern and aborts its own emulation thus
killing off every other emulation.