Comments on the format of the termination problems of the TPDB

[Juergen Giesl]

Dear all,

first of all, thanks a lot to Albert and Claude for
putting the draft together!

Here are my comments:

- We should fix a suffix for files in the
   different formats. I guess we're going to
   use .trs for TRSs and .srs for SRSs, but
   what are we going to use for logic programs?
   I could think of .pl or .lp?

- As discussed by Alfons and Claude, one could
   think about fixing some of the otherdecl's.
   I would suggest to add commentdecl (for comments),
   titledecl (for the title of the examples),
   and bibdecl (for a reference in bibtex-format
   describing the source of the example).

- If it's really allowed to have several VAR-,
   THEORY-, and RULES-declarations, then I would
   propose to permit the repeated declarations of
   the same variables. The reason is that then
   one could write files where all variables of
   a certain bunch of rules (defining one function)
   are declared just before the rules. Clearly,
   typical variable names like "x" will be used
   in many rules.

- I think we should add a format for rewriting
   modulo arbitrary equations (not just AC). My
   proposal it to extend the rule for thdecl
   as follows:

	thdecl := (thkeyword idlist) | (EQ eqlist)
  	eqlist := equation | equation eqlist
	equation := term = term

- I don't understand why you permit an empty listofrules,
   whereas an idlist or a listofthdecl may not be empty.
   I would suggest to disallow empty lists of rules.

- I like option 1 for CTRSs more than option 2.
   Option 2 is very LISP-like and in my opinion, hard
   to read for the human (unless the human is used
   to program in LISP or Scheme).

- Sometimes you write "empty" and sometimes you write
   "epsilon" in the grammar rules. I would propose to
   replace all "empty"s by "epsilon".

- I agree with having a special format for SRSs. However,
   in your grammar you can't formulate rules with the
   empty word on the right-hand side. My proposal is to
   reformulate the rules as follows:
	
	rule := word -> word | word -> emptyword
	word := id | id word

- Concerning the format for strategies, why don't we
   combine them in a strategydecl of the form
   (STRATEGY listofstrategydecl)? This would then
   be analogous to the way theories are treated.

- What is the meaning of the "outermost" strategy?
   Is it "leftmost outermost" or termination under every
   outermost reduction? (The semantics of these keywords
   need to be fixed in order to compare the performance of
   termination provers on such examples.)

Let me also comment on Alfons' comments:

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

But otherwise, one has all informations about
theories together. But I don't have a strong opinion
about that. We should just treat theories and strategies
in an analogous way.


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

We don't use commas for separating rules, for example. So why
introduce unnecessary syntax?

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

This notation is unnecessary since variables are declared
and so there is clear distinction between constants and variables.

 >
 > 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_]* .

I agree with Claude that some extra symbols like +, *, ... should
be permitted.

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

I think numbers and some extra symbols should be allowed.

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

As Claude wrote, linefeeds are not separators of rules, but have
no influence on the syntax.


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

I think, almost every other symbol has also some extra meaning. So I
have nothing against "|" (but I have no strong opinion on this).


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

I'm in favor of conjunctions since (as Claude wrote) the order
of the conditions is important and it increases readibility. I find
comma more readable than & or AND.


Best Regards
Juergen