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

[Claude Marche]

>>>>> "Johannes" == Johannes Waldmann <waldmann at imn.htwk-leipzig.de> writes:

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

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

OK, please send me the requested information (URL, description, etc.)
as soon as possible.

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

Indeed, I would like to have a version of your tools as soon as
possible, so that I can check if I am able to run it. You could send
me a "final" version later (say, in may), for the real participation
to the competition.


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

No, it is your own job to find the best settings. The idea is that
your tool might be distributed to naive users, who will use the
default settings, and the competition will evaluate your tool under
this context.

    Johannes> What kind of GNU/Linux system will be used?
    Johannes> Possibly there are versioning problems for DLLs
    Johannes> (like, SuSE 8.1 has older libc than SuSE 8.2)

Good question. It will be a Debian/Woody, so a quite old version of
libc, I guess. If I'm not wrong it is a libc 6, version 2.2.5

You can send a copy of your tool so that I can test. If it does not
work, you will need to provide a statically linked executable
(something like gcc -static, I am not sure)

    Johannes> How much main memory can a program get?

Good question: 1 Gbyte

    Johannes> In the grammar,  decl ::= id anylist
    Johannes> is supposed to be used for comments?
    Johannes> So we need to check that parentheses are balanced in
    Johannes> comments.

Yes. Please notice that there is a tool to check the syntax of TRS
files, in the Web page, 

http://www.lri.fr/~marche/wst2004-competition/tpdb/tools/

you will find a yacc grammar for them.

    Johannes> I guess that's not a real problem.
    Johannes> See also "Wadler's Law on Language Design", cited here:
    Johannes> http://www.informatik.uni-kiel.de/~mh/curry/listarchive/0017.html

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

Yes. I'm using the tool above to check their conformance, and I need
time to make the necessary corrections. 

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

Yes


    Johannes> Claude:

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

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

This is why I would like to run the tools a bit before the workshop,
so that we have time to solve such possible problems. Generally
speaking, a tool should answer YES or NO on the first line of their
answer, but more lines should be used to give some evidence/trace of
the answer, so we can check by eyes.

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

Generally speaking, I think the main goal of such a competition is to
see what are the important issues to solve for the practice of
automatically proving termination. So yes, examples that cannot be
decided by any tool are very interesting.

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

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

Great, I like that. I would like to have a similar ability for
TRSs/Logic programs.

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

Unfortunately, I think the list has not been configured to keep an
archive. I will see what I can do. At least I have a copy of all
messages so far, which is not very much.

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

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