[Termination tools] Rules of the WST competition

[Claude Marche]

Dear colleagues,

I would like to make some clarifications regarding the so-called
WST "competition" of termination tools. 

Last year, during WST'03 in Valencia, a first "competition" was
initiated by Albert Rubio. There were no formal rules, participants
were gathered in the same room, and both participants and other people
in the room were asked to suggest examples to work on. Then participants
were trying to prove termination of proposed examples, using their own
tool running on their own laptop. They were spending time
in tunning the various settings their tool propose to achieve a
termination proof. At the end, only few examples have been tested on
all tools, so it was not possible to make a realistic comparison.

My idea was then that such a "competition" should be more formally
organized so that: 
. tools should be run all on the same computer
. tools should be run fully automatically, as they would be run by a
  "naive" user of the tool
. tools should be all run on the same large set of examples.

The large set of examples exists now: the TPDB, with the common
format. I have now coded some wrapper that is able to run tools
without user interaction, so I'm ready to start the process as soon as
I have the tools themselves.  This wrapper may be interrupted and
restarted later on, new tools may be added as new participant in the
middle of the process. I think a few days are enough to run all tools
on all the TPDB, and for me this should be the "competition", whose
results would be very interesting on a scientific point of view.

Now, some of you would like this "competition" to become some "sport"
were, as we all know, what is important is to win and not to
participate. This is not my idea of this "competition". I don't want
to spend time to track possible cheats, such as recognizing the shape
of the given TRS and looking up to database of examples which are already
known to be terminating. I don't think there is any tool doing this
anyway. I don't want to spend time in trying to find a way of
selecting a set of examples that will be agreed by all participants.
Some of you suggested that each participant should select a set
of examples, say 10 or 20. I don't think it is a good idea: this rule will
encourage people to find examples which are solved by their own tool,
but not by the others, and the results will not reflect the real
abilities of each tool. Other suggested that examples should be chosen
by independant people, why not, but who ? Not me because I'm a
participant. It could be hard anyway to find people who would be
completely impartial. So which solution remains ? We could benefit
from the CASC experience (The competition of theorem provers of CADE),
which has been run successfully for years: the solution found by the
organizers is to select problems randomly from 
the TPTP database. We could do the same using the TPDB, but the TPDB
is unfortunately much younger than the TPTP, has much less problems,
so is probably not yet "representative" of termination problems (if it
means something).

I think the best thing for future WST competitions would be to
encourage growth of the TPDB (with cleaning, removing duplicates,
organizing problems differently, etc.), so that a selection of random
problems would become the best way of running the WST competition.
Unfortunately, Albert Rubio had to give up from its task of
maintaining the TPDB, I had to do the porting to the new format
myself, hence the TPDB did not grow much since last year. Regarding
that, I would like to thank people who sent me mails pointing out the
mistakes, and proposed new examples. I think there is no more mistake
now. Any idea of organizing the TPDB differently, any suggestions, are
welcome.  Volunteers are welcome.

So, for this year, I will follow my first idea of running all tools on
all the TPDB. If some of you are willing to set up another
"competition" on a set of examples that will come from another source,
please do so.  If this set of examples is made available in the TPBD
format, I can run my wrapper on it, it is no problem with me since it
runs automatically.

Finally, during next WST, there will be a special session devoted to
something similar to the last "competition", that will called an
"exhibition". During this, we could also take time to discuss the
future of the competition, and the future of the TPDB.

Any comments/suggestions welcome.

- Claude

-- 
| Claude Marché           | mailto:Claude.Marche at lri.fr |
| LRI - Bât. 490          | http://www.lri.fr/~marche/  |
| Université de Paris-Sud | phoneto: +33 1 69 15 64 85  |
| F-91405 ORSAY Cedex     | faxto: +33 1 69 15 65 86    |