Format of the termination problems of the TPDB

[Alfons Geser]

Dear Albert,
Dear committee members,

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

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

Here are my comments:

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

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

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

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

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

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

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

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

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

10) I know that I have agreed to it, but I feel that linefeeds as
separators of rules are not a good choice. For instance, how do you
break a long rule, given that a linefeed means the end of the rule? 
Linefeeds have been separators in FORTRAN, and have been replaced by
the semicolon in ALGOL with great success.

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

12) The comma in a listofconditions means "and", so why not replace it
by "&" or "AND"?  Actually a conjunction a -><- b, c -><- d can be
replaced by f(a,c) -><- f(b,d) with a free function symbol f. So do we
want conjunctions as connectives here anyway?

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

Please let me know your point of view.

Kind Regards,
Alfons