Format of the termination problems of the TPDB

[Claude Marche]

Dear Alfons, and others,

>>>>> "Alfons" == Alfons Geser <geser at nianet.org> writes:

    Alfons> Dear Albert,
    Alfons> Dear committee members,

    Alfons> Thank you for the proposal. Albert and Claude, I sure appreciate your
    Alfons> effort.

    Alfons> In contrast to Albert, I feel that even though we have agreed on a few
    Alfons> basic items in Valencia, there are some more that need to be
    Alfons> discussed. Before we start voting, let us debate what we could do
    Alfons> differently.  Please, let us not haste the decisions.

Please allow me first to recall what is the purpose of this format: we
need a common format for definition of TRSs and SRSs, to be used for
files in the TPDB (Termination Problem Data Base), a format that can
be understood by any termination tool without too much implementation
effort, so that such a tool can run the problems of TPDB.

But any termination tool can have its own input format. So it is not a
main goal of the common format to provide a very user-friendly
syntax. (In particular I think I will never type a file in this format
myself, I will always output such a file from the internal format of
my own tool).

For such a goal, an XML format could have been also quite good,
however in Valencia we discussed about that and the general feeling
was it was better to keep a human readable format.

Now let me comment on your comments


    Alfons> Here are my comments:

    Alfons> 1) I support the suggestion to keep a separate syntax for string
    Alfons> rewriting systems.

I think nobody will go against, at least Albert and I agreed it
should exist. 

    Alfons> 2) I suggest to enforce a header, e.g. PROBLEM blabla, that introduces
    Alfons> the same name as the file blabla.trs. This is useful information if
    Alfons> you print the file.

In the current format, such a PROBLEM is perfectly allowed, and you
can put any information you like in it. But I don't see why we should
enforce it, since it gives no information to the problem itself, I
mean information that a tool can use.

    Alfons> 3) We need a construct for comments. What about "#" at the beginning
    Alfons> of the line?

(COMMENT blabla) is allowed, (# blabla blabla) is allowed, etc. But as
I said before, this is not the main goal of this format to be written
by hand directly.

Anyway, such an addition does not add ambiguity, so can be added easily.

    Alfons> 4) Instead of (THEORY (AC +) (C *)) I prefer (ACTHEORY +) (CTHEORY *)
    Alfons> or so, avoiding the nesting.

But (THEORY ...) allows to extend easily the set of theories. And
again, this is of very small importance for a format whose main goal
is not to be written by hand.

    Alfons> 5) The parentheses around vardecl, theorydecl, rulesdecl, etc. are
    Alfons> spurious.

If things remain unambiguous, I would agree, but I'am not sure. I will check.

    Alfons> 6) As we use commas as separators elsewhere, let us use commas to
    Alfons> separate ids everywhere.

In Valencia, I suggested to write (f a b c) instead of f(a,b,c), to
completely remove the use of commas, and have a completely lisp-like
syntax. but this was not appreciated. Now, I don't like adding more
commas elsewhere. Please others, give your opinions.

    Alfons> 7) I understand that the notation f() is disallowed.

Yes, but maybe we can add it, if you want.

    Alfons> 8) The definition of "id" is too liberal. Who wants to read stuff like
    Alfons> &%(*&_,*^) ? We improve readability by sticking to the regular
    Alfons> expression [A-Za-z][A-Za-z0-9_]* .

At least I like to use +, *, and such. We could of course restrict
allowed identifiers, it changes absolutely nothing to the format
itself, I mean the grammar is unambiguous like this.

    Alfons> 9) otherkeyword should also be in [A-Z]^+

Why being restrictive without any reason ?

    Alfons> 10) I know that I have agreed to it, but I feel that linefeeds as
    Alfons> separators of rules are not a good choice. For instance, how do you
    Alfons> break a long rule, given that a linefeed means the end of
    Alfons> the rule? 

You probably miss something, linefeed are separators of lexical
tokens, just like space or tab, and you are perfectly allowed to split
a long rule into several lines.

    Alfons> Linefeeds have been separators in FORTRAN, and have been replaced by
    Alfons> the semicolon in ALGOL with great success.

:-) Fortunately, we don't have to put the problems of TPDB on those
cards with holes, you know (I don't know the english name for them, it
is "cartes perforées" in french).

    Alfons> 11) The symbol "|" is problematic as it is used elsewhere for "or". What
    Alfons> about the keyword "IF" or the symbol "=>" (with term and listofconditions
    Alfons> swapped).

I completely agree. And I see you also like identifiers outside
[A-Za-z][A-Za-z0-9_]* 

However, IF is also quite common. What do you think about the variant
with parentheses only ? (It's my prefered choice.)

    Alfons> 12) The comma in a listofconditions means "and", so why not replace it
    Alfons> by "&" or "AND"?  Actually a conjunction a -><- b, c -><- d can be
As before, it is nice to be able to use "&" and "AND" as identifiers.
In the second variant, commas are simply absent, so may be you would
like it ?

    Alfons> replaced by f(a,c) -><- f(b,d) with a free function symbol f. So do we
    Alfons> want conjunctions as connectives here anyway?

Sure, we need conjonctions, the scheme you propose is certainly not
enough, we need to mix -><- and -> conditions, we need conditions
where some variables are bounded only in previous conditions:


f(X) -> g(X,Y) if h(X) -> Z , i(X,Z) -> Y

so even the order of conditions is itself important.

    Alfons> Finally let me suggest to compose a bison input file for the syntax,
    Alfons> in order to enable tool developers to write their parsers, and to
    Alfons> check new examples for syntax before adding them to the library.

Indeed, I already have an ocamlyacc parser, which I can provide, and
writing a bison file from it would be straightforward.

    Alfons> Please let me know your point of view.

    Alfons> Kind Regards,
    Alfons> Alfons

Yes, others, please, give us your point of view, at least "I don't
mind", so that we can have this common format fixed as soon as
possible. 

- Claude

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