Re: Proving the: Simulating termination analyzer Principle

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.
--
Richard Heathfield
Email: rjh at cpax dot org dot uk
"Usenet is a strange place" - dmr 29 July 1999
Sig line 4 vacant - apply within