Comments on the format of the termination problems of the TPDB

[Claude Marche]

>>>>> "Juergen" == Juergen Giesl <giesl at informatik.rwth-aachen.de> writes:

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

    Juergen> Here are my comments:

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

I think .pl is already the extension used in TPDB, and the usual one
anyway for Prolog programs. So it would be .trs, .srs and .pl if
nobody complains.

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

As I said before, these are perfectly allowed, and are meaningless for
tools reading them. Do we need to fix a convention on such comments ?
At least we could left that for the future.

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

This is indeed a difficult point. I would like to allow several VAR,
THEORY, RULES sections, because it allows to define TRSs in several
parts. So we need to fix a clear semantics. May be we can say that a
VAR decl somewhere completely hides the previous VAR decl (if any) ?
So that in

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

then the f in the first rule is function symbol, it is a variable in the
second rule, the y in the first rule is a variable, whereas it is a
constant in the second one. In other words the semantics would be:

  In a rule l -> r, an ident is assumed to be a function symbol,
  unless it is declared a variable in the previous VAR declaration. 

Perhaps its better than what is written in the current document,
because it may avoid to accidentally consider a constant as a
variable, just because it would have been declared a variable very
early in the file. As in :


(VAR f)

..... very long set of rules


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

Indeed, this semantics would be more closer to usual semantics of
quantifiers, or binders in general. 

It will also allow to concatenate .trs files without modifying the
semantics. 

Any comment ?

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

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

I strongly support this. This is why we wanted to left open the
theorydecl. 'A' for associative but non commutative, could be
interesting also. The only thing we need when adding a new theory is
to write the meaning somewhere, in future version of the common format
description. 

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

I agree it should be consistant. May I suggest to allow empty list of
id instead ? This is because I have in mind the possibility of having
TRSs which are automatically generated, say from Prolog programs, OBJ
programs, or whatever, and sometimes an automatic generation may
generate empty list of ids, and/or of rules. 

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

OK, one vote for option 1 then.

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

Sure.

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

Sure we need rules with epsilon in the rhs. (We may even accept epsilon
in the lhs, although we then know that it will never terminate...)

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

I agree.

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

Sure we need to define the semantics of strategy declarations. May be
we could allow both OUTERMOST and LEFTMOST_OUTERMOST. As for THEORY
declarations, the list of possible STRATEGY declarations should be
extensible. 

    Juergen> Let me also comment on Alfons' comments:

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

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

Let me argue in favor of (THEORY (AC +) (C *)). I think that when a
computer tool will read a toplevel declaration

(keyword ...)

where the keyword is different from VAR, THEORY, STRATEGY and RULES,
then it should be allowed to ignore the declaration, because it is
supposed to be irrelevant w.r.t. the reduction system defined in this
file, that is its termination does not depend on this declaration. On
the other hand, when a tool reads a declaration

(THEORY (thkeyword ...))

then it has to consider the thkeyword there, and if it is a keyword
that it cannot handle, such as AC for a tool that does not support
proving AC-termination, then the tool should give up saying 'I do not
support AC theory'

The same should apply the STRATEGY decl. (Except that when a tool
meets a STRATEGY decl that it does not handle, it can try to prove
termination under any strategy) 

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

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

I completely agree with Juergen, as I said in my previous message.

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

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

Yes. Anyway we could allow it !

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

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

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

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

    Juergen> As Claude wrote, linefeeds are not separators of rules, but have
    Juergen> 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).

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


I understand that option 2 to avoid introducing an extra special
symbol is not appreciated, because of less readable. But we may still
change "|" for some longer symbol like "=>". I have no strong
opinion. 
    >> 
    >> 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?

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



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