[Termination tools] SRS syntax

[H. Zantema]

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

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

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

		Best regards, Hans Zantema.

+--------------------------------------+-----------------------------+
|                                      |                             |
|   Dr Hans Zantema                    |   Hoofdgebouw   kamer 6.73  |
|   Faculteit Wiskunde en Informatica  |   tel (040)2472749          |
|   Technische Universiteit Eindhoven  |   fax (040)2468508          |
|   Postbus 513     5600 MB Eindhoven  |   e-mail  H.Zantema at tue.nl  |
|   The Netherlands                    |   www.win.tue.nl/~hzantema  |
|                                      |                             |
+--------------------------------------+-----------------------------+