[Termtools] Suggestion for a new Category

[Salvador Lucas]

Dear all,

Unfortunately, I will not be in Hagenberg, but I fully support your
proposal.

Best regards,

Salvador.

Georg Christian Moser escribió:
> 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.
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/mailman/listinfo/termtools
>