[Termtools] Outermost Category

[René Thiemann]

Dear all,

Hans wrote:
>>> We should include outermost to have an objective comparison of the  
>>> tools.
>
> René wrote:
>> that would indeed be a good idea. However, the question arises which
>> examples to use. I would go for all TRSs where full termination has
>> not already been proven.
>
> This is a low cost approach to generate lots of uninteresting  
> examples.
> We can include some of them, but I think for getting a sensible  
> comparison we need a list of examples in which the majority is  
> really about outermost.
>
> Of course it is very subjective when an example is 'interesting'.  
> But I am not in favour of running a competition about a sensible  
> variant of rewriting and only apply it to artificial / uninteresting  
> examples, and then draw conclusions about the tools based on the  
> results on these examples. In fact this is the same as what happened  
> with SRS termination where the focus is on artificial extremely  
> small examples (in retrospect I must admit I was partly responsible  
> for that).

Well, then we should also throw out some rubbish (whatever that is)  
for the TRS-category? The reason for my proposal was as follows:

The TRSs which could not be proven terminating might be
1) non-terminating: for these systems it would be interesting if they  
are still non-terminating if one is restricted to outermost strategy,  
or whether they are outermost terminating
2) don't knows: perhaps these are outermost terminating whereas full  
termination was to hard to prove (it is unlikely, that one can  
disprove outermost termination where not even termination could be  
disproven)

So, if one wants to reduce my proposed example list, then I would like  
to see at least the examples of kind 1) in the outermost category.  
(which are about one fourth of the list in my previous mail)

Best regards,
René
-- 
René Thiemann                    mailto:rene.thiemann at uibk.ac.at
Computational Logic Group        http://cl-informatik.uibk.ac.at/~thiemann/
Institute of Computer Science    phone: +43 512 507-6434
University of Innsbruck