[Termination tools] Several issues

[Juergen Giesl]

Dear all,


 > + AProVE (TRSs) and TORPA (SRSs) are far ahead, which raises the
 >   question whether the performance of a tool is directly related
 >   to the number of techniques implemented :-

Indeed, I think that one of the conclusions is that there is no
single technique which beats everything, but the most successful
approach is to combine many techniques. However, how to combine
these techniques in order to obtain something successful
is a non-trivial problem (and here, further improvements
are clearly possible).



 > Also, the timeout needs not to be necessarily the same for each
 > problem. One could imagine a way to enlarge the timeout, for all the
 > problems that have not been solved this year. It could even be done
 > automatically : if a problem is not solved by any tool, then we rerun
 > the tools with a larger timeout. Imagine we do that
 > first with 1 second, then 10, then 1 minute, then 5 minutes : I guess
 > TTT will be pleased with that !

I think that even if there is a system
that can solve a problem in 1 second, it is still interesting to know
whether other systems can probably solve it in 10 seconds. But I agree
that raising the timeout from 1 minute to something higher should only
be done for systems where no tool was successful within 1 minute (since
otherwise, the competition will take too long).


 > + Asking developers to extend their tools with known transformations
 >   from, say, conditional or context-sensitive systems to standard
 >   TRSs doesn't produce interesting competitions in the respective
 >   categories. The participation of tools (like MU-TERM) that apply
 >   direct methods is needed.
 >
 >  > Since here, the termination proofs work via a translation into
 >  > first-order TRSs, the other tools could easily be extended to
 >  > accept these higher-order TRSs as well. So maybe it is a good
 >  > idea to add this category (what do you think, Aart?).
 >
 > If we can agree on a common syntax and, more importantly, convince
 > the people from the research groups in Japan working on termination
 > of higher-order systems to implement their techniques then this
 > could be interesting. Something to discuss next week in Nara!


I'm not sure that adding the transformations to the existing tools
is uninteresting. For example, the TRSs resulting from CTRSs have a certain form
and it might be interesting to see how good the tools are on these TRSs.

But I agree that it would be even more interesting to compare tools
which work via a translation with tools which work on LPs or CSRSs
directly.

 > + Now for a proposal to make the competition more attractive for
 >   outsiders (and insiders?): Every year a particular method (e.g.
 >   LPO) is selected and everyone is invited to implement the method;
 >   the implementations are then compared on the problems in the TPDB.
 >   So the emphasis will be on efficiency. We believe this might
 >   attract many new people to the area which in turn could stimulate
 >   further termination research.

Indeed, I agree that would be interesting. As I mentioned above,
I believe that in order to be as successful as possible, one has to
combine many techniques in a sophisticated way. But how to implement
each of these techniques efficiently is also an interesting question.

However, I see the problem that simply
comparing the runtimes does not give an objective comparison since people
use different programming languages. I guess that there exist some
investigations on the speed of different languages. Maybe one could multiply
the runtimes in this special efficiency-competition by a certain factor
depending on the language used.

 > I would like to suggest adding a new category (or categories)
 > involving real (rule-based) programming languages like Maude,
 > Elan, or Haskell...

I agree that would be very interesting, but first we need to make sure
that there will be tools which can handle these languages. Indeed, we are
working on extending AProVE to handle Haskell as well and can more or less
parse and type-check Haskell programs by now. However, I can't yet say
how far we will be with this by the time of the next competition and
whether we can already prove termination of many programs by then.
But we should discuss the issue of adding Haskell to the competition
further.

Best Regards
Juergen