A Perron-Frobenius Theorem for Jordan Blocks for Complexity Proving
Jose Divasón, Sebastiaan Joosten, René Thiemann, Akihisa YamadaProceedings of the 16th International Workshop on Termination, pp. 30-34, 2018.
Abstract
We consider complexity proofs for rewrite systems that involve matrix interpretations. In order to certify these proofs, we have to validate polynomial bounds on the matrix growth of An for some non-negative real-valued square matrix A. Whereas our earlier certification criterion used algebraic number arithmetic in order to compute all maximal Jordan blocks, in this paper we present a Perron-Frobenius like theorem. Based on this theorem it suffices to just compute the Jordan Blocks of eigenvalue 1, which can easily be done. This not only helps to improve the efficiency of our certifier CeTA, but might also be used to actually synthesize suitable matrix interpretations.
BibTeX
@inproceedings{JDSJRTAY-ITP18,
title = {A {P}erron--{F}robenius Theorem for {J}ordan Blocks for Complexity Proving},
author = {Jose Divas\'on and Sebastiaan Joosten and Ren\'e Thiemann and Akihisa Yamada},
year = 2018,
booktitle = {Proceedings of the 16th International Workshop on Termination},
editor = {Salvador Lucas},
pages = {30--34},
url = {http://wst2018.webs.upv.es/wst2018proceedings.pdf}
}