[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |
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.
[Submit a comment] [RTALooP home] [Index] [Previous] [Next] | [Postscript] [PDF] [BibTeX Source] [LaTeX Source] |