Matrices, Jordan Normal Forms, and Spectral Radius Theory.
René Thiemann, Akihisa Yamada · 2015
Matrix interpretations are useful as measure functions in termina-tion proving. In order to use these interpretations also for complexity analysis, the growth rate of matrix powers has to examined. Here, we formalized an important result of spectral radius theory, namely that the growth rate is polynomially bounded if and only if the spectral radius of a matrix is at most one. To formally prove this result we first studied the growth rates of matrices in Jordan normal form, and partially prove the result that every complex matrix has a Jordan normal form: we are restricted to upper-triangular matrices since we have not yet formalized the Schur decomposition. The whole development is based on a new abstract type for matri-ces, which is also executable by a suitable setup of the code generator. It completely subsumes our former AFP-entry on executable matri-