[Termtools] Remarks on the Termination Competition

[Zantema, H.]

Dear all,

I am not in favor of Juergen's proposal. 

The 2007 competition has finished now, with the results as we can read
on the web page. I just saw Claude's email with the same conclusion.

Juergen mentions two problems motivating his proposal.

1. Unclear time limits. Indeed this was a problem. On the competition
web page it was announced that the time limit would be in between 1 and
5 minutes. Separate from that in discussions on termtools I proposed
only to change time limits if this was announced in advance. Apparently
this proposal was not followed by Claude, but he followed the range as
it was announced on the web page. 

2. Bugs found in tools. I think this is not different than other years.
Remember that last year also there were two disqualifications: one due
to a YES generation for a non-terminating TRS and one due to wrong
proofs with agreement with the tool author. This year it was exactly the
same, with the only difference that we decided not to show the
disqualified tools. This decision was motivated by undesired effects of
showing disqualified tools.
There were indications that referees of papers written by disqualified
tool authors were already negative in advance before even having read
the paper. Of course this attitude is not fair, but we do not have any
control on this. Due to this kind of undesired effects we preferred not
to emphasize disqualifications.

The fact that the TTT2 team now finds an error in their tool is in my
view no reason of disqualifying / removing TTT2 from the competition
results pages. Several other tool authors found errors in their tools
after the competition was finished without any consequence for the
result pages.

Juergen's arguments are mainly arguments in favour of an ongoing
competition, in which any column in the competition result page can be
renewed as soon as the corresponding tool comes with a new release, and
the result page always show the results for the newest versions of all
tools. There are several arguments against or in favour of this other
format; I think we should only switch to such a format after more
discussion.


            Best regards, Hans Zantema.

_________________________________________________________
Dr Hans Zantema            
Technische Universiteit Eindhoven, Department of Computer Science 
P.O. Box 513, 5600 MB Eindhoven, The Netherlands 
e-mail: H.Zantema at tue.nl, homepage: www.win.tue.nl/~hzantema
office: Hoofdgebouw room 6.73, tel: (040)2472749
 

-----Original Message-----
From: termtools-bounces at lists.lri.fr
[mailto:termtools-bounces at lists.lri.fr] On Behalf Of Juergen Giesl
Sent: dinsdag 12 juni 2007 12:58
To: termtools at lri.fr
Subject: [Termtools] Remarks on the Termination Competition

Dear all,

> Now what to do? Should TTT2 be removed from the TRS table since
> correctness is not guaranteed? We wonder though what message that
> conveys. Only three participants in the TRS category? AProVE against
> a weak version of Jambox (due to unclear time limits?) and a tool
> (NTI) that "only" aims to disprove termination?

I think that this year's termination competition suffered from 2
problems:

1. The time limits were unclear and didn't correspond to what was
    discussed before. It seems that most participants assumed that the
time limit
    would be 60 seconds wall-clock-time, but it turned out that
    a different time limit of 120 seconds user-time was used.

2. There were many tools where bugs were discovered during the
competition.

Concerning buggy tools, I don't think that disqualification is
the right idea. After all, the tools that are not disqualified are not
at all guaranteed to be bug-free. They were probably just lucky. Indeed,
for several of the successful tools in the 2006-competition, bugs were
discovered afterwards.

I think that a main goal of the competition is to demonstrate the
state-of-the-art in termination proving. As it is now (and even more if
TTT2 would be disqualified), the impression that one gets from the
webpages
of the competition is that almost nobody is working on TRS-termination
anymore
and that the only really active research area is SRS-termination.
I am not happy with giving this impression.

After all, this "competition" is not really concerned with money or
anything like
that, and we should not behave like competitors, but like colleagues.
Therefore,
my proposal would be the following:

- Give all tools with known bugs the chance to repair these bugs. We
would trust
   the tool authors that they only perform bug fixes and will not tune
their tools further.
   One should impose a deadline for the submission of the repaired tools
   (e.g., beginning of next week).

- Then re-run the competition with all tools (including the fixed ones),
   but with the time limit that was assumed by the participants
   (60 seconds wall-clock time, not user time).

This should enable the tools with bugs as well as Jambox (who suffered
most from the modified time limit) to participate in the competition in
a sensible way.
Re-running the competition would then still be finished in time for RDP.

Best Regards
Juergen
_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools