[Termination tools] inheritance of categories

[H. Zantema]

On Thu, 29 Apr 2004, Claude Marche wrote:

> You suggest in some sense to include SRSs as particular cases of
> TRSs. But there is not only one way to do it. For CiME, I simply
> considered a SRS as a TRS with unary function symbols, so that
> 
> a b c -> d e
> 
> becomes
> 
> a(b(c(x))) -> d(e(x))
> 
> but I could have done it differently, for example from right to left:
> 
> c(b(a(x))) -> e(d(x))
> 
> So, if a tool for TRS is also able to handle SRS syntax, of course it
> can compete in the 2 categories, but I don't see how I can make this
> automatic. 

The standard way is simply to transform a b c -> d e  to  
a(b(c(x))) -> d(e(x)). This is indeed different from 
c(b(a(x))) -> e(d(x)), just like the SRS  a b c -> d e  is 
syntactically different from  c b a -> e d.

So my proposal is to apply this basic transformation on all SRSs of the
SRS competition, and then apply all TRS tools on the resulting TRS's
(all having only unary symbols).

An alternative approach would be to apply the TRS tools both on the
TRS obtained by the basic transformation and its reversed counterpart.
I am not in favor of this: then the competition software takes over
this method of applying techniques on both versions while it could have
been implemented (and may be is implemented) in the tools themselves.


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