[Termination tools] SRS syntax

[Claude Marche]

Dear Hans,

First, apparently your subscription to the list did not work, your
messages are rejected. I guess you don't received the messages from
others, right ? Could you please do it again :

send a mail to 

  majordomo at lri.fr 

with

  subscribe termtools

in the body of the message.

>>>>> "Hans" == H Zantema <hzantema at win.tue.nl> writes:

    Hans> On Wed, 10 Mar 2004, Claude Marche wrote:
    >> >>>>> "Johannes" == Johannes Waldmann <waldmann at imn.htwk-leipzig.de> writes:
    >> 
    Johannes> what about:
    Johannes> ( RULES "aabb" -> "bbbaaa" "c" -> "" )
    >> 
    Johannes> advantages:
    Johannes> * follows TRS syntax, needs no delimiters (+)
    Johannes> * need no special provision for empty string
    >> 
    Johannes> disadvantage:
    Johannes> * restricted to "one-letter letters"
    >> 
    Johannes> (+) implicit delimiting is rather a design flaw of the TRS syntax :-)
    >> 
    >> As I said before, I need more than one-letter symbols, like q1 q2, or
    >> a1, a2, so my preference remains 
    >> 
    >> ( RULES a a b b -> b b b a a a, c -> )

    Hans> I can agree with this syntax, as long as the symbols are single letters.
    Hans> Typically in TORPA replacing a by A is done for dependency pairs, and 
    Hans> replacing a by a0 and a1 is done for semantic labelling. It would be 
    Hans> possible to modify the code in such a way that it can handle symbols of 
    Hans> more than one letter, but then the resulting proofs may be less readable,
    Hans> and this modification will be quite boring. I never saw SRSs for which
    Hans> 26 symbols were not sufficient. 

    Hans> I think it is much easier to replace q1 and q2 by single letters in
    Hans> these few examples then to change all code to accept this. In this way
    Hans> blanks may be ignored, and we are not forced to follow the unusual convention
    Hans> to write blanks between consecutive symbols in a string.

    Hans> 		Best regards, Hans Zantema.


Please look at 

  http://www.lri.fr/~marche/wst2004-competition/tpdb/SRS/

there is already an example with 15 symbols: a srs representing the
permutation group S6. I plan to add systems for S7, S8, etc, which
will have 21, 28, etc symbols (this is why I would like to allow the
syntax with exponents...)

I think one of the interesting issue in this competition is to see how
tools scale up, when working on larger and larger examples.

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