[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]

Problem #107

Originator: Georg Moser and Harald Zankl
Date: 2010

Summary: Give a complete (resource free) characterisation of rewrite systems with polynomial derivational complexity.

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 resource freeness is borrowed from implicit computational complexity theory. Here it refers to characterisations devoid of direct references to polynomial derivational complexity.

Currently suitably restricted matrix interpretations (see [MSW08, Wal10, NZM10]) form the method for proving polynomial upper bounds on the derivational complexity. Thus it is perhaps important to emphasise that matrix interpretations as studied in [EWZ08] are not sufficient as a starting point to solve the problem. Consider the one-rule TRS g(x,x) → g(a,b). This TRS has linear derivational complexity, but no compatible matrix interpretation can exist.

References

[EWZ08]
Joerg Endrullis, Johannes Waldmann, and Hans Zantema. Matrix interpretations for proving termination of term rewriting. Journal of Automated Reasoning, 40(2-3):195–220, 2008.
[MSW08]
Georg Moser, Andreas Schnabl, and Johannes Waldmann. Complexity analysis of term rewriting based on matrix and context dependent interpretations. In Ramesh Hariharan, Madhavan Mukund, and V Vinay, editors, Proceedings of the IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2008), volume 2 of Leibniz International Proceedings in Informatics (LIPIcs), pages 304–315. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2008.
[NZM10]
Friedrich Neurauter, Harald Zankl, and Aart Middeldorp. Revisiting matrix interpretations for polynomial derivational complexity of term rewriting. In 17th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 6397 of ARCoSS, October 2010. To appear.
[Wal10]
Johannes Waldmann. Polynomially bounded matrix interpretations. In Christopher Lynch, editor, Proceedings of the 21st International Conference on Rewriting Techniques and Applications, volume 6 of Leibniz International Proceedings in Informatics (LIPIcs), pages 357–372, Edinburgh, UK, July 2010. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.

[Submit a comment] [RTALooP home] [Index] [Previous] [Next] [Postscript] [PDF] [BibTeX Source] [LaTeX Source]