[Termtools] Suggestion for a new Category

[Georg Christian Moser]

Dear All,

in the name of Johannes Waldmann and mine, I would like to post
the following suggestion for a new category. Perhaps we can
discuss this matter in more detail in Hagenberg.

---

It is a  challenging topic to automatically determine  upper bounds on
the complexity of rewrite systems.  Here complexity is measured as the
maximal  length of derivations,  where either  no restrictions  on the
initial   terms  are   present  (derivational   complexity)   or  only
constructor   based  terms   are   considered  (runtime   complexity).
Additionally  one distinguishes between  complexities induced  by full
rewriting as  opposed to complexities induced  by specific strategies,
as for example innermost rewriting.

We  believe this  might be  a candidate  category to  be added  to the
competition,  provided we  have enough  (potential)  participants, and
provided  one can  come  up with  a  reasonable competition  semantics
specification and interesting problem sets.

There  are at  least two  independent implementations  that  can prove
polynomial termination on derivational complexity (one from Innsbruck,
one from Leipzig) so that looks like a good start. (Currently only the
tool  from  Innsbruck  can  handle runtime  complexity  and  innermost
rewriting.)

As  competition semantics,  we propose  to focus  on  polynomial upper
bounds. The current input format  could be kept, but the output format
adapted so  that additional  information on the  asymptotic complexity
(i.e.  big-Oh  format) is given.   These changes would  allow standard
termination provers to enter the  competition easily: It would only be
necessary   to  restrict  to   those  termination   techniques,  where
polynomial  (derivational  or runtime)  complexity  is induced.   (For
example   linear  match-bounded   TRSs   induce  linear   derivational
complexity.)

Of course this suggestion implies that the evaluation software
might have to be more complicated. On the other hand this seems to
be the most intuitive choice.

Georg Moser & Johannes Waldmann.