\documentclass{rtaloop}


\begin{document}
\begin{problem}{Georg Moser and Harald Zankl}{}{2010}

  \begin{abstract}
    Give a complete (resource free) characterisation of rewrite systems with
    polynomial derivational complexity.
  \end{abstract}
  
  It is well-known that well-founded monotone algebras form a complete
  characterisation for termination while such a result is currently
  unknown for polynomial derivational complexity. The notion of
  \emph{resource freeness} is borrowed from implicit computational
  complexity theory. Here it refers to characterisations devoid of
  \emph{direct} references to polynomial derivational complexity.

  Currently suitably restricted matrix interpretations
  (see~\cite{moser08fsttcs,waldmann10rta,neurauter10lpar}) form
  \emph{the} method for proving polynomial upper bounds on the
  derivational complexity.  Thus it is perhaps important to emphasise
  that matrix interpretations as studied in~\cite{endrullis08jar} are
  not sufficient as a starting point to solve the problem. Consider
  the one-rule TRS $\mathsf{g}(x,x) \to
  \mathsf{g}(\mathsf{a},\mathsf{b})$.  This TRS has linear
  derivational complexity, but no compatible matrix interpretation can
  exist.


\end{problem}


\end{document}