[Termination tools] Re: WST'04 Competition of termination Systems

[Claude Marche]

>>>>> "Hans" == H Zantema <hzantema at win.tue.nl> writes:

    Hans> Dear Claude,
    >> First, a technical question: did you try to send your message to the
    >> termtools list? I'm puzzled with the Cc line I received:
    >> 
    >> 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>
    >> 
    >> May be this new list is not well configured yet... Anyway, to send a
    >> message to this list, you have to register before.

    Hans> I tried to register, and I expect it is OK now, and I will send general 
    Hans> discussion contributions to the termtools address.
 
I think you are registered now.

    >> Now for your questions: yes, there are very few SRS in the tpdb, and
    >> we need more, so examples are welcome. Even if they are randomly
    >> generated, but in that case please make a selection of interesting
    >> ones. 
    Hans> I am busy already making a list of example SRSs. Of course this is an 
    Hans> ongoing action, but I intend to send a first list within a few weeks, in 
    Hans> the syntax we have agreed by then. Do you prefer every SRS in a separate 
    Hans> file?

Yes, one file for each system.

    Hans>  About the syntax, you're right, the one we give is
    >> ambiguous. This reveals that it has not been tested, unlike the TRS
    >> one... So send me some examples in your common syntax with matchbox, I
    >> will see. If all participants agree with it, of course we can adopt
    >> it.
    Hans> In the present TORPA syntax one has for example the three rule SRS
    Hans> acb -> baba
    Hans> b -> cc
    Hans> aa -> abca

    Hans> This is not exactly the matchbox syntax, but the difference is minor. I will
    Hans> discuss with the matchbox people a common syntax. Do you have ideas about 
    Hans> that, for instance:
    Hans> * Do you prefer to start by RULES or something like that? On the one hand
    Hans>   this may be convenient if also other information like LEFTMOST should be 
    Hans>   possible, on the other hand it is redundant if it used for
    Hans> giving an SRS only.

Yes, I would like to have the possibility of giving strategies. So
yes, a RULES section.

    Hans> * Do you agree with newline as the marker between different rules, and not having
    Hans>   an explicit end marker? Otherwise we can use a comma "," as marker between
    Hans>   rules and a dot "." as end marker, by which the above example may read
    Hans>   acb -> baba, b -> cc, aa -> abca.

No, I think the newline for the end marker is bad, so yes, please
let's use an explicit marker. What do you think of the syntax proposed
yet, with additional commas between rules ? So it will be

(RULES a c b -> b a b a, b -> c c, a a -> a b c a)

Remains the issue of spaces between symbols or not. I would like to
require them, because otherwise it seems to me that you are limited to
26 symbols, right ? Moreover, I have some examples, coming from some
Turing machine simulation, where I have symbols q1 q2 etc.

    >> About your YES/NO question: yes, there are non-terminating examples in
    >> the database. So a program that would answer always answer YES would
    >> be disqualified. About giving one point for a correct NO answer: I
    >> don't even know if there exist a tool which is able to prove
    >> non-termination, so this question may be irrelevant. But I think it is
    >> an important issue. Anyway, for this first attempt of an automatic
    >> competition, the scoring is not my main concern.

    Hans> I know that Matchbox has facilities for searching for loops, hence for 
    Hans> non-termination. As far as I know the other tools (including TORPA and AProVE)
    Hans> have no such facilities. You should realize that by the rules of the competition
    Hans> you influence the direction of further development. In particular if points are
    Hans> not only achieved for termination proofs but also for non-termination proofs,
    Hans> then you encourage the participants to develop facilities for this. I think
    Hans> (and I know many people agree) that proving termination and proving 
    Hans> non-termination should be kept separate since the techniques are completely 
    Hans> different.

Indeed, I hope that the competition will influence the direction of
further development. I understand your objection about scoring, so
yes, maybe we will not take the NO answers into account into the
scoring. 



    Hans> 		Best regards, Hans Zantema.

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

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