Paper Info
Title
Matrices, Jordan Normal Forms, and Spectral Radius Theory.
Abstract
Matrix interpretations are useful as measure functions in termination 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 prove the result that every complex matrix has a Jordan normal form by means of two algorithms: we first convert matrices into similar ones via Schur decomposition, and then apply a second algorithm which converts an upper-triangular matrix into Jordan normal form. We further showed uniqueness of Jordan normal forms which then gives rise to a modular algorithm to compute individual blocks of a Jordan normal form. The whole development is based on a new abstract type for matrices, which is also executable by a suitable setup of the code generator. It completely subsumes our former AFP-entry on executable matrices [6], and its main advantage is its close connection to the HMArepresentation which allowed us to easily adapt existing proofs on determinants. All the results have been applied to improve CeTA [7, 1], our certifier to validate termination and complexity proof certificates.
Year
Venue
Field
2015
Archive of Formal Proofs
Uniqueness,Spectral radius,Matrix (mathematics),Pure mathematics,Schur decomposition,Jordan normal form,Mathematics,Jordan matrix,Abstract type,Bounded function
DocType
Volume
Citations 
Journal
2015
2
PageRank 
References 
Authors
0.38
4
2
Name
Order
Citations
PageRank
René Thiemann198469.38
Akihisa Yamada 00022347.11