Sciweavers

LPAR
2010
Springer

Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting

13 years 1 months ago
Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting
Matrix interpretations can be used to bound the derivational complexity of term rewrite systems. In particular, triangular matrix interpretations over the natural numbers are known to induce polynomial upper bounds on the derivational complexity of (compatible) rewrite systems. Using techniques from linear algebra, we show how one can generalize the method to matrices that are not necessarily triangular but nevertheless polynomially bounded. Moreover, we show that our approach also applies to matrix interpretations over the real (algebraic) numbers. In particular, it allows triangular matrix interpretations to infer tighter bounds than the original approach. Key words: derivational complexity, polynomial matrix interpretations
Friedrich Neurauter, Harald Zankl, Aart Middeldorp
Added 14 Feb 2011
Updated 14 Feb 2011
Type Journal
Year 2010
Where LPAR
Authors Friedrich Neurauter, Harald Zankl, Aart Middeldorp
Comments (0)