[Termtools] Outermost Category

[joerg at endrullis.de]

I have created a wiki page for the outermost category:
  http://termination-portal.org/wiki/Outermost

I think we can prevent that "uninteresting examples" dominate the
outermost category by choosing an appropriate scoring function.

I would suggest to split the score. That is, give 50 points for the tool
that proves most of the examples with "STRATEGY OUTERMOST" terminating,
and 50 points for the tool that proves most of the "TRSs where full
termination has not already been proven" to be outermost terminating. The
non-winning tools get in both categories 50 * (number of problems solved)
/ (number of problems solved by winner). Thus in theory a tool winning
both categories obtains 100 points.

You are welcome to suggest a different scoring function.

Joerg

> 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
>
>
>
>
>
>
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/mailman/listinfo/termtools
>