Comments on the format of the termination problems of the TPDB

Aart Middeldorp Aart.Middeldorp at uibk.ac.at
Fri Nov 28 18:07:29 CET 2003


Dear all,

> 1) About the suffix for files I think we can agree:
> 
> .trs for TRS
> .srs for SRS
> .pl  for LP 

I'm a bit puzzled here: why have a special file suffix
for a subclass of TRSs whereas all extensions to the
basic TRS format (conditions, theories, strategies, etc.)
are supposed to be covered by .trs?

> 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 was hoping for some more discussion on this point
(in Valencia XML was not seriously discussed). Failing
that, I guess the only way forward is to continue with
the readable format, although I remain keen to develop
a suitable XML format.


> - We all agree in having separate syntax for SRS.

True, but why does that have to come with a change
in the file ending?

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

The (only) drawback with the current proposal for option 1
is that the sign '|' to separate the conditions from the
rule part is that it is symmetric. When faced with

/(y,y) -> 1 | >(y,0) -> true

it is not clear which part is the condition. So, although
I prefer option 1 above 2, a different (sequence of) symbol(s)
should be adopted.

-- Aart



More information about the Termtools mailing list