Re: Termination analyzer defined ---RICHARD IS WRONG !!!

On 2024-05-12 17:12:00 +0000, olcott said:

On 5/12/2024 10:27 AM, Mikko wrote:

On 2024-05-12 13:59:28 +0000, olcott said:
 

On 5/12/2024 3:45 AM, Mikko wrote:

On 2024-05-11 16:35:48 +0000, olcott said:
 

On 5/11/2024 4:39 AM, Mikko wrote:

On 2024-05-11 00:30:40 +0000, olcott said:
 

A termination analyzer is different than a halt decider in that it need
not correctly determine the halt status of every input. For the purposes
of this paper a termination analyzer only needs to correctly determine
the halt status of one terminating input and one non-terminating input.
The computer science equivalent would be a halt decider with a limited
domain that includes at least one halting and one non-halting input.

 From https://www.google.fi/search?q=termination+analysis and
https://en.wikipedia.org/wiki/Termination_analysis :
 "In computer science, termination analysis is program analysis which attempts to determine whether the evaluation of a given program halts for each input. This means to determine whether the input program computes a total function."
 So the term "termination analysis" is already defined. The derived term
"termination analyzer" means a performer of termination analysis. That
does not agree with the propsed defintion above so a differnt term
should be used.
 That "termination analysis" is a know term that need not be defined
is demostrated e.g. by
    https://arxiv.org/pdf/2101.09783
 which simply assumes that readers know (at least approximately) what
the term means.
 

 You are doing a great job performing an honest review!
So every time that Richard referred to a {termination analyzer} that
ignores its inputs *Richard was WRONG*

 More important is that you are wrong whenever you use "termination
analyser" for something that by the conventional meaning isn't.
 

 A conventional termination analyzer is free to use any algorithm
as long as it analyzes termination.

 It is not sufficient to analyse something about termination. The
conventional meaning is that a termination analyser does not say
"yes" unless the analysed program terminates with every possible
input.
 

 A specific program halts with every input is not at all the same
thing as correctly analyzing every program with every input.

If you can't find out whether a program halts with every input even
after analyzing it with every input your analysis is not really
good enough for the purpose.
Anyway, if an analyzer can never tell whether a program terminates
with every possible input then it is not a termination analyzer.

Termination analyzers are allowed to be quite dumb so that they
handle very few programs.

True, but the more the better. But they must not report "yes" if
the program may fail to terminate.

One of the best termination analyzers could not handle any
recursive programs at all for quite a few years.

In many context recursive programs are prohibited anyway so that
is not always a serious restriction.
--
Mikko