Re: How do simulating termination analyzers work?

Op 19.jun.2025 om 17:09 schreef olcott:

On 6/19/2025 4:09 AM, Fred. Zwarts wrote:

Op 19.jun.2025 om 08:59 schreef olcott:

On 6/19/2025 1:17 AM, Mikko wrote:

On 2025-06-18 13:46:16 +0000, olcott said:
>

On 6/18/2025 5:12 AM, Fred. Zwarts wrote:

Op 18.jun.2025 om 03:54 schreef olcott:

On 6/17/2025 8:19 PM, Richard Damon wrote:

On 6/17/25 4:34 PM, olcott wrote:

void Infinite_Recursion()
{
   Infinite_Recursion();
   return;
}
>
void Infinite_Loop()
{
   HERE: goto HERE;
   return;
}
>
void DDD()
{
   HHH(DDD);
   return;
}
>
When it is understood that HHH does simulate itself
simulating DDD then any first year CS student knows
that when each of the above are correctly simulated
by HHH that none of them ever stop running unless aborted.

>
WHich means that the code for HHH is part of the input, and thus there is just ONE HHH in existance at this time.
>
Since that code aborts its simulation to return the answer that you claim, you are just lying that it did a correct simulation (which in this context means complete)
>

>
*none of them ever stop running unless aborted*

>
All of them do abort and their simulation does not need an abort.
>

>
*It is not given that any of them abort*

>
It is known a priori that HHH either does or does not abort.

>
Very good.
>

If HHH does
not abort it does not terminate the simulation of DDD and therefore

>
DDD never stops running.

>
because HHH never stops running and therefore this HHH
>

 So you agree that when HHH never aborts that none
of the above three functions ever stop running?
 

>

does
not report correctly. If HHH does abort it reports that DDD does not
halt, which is incorrect as in that case DDD does halt. HHH is correct
about DDD only if it does abort its simulation and reports "halts".
But you HHH does not do that.
>

>
>

>
So, both the aborting and the non-aborting HHH do not provide a correct report.

 I am not yet talking about any reports.
I am only talking about:
(a) stops running
(b) never stop running.
 

We can agree that all of them fail to reach the end of a correct simulation. The simulation stops running in some cases, but that is only a failure to see the halting behaviour specified in the input.