[Termination tools] Rules of the WST competition

[Claude Marche]

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

    H> I saw that in the mean time CiME has been included in the test results
    H> page in the SRS category.

    H> More general I propose that for every category X being a subcategory
    H> of Y, all tools for category Y automatically apply for category X.

    H> So tools for context sensitive rewriting and rewriting modulo AC
    H> are also applied on the set of systems for (plain vanille) term 
    H> rewriting, and tools for term rewriting are also applied on the
    H> set of string rewriting systems. The extra work for doing this is
    H> hardly anything (a script for transforming SRS syntax to TRS syntax
    H> is trivial to write and probably already available). I think the
    H> result will be of interest. For instance, some people said to expect
    H> that the match-bound technique from Matchbox is quite orthogonal to
    H> the techniques of dependency pairs and path orders as they are applied
    H> in term rewriting tools. If the above proposal is followed, such a
    H> claim can be verified from the results of the competition.

    H> Do you agree? Or are there reasons for not doing so?

For the moment, there only 2 categories: TRS and SRS. So a tool for
context-sensitive rewriting (for example) will be applied to all TRS
examples. 

The distinction between the 2 categories is only due to the difference
in the input syntax. 

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. 



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