Paper Info
Title
Formalizing jordan normal forms in Isabelle/HOL.
Abstract
In automated complexity analysis of term rewriting, estimating the growth rate of the values in the k-th power of a matrix A – for fixed A and increasing k – is of fundamental interest. This growth rate can be exactly characterized via A’s Jordan normal form (JNF). We formalize this result in our library IsaFoR and our certifier CeTA, and thereby improve the support for certifying polynomial bounds derived by (untrusted) complexity analysis tools. To this end, we develop a new library for matrices that allows us to conveniently work with block matrices. Besides the mentioned complexity result, we formalize Gram-Schmidt’s orthogonalization algorithm and the Schur decomposition in order to prove existence of JNFs. We also provide a uniqueness result for JNFs which allows us to compute Jordan blocks for individual eigenvalues. In order to determine eigenvalues automatically, we moreover formalize Yun’s square-free factorization algorithm.
Year
DOI
Venue
2016
10.1145/2854065.2854073
CPP 2016: Certified Proofs and Programs St. Petersburg FL USA January, 2016
Keywords
Field
DocType
matrix theory, Jordan normal form, Isabelle/HOL, complexity
HOL,Polynomial,Matrix (mathematics),Computer science,Algorithm,Factorization,Rewriting,Schur decomposition,Jordan normal form,Eigenvalues and eigenvectors
Conference
ISBN
Citations 
PageRank 
978-1-4503-4127-1
6
0.52
References 
Authors
15
2
Name
Order
Citations
PageRank
René Thiemann198469.38
Akihisa Yamada 00022347.11