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

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.