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

[Johannes Waldmann]

Hello.

Thanks to Albert and Claude for organizing the competition.
I think it is a very good idea to run the programs fully automatically,
and to check YES/NO/UNKNOWN answers.

Matchbox will take part (for string rewriting),
and we might even have something for term rewriting working by then.

When will the competition actually take place?
In the announcement, it reads "during the workshop or a bit before".
I guess "before" is more convenient for the organizers.
But then we need a deadline for sending in the executables.
(At the moment, it says "as soon as possible".)

Is it possible to submit two versions of one program
(say, with different parameter settings)?

What kind of GNU/Linux system will be used?
Possibly there are versioning problems for DLLs
(like, SuSE 8.1 has older libc than SuSE 8.2)
How much main memory can a program get?

In the grammar,  decl ::= id anylist
is supposed to be used for comments?
So we need to check that parentheses are balanced in comments.
I guess that's not a real problem.
See also "Wadler's Law on Language Design", cited here:
http://www.informatik.uni-kiel.de/~mh/curry/listarchive/0017.html

It seems that not all files in
http://www.lri.fr/~marche/wst2004-competition/tpdb/various/
follow the proposed syntax. (the rules are not embedded in (RULES ...) )

A very formal question, but just to make sure:
I guess we shall assume that there are nullary symbols in the signature,
even if they're not mentioned in the rules.
Otherwise, f(x) -> f(x) would be trivially terminating on ground terms,
because there are none.


Claude:

> ... So yes, your idea
> of asking of fixed number of examples from participants is
> interesting. We could ask to other persons as well.

Hypothetically, suppose the following:
at the workshop, someone proposes a TRS.
For that, one tool says YES, another tool says NO.
Which one gets the point? Assume the original proposer has disappeared,
the TRS has no obvious RPO, and no obvious infinite reduction,
and both the tools emit some obscure "certificates"
only meaningful to the respective authors
(but even they might not be able to verify them on the spot).

I wonder how the SAT contest organizers ( http://www.satlive.org/ )
verify their *negative* benchmarks. Compared to Termination,
they have the obvious advantage that SAT is in NP,
so they can require that anyone who submits a satisfiable formula,
has to submit proof as well. But since it's probably not in co-NP ...
It is interesting to read their benchmark submission guidelines
http://satlive.org/SATCompetition/2003/cfb.html
They even have a prize for the author of the smallest benchmark
that could not be decided by any of the programs. *I like this idea!*


> First, let's see if there is any tool able to answer NO. 

Matchbox can say NO (for strings, at the moment).


PS: Is there an online archive of this list's messages?

Best regards,
-- 
-- Johannes Waldmann,  Tel/Fax: (0341) 3076 6479 / 6480 --
------ http://www.imn.htwk-leipzig.de/~waldmann/ ---------