[Termination tools] Competition 2005 is over !

[H. Zantema]

On Thu, 14 Apr 2005, Claude Marche wrote:

> Please allow me to write a few comments about the competition
> 2005. Since we have no meeting to discuss about the competition, like
> last year, I encourage people to write their own comments to this list.
> 
> First, I would like to thank the new entrants, Jambox, TEPARLA and
> TPA, which performed very well, and contributed to make the
> competition more interesting.

First I want to thank you for running the competition. As far as I can see
everything was perfect.
 
> 1) The system of "secret" problems given just before the competition
>    seems good to me. It is clear that this collection reveals the
>    respective strengths and weaknesses of the tools.
I agree, this makes it more exciting. I propose to keep this format.
Also the number of 5 is OK I think. Before establishing the rules we
doubted between 5 and higher numbers, but I think 5 is sufficient for its
purpose.
  
> 3) A particular satisfactory point: the secret problem cime1.trs was
>    an open problem to me and its original author Eduardo Bonelli. But
>    TEPARLA solved it ! I'm sure that Eduardo will be very interested
>    in that proof. 
And a very simple proof: only using polynomials and nothing more. We were
surprised that the other tools could not solve it.
 
> 3) I find the 1 minute timeout a bit to low. I would like to suggest,
>    for the next competition, a larger one, say 5 minutes. 
Why? By far most of the proofs are found in at most a few seconds; for the
present tools a time limit of 1 minute or 5 minutes would hardly influence
the results. And I do not expect that extending this time limit would 
influence the research in termination techniques. May be I am biased by
the average 0.04 seconds YES score for TORPA... 
I think that extending this time limit will cause practical problems.
Now the competition could be run in 2 1/2 days, which is acceptable, but
should not be much more. The majority of this computation time is consumed
by failing attempts until the time limit is reached. So increasing the
time limit will strongly increase the total computation time. I am afraid
that if next year again there will be more participants and TPDB will be
increased (as I hope), then extending time limits will make the whole 
operation intractable.

> 4) Onl the 'standard rewriting' sub-categories have a real interest:
>    the others have too few participants. And nobody proposed "secret"
>    problems for those... (except one, cime6.trs, which was not
>    difficult anyway)
I think it is hard to control this. About the secret problems I think it is 
preferred that they are mainly chosen in the subcategory with the most 
competitors, being the standard subcategory.

> I think we have to think about the next competition as soon as
> possible :
> 
> 1) Will the participants of this year still want to participate ?a
About the T*A systems I definitely expect there will be new developments and 
participation next year, but I have no idea in which shape.


> 2) When should it take place ? If it was much before WST (or RTA), we
>    could have an opportunity the insert a report on the competition in
>    WST (RTA ?) proceedings.
I think running just before WST / RTA is the most natural moment. We can think
of a report in the proceedings explaining the background, the rules and the 
objective, with a reference to the web page containing the (forth-coming)
results.
  
> 3) How can we attract participants for LP categories ?
My impression is that the hype is over in the LP community, and that the
different LP tools mainly do incomparable things. Both observations make
it hard to attract participants in this category.
 
> 4) Should we add new categories ? higher-order rewriting ?
I should like to extend the categories outside rewriting, including
programming. LP is an option, but one can also think of imperative 
programming. A few weeks ago I was surprised that straightforward 
transformations of non-deterministic bubble sort and the program
while x < y do x := x+1 for natural number variables x and y to TRSs, 
could not be solved by the 2004 version of AProVE.
I am afraid development of new categories is hard to control. It has to
start by several groups developing software for similar problems. As soon
this software has been developed it can be involved in the competition. 

> 5) How could we enhance the tpdb ? Are there volunteers to work on it ?
I did some organization of TPDB this year, and I volunteer to do that again
next year. But the main work to be done is that new systems are developed,
and it would be nice if more people than now would develop new systems for
TPDB.
  

		Best regards, Hans Zantema.

+--------------------------------------+-----------------------------+
|                                      |                             |
|   Dr Hans Zantema                    |   Hoofdgebouw   kamer 6.73  |
|   Faculteit Wiskunde en Informatica  |   tel (040)2472749          |
|   Technische Universiteit Eindhoven  |   fax (040)2468508          |
|   Postbus 513     5600 MB Eindhoven  |   e-mail  H.Zantema at tue.nl  |
|   The Netherlands                    |   www.win.tue.nl/~hzantema  |
|                                      |                             |
+--------------------------------------+-----------------------------+