[Termination tools] competition rules, extra systems

[H. Zantema]

Dear Claude,

In the mean time I made a version of TORPA accepting the format
as it is used for SRSs in TPDB, and generating `YES' if termination
is proved. In particular it easily proves termination of your 
examples s6.srs and turing_add.srs, but not for turing_mult and 
turing_copy.

It is in plain PASCAL. If you have a PASCAL compiler (e.g. Gnu-pascal or
free-pascal) it is most convenient that I send you the source. 
Otherwise I may look for a machine with i386/Linux somewhere here 
to generate an executable file (I never use it myself).

Some time ago I proposed an alternative format for the competition
(with systems submitted by participants) on the termtools list. I 
did not yet get any reaction. I can imagine that there are good 
reasons for not following my proposal, but then I should like to hear
them. Anyhow, this should be clear soon.

Apart from that I have some questions:

* Does a participant also get credit for a valid 'NO' answer? Most
  of the tools do not have facilities for this. To my taste proving
  non-termination is a completely different branch of sport than
  proving termination. So I propose to keep them separate, and only
  give credits for valid `YES" answers, and disqualify participants
  that generate `YES' for non-terminating systems (as you already
  proposed).
  
* The list of SRSs is still quite poor. I have some more examples
  from various origins: would you include them in the list?

* Your SRS examples typically have dozens of rules. In many 
  applications TRSs occur having dozens or hundreds of thousands of
  rules. However, in TPDB most TRSs have only a few rules, or at most
  some dozens. Are you interested in bigger examples from real 
  applications? I have some examples of this shape that I should like 
  to see included.
 

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