cl-banner

Revisiting Matrix Interpretations for Polynomial Derivational Complexity of Term Rewriting

Friedrich Neurauter, Harald Zankl, and Aart Middeldorp

Proceedings of the 17th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-17), Lecture Notes in Computer Science (Advanced Research in Computing and Software Science) 6397, pp. 550 – 564, 2010.

Abstract

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.

 

  PDF |    doi:10.1007/978-3-642-16242-8_39  |  © Springer

BibTeX 

@inproceedings{FNHZAM-LPAR17,
author = "Friedrich Neurauter and Harald Zankl and Aart Middeldorp",
title = "Revisiting Matrix Interpretations for Polynomial
Derivational Complexity of Term Rewriting",
booktitle = "Proceedings of the 17th International Conference on Logic
for Programming, Artificial Intelligence, and Reasoning",
series = "Lecture Notes in Computer Science (Advanced Research in
Computing and Software Science)",
volume = 6397,
pages = "550--564",
year = 2010
}
Nach oben scrollen