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

On 2025-06-15 14:51:30 +0000, olcott said:

On 6/15/2025 4:23 AM, Mikko wrote:

On 2025-06-14 13:53:01 +0000, olcott said:
 

On 6/14/2025 6:30 AM, Mikko wrote:

On 2025-06-13 15:22:04 +0000, olcott said:
 

On 6/13/2025 5:20 AM, Mikko wrote:

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.

 When you try to prove this by providing ALL of the
details you will find that you are incorrect.

 I don't need to prove anything. It is sufficient to point out that
you have not proven anything. For this discussion a sufficient
proof that HHH aborts is simulation is that you have said it does.

 This code proves everything that I claimed beyond all possible doubt
https://github.com/plolcott/x86utm/blob/master/Halt7.c

 More importantly, it proves what I climed: HHH does abort its simulation.

 *Just like it is required to do*

That is an extraneous requirement that is not a part of halting problem.
The halting problem does not require any simulation and therefore not
any aborting of simulation.
But the point was that your code proves what I claimed, which was
not about requirements.
--
Mikko