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.