[Termination tools] Competition 2005 is over !

[Aart Middeldorp]

Dear all,

Claude and Hans did a superb job! Here are some (personal TTT)
comments on the competition and some of the issues raised in the
earlier mails:

+ 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 :-)

+ The new tools did very well and it is very good to have new
   tools competing. However, there are no new research groups
   involved. We think this problem should be given serious
   consideration (see below for a proposal in this direction).

+ Raising the timeout doesn't make sense: some tools can solve
   some more problems, so what? The outcome remains the same. The
   competition took more than 3 days, so it wasn't too exciting to
   watch it "live", all the more because the binaries of the tools
   were available before the competition (which isn't necessarily
   a bad thing; one tool would have been disqualified otherwise).
   One could imagine a two phase competition: first run all tools
   for 1 or 2 seconds, and then run the tools again for 1 minute
   (saving the earlier results, so that the tools run only on those
   examples where they produced a timeout before). Real challenging
   problems could be distributed on this mailing list or put on-line,
   with the invitation to report successful (non)termination proofs.
   (Coming back to an earlier mail on this mailing list, most systems
   solved by AProVE were solved within 1 second.)

+ 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!

+ 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.

Cheers,

Aart & Nao