[Fwd: Re: WST'04 Competition of termination Systems]

[Juergen Giesl]

Dear Colleagues,

first of all, thanks a lot to Claude and Albert
for organizing the exhibition/competition.
I think most points in the rules mentioned
on the web are fine.

But I agree with Hans that there are still
some things that could.should be improved.
(I forward his mail again, since
he sent it to "termtools-approval" instead of
"termtools".) Basically, I think that most of the suggestions
he made for string rewriting
also hold for the competition on termination of
TRSs instead of SRSs. So to summarize, my suggestions
to improve the rules of the competition would be
the following:

1. I think that the problems should not be chosen
    from the data base by the organizers. This has
    two disadvantages:

     a) Since all these examples are known before, people
        can train their system w.r.t. the data base.

     b) It might give a strange impression if
        the organizers (who most likely
        participate themselves) have more influence or
        more knowledge about the examples than the other
        participants.

    Therefore, I think the better solution is that
    the examples for the competition come from the participants
    (as Hans suggested), where everyone can bring a
    fixed number of examples, e.g. 10. These examples
    should be unknown before to everyone, including
    the organizers. Since the competition
    will be performed on just one computer, this is easy to
    organize (the participants just have to bring
    their examples on a floppy or memory stick etc.)


2. I think that there should be several categories,
    not just TRS, SRS, and LP. For example, there might
    be a category for TRC with AC, just innermost termination,
    just full termination, etc. In particular, I don't think
    that it is a good idea to only to offer a category for proving
    both termination and non-termination. Since most systems
    specialize on proving termination, I think there should
    clearly be a category where only "YES" counts (here I completely
    agree with Hans). One could of course have another category,
    where only "NO" or both "YES" and "NO" counts, and then
    most likely only systems will participate in this category
    which have a feature for non-termination proofs.

Please let me know what you think about it.

Best Regards
Juergen


-------- Original Message --------
Subject: Re: WST'04 Competition of termination Systems
Date: Mon, 08 Mar 2004 16:24:10 +0100 (CET)
From: H. Zantema <hzantema at win.tue.nl>
To: Claude Marche <Claude.Marche at lri.fr>
CC: termtools-approval at serveur-mail.lri.fr, "Hofbauer, Waldmann Geser" 
<dieter at theory.informatik.uni-kassel.de>, geser at nianet.org, waldmann at imn.htwk-leipzig.de, Juergen 
Giesl <giesl at informatik.rwth-aachen.de>

On Mon, 8 Mar 2004, Claude Marche wrote:

> Dear Colleague,
> 
> This year, we try to organize the WST'04 competition in a more formal
> manner. Please look at
> 
> http://www.lri.fr/~marche/wst2004-competition/
> 
> for details. You will see in particular that there is a mailing list
> for general discussion about this competition, which will be the right
> place to ask questions and discuss about the rules.

I am happy that the termination competition will be organized in a more
formal manner than last year. I should like to participate with my tool
TORPA on string rewriting. However, there are still quite a lot of problems:

* For string rewriting there are hardly examples in the data base. So these
   should be added in case the competition is only restricted to SRSs from
   this data base. However, I am convinced that for string rewriting it is not
   appropriate to restrict the competition to systems from a fixed data base.
   It is quite easy to generate thousands of SRSs for which termination is
   non-trivial to prove: for instance by randomly generating SRSs and apply
   TORPA to it, and only submit those SRSs to the database for which TORPA
   proves termination in a non-trivial way.

   If you like I can do this, but then the competition is not really fair.
   I think a much more fair competition is obtained if the SRSs on which
   the competition is applied are not drawn from such a fixed data base, but
   is submitted by the participants. If every participant may submit a fixed
   number (say ten) SRSs, then a much more interesting and fair competition
   is obtained.

* In the rules it is said that one point is obtained for a correct answer,
   both if it is YES ore NO. It is expected that the correct answer for most
   of the systems in the competition will be YES, but this is not for sure.
   Most systems concentrate on proving termination, and have no facility for
   proving non-termination. If it is a termination competition, then only a
   point should be obtained if YES if generated for a terminating system, and
   no point if NO is generated. On the other hand a program always generating
   YES should not win the competition. Such a program only will be disqualified
   (as is desired) if at least one of the systems for the competition is
   non-terminating.

* The syntax proposed for string rewriting is ambiguous. As far as I can see
   ( RULES a b -> a a a -> b ) is in this syntax, but it is not clear whether
   the two rules ab -> a, aa -> b,  or the two rules ab -> aa, a -> b  are
   meant. Moreover, in string rewriting it is usual that symbols in a string
   are single letters and not full identifiers; I think that for all
   participants it will be more convenient to follow this convention, and
   not use space between consecutive symbols in a string. As far as I know
   TORPA and MATCHBOX are the only two tools concentrating on string rewriting.
   Do you agree that if the matchbox people and me agree on a syntax, then
   this syntax is used?

I realize that some of these points may sound quite negative. Let me emphasize
that the intension is positive and constructive: I hope we will have a
challenging, interesting and fair competition, and I really appreciate your
steps towards achieving this.

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