[Termtools] Outermost Category
René Thiemann
rene.thiemann at uibk.ac.at
Fri Oct 31 09:21:53 CET 2008
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
More information about the Termtools
mailing list