Re: Proving the: Simulating termination analyzer Principle

On 4/5/2025 4:58 PM, Richard Heathfield wrote:

On 05/04/2025 21:52, olcott wrote:

*Simulating termination analyzer Principle*
It is always correct for any simulating termination
analyzer to stop simulating and reject any input that
would otherwise prevent its own termination.

 *Halting Problem Principle*
Let us call the function that will
determine whether the program terminates
"terminates (f, x)," and let us further sup-
pose that it gives the answer true if the com-
putation f(x) will eventually (in theory)
terminate, and the answer false if it will
never terminate. Of course, the function
"terminates" itself should be designed
always to terminate; otherwise its general
usefulness would be seriously impaired.
CAR Hoare AND DCS Allison, "Incomputability", 1972.
 So a "termination analyzer" (as you call it) is /required/ to terminate (with the correct answer).
 Because it must terminate, it cannot be allowed to depend on running programs to completion to see if they terminate, lest they don't. They must be cleverer than that.
 Fortunately we don't need to be too clever just to reason about terminates(). We can use pseudo-code to show how to call it and wave our way past its guts.
 We will assume that terminates() correctly echoes either "Does halt" or "Never halts" to the output device, ))))however((((( it arrives at the result, because whether it determines the answer by simulation or by parsing the source is /irrelevant/ as long as it gets the answer right.
 hp(arg candidate, arg testdata)
{
   if(terminates(candidate(testdata)))
   {
     while(forever);
   }
   else
   {
     halt;
   }
}
 We then invoke the program:
 hp(hp, hp)
 and try to predict what terminates() will report, and of course the answer is that we don't know, because neither does terminates(). The function cannot be written.
 

Understanding my simpler example was a mandatory
prerequisite to complex examples such as this:
typedef void (*ptr)();
int HHH(ptr P);
int DD()
{
   int Halt_Status = HHH(DD);
   if (Halt_Status)
     HERE: goto HERE;
   return Halt_Status;
}
Please go back and try again so that many levels
of quotation do not make this key essence more
difficult to see.
--
Copyright 2025 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer