Comments on the format of the termination problems of the TPDB

[Albert Rubio]

Dear all,

first of all, thanks for all contributions to the discussion, and
especially to Alfons who started the discussion when we began to be a
little worried. Second, sorry for my late reaction.

I'll try to go from the more general comments to de more specific, and
try to fix the potential points of agreement. Although we are not in a
hurry it would be better if we start to converge.


1) About the suffix for files I think we can agree:

.trs for TRS
.srs for SRS
.pl  for LP


2) About XML or a readable format.

I don't think we will find a full agreement on that. In fact, as
Claude said, in Valencia there was a majority agreement of not having
XML (only the SRS people was against this).

I'm really in favor of having a readable format, which may become a
kind of standard for giving examples, even if when writing examples in
e.g. papers, some part of the syntax (which is necesary to have an
unambiguous grammar) is not used, like e.g. some parentheses.  On the
other hand I can see potential usefulnes of using a standard format
like XML.

Instead of discussing about which is better, there is a third
possibility which is to have both cohexiting. There is no major
problem on having each example in both formats a readable one (with
suffix .trs, .srs or .pl) and an XML one (with suffix .xml). If we
agree in the readable one we can extract an XML on from it (like Aart
started). We can easily obtain one format from the other in the
database.

If we can agree in this third possibility we can go on in fixing the
readable format and later define the XML format.


3) About the readable format.


- We all agree in having separate syntax for SRS.

- I think we can all agree in restricting the definition of
  identifiers, taking e.g Aart's suggestion

> a regular expression that includes the common
> mathematical symbols but forbids expressions like "&%(*&_,*^)".

  Similarly for otherkeywords, combining Alfons and Juergen proposals:

  a regular expresion using capital letters plus numbers and some
  extra symols like e.g. '_'

- Like Juergen I prefer option 1 for conditional rules, mainly for
  readability reasons (which is the main reason of this format, as
  said before).


Before starting to comment on other's comments I want to stress the
fact that we have to firts agree on the syntax or on the style of the
syntax in order to go on. If you all agree, with all comments
received until the end of the week, we can produce a second version of
the proposal to be considered. BTW. do not forget to vote on one (or
none) of the two options for conditional rules. 


- Regarding Alfons' comments:

  Comments 2 to 5. I fully agree with Claude's comments. In fact, that
  was part of our discussion before sending you the proposal.

  Comment 7, Juergen's comment is the reason we
  disallowed the possibility of having f().

  Comments 6 and 10 on the use of commas. I just want to recall that
  we explicitely agreed in Valencia on not having commas ending
  rules. There is no need to use commas and the presentation is
  cleaner.

  Comment 11. As Claude and Juergen commented there
  may be conflicts with any reasonable alternative to "|" in the
  conditional rules so I keep suggesting to use it.

  Similarly for comment 12 on the use of an alternative to "," for
  conjunction of conditions.

- Regarding Juergen's comments. Since they where not numbered I'll
  reproduce a part of each one.

> one could
> think about fixing some of the otherdecl's....

  Again I agree with Claude in the fact that all this is
  allowed. However if wanted we can reserve some keywords for Comment
  or Bibtex or Title..., but as Claude said this would mean that we
  need to impose special syntactic and semantical conditions on the
  contents of the text associated to those keywords. As Claude, I
  think this can be done in a second refinement.


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

and the comment by Claude pointing the possibility to have things
like:

> (VAR x y)
> (RULES f(x,y) -> x)
> (VAR f z)
> (RULES y(f,z) -> f)

I see Juergen's point but I think Claudes proposal is a bit too much,
at least concerning readability.

So I suggest to permit multiple non-contradictory declarations.
Regarding the intersting Claude's comment on concatenation of files,
maybe we need to add a new construction of the kind:

(USE idlist)

or the like, in order to include hierarchicaly already existing
examples. And then fix the semantics and the (visibility) conditions
for the union, etc. Again I think this can be left for a second round.


> I think we should add a format for rewriting
> modulo arbitrary equations (not just AC)...

I also support this proposal.

> 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 agree we need to be consistent, but like Claude I rather prefer to
allow the user to have empty lists everywhere (it is more general and
it is harmless).

> in your grammar you can't formulate rules with the
> empty word on the right-hand side. 

I agree with Claude that it may happend, so we do not restrict it.


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

I agree but we have to give a different treatment to strategies like
INNERMOST that only need a list of identifier and strategies like
CONTEXTSENSITIVE that need a list of "identifiers plus list of
numbers". In fact it is the same as you have proposed for know thories
like AC,C.. and equational theories defined by the user.


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

As Claude answered, we have to fix that, but somehow it does not
affect to the syntax of the format which is the first thing we have to
agree on.


That's all,

Albert