CPP 2016
Mon 18 - Tue 19 January 2016 St. Petersburg, Florida, United States
co-located with POPL 2016
Mon 18 Jan 2016 17:00 - 17:30 at Room St Petersburg II - Session 4: Mathematics

In automated complexity analysis of term rewriting, estimating the growth rate of the values in A n – for a fixed matrix A and increasing n – is of fundamental interest. This growth rate can be exactly characterized via A’s Jordan normal form (JNF). We formalized 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 admits to conveniently work with block matrices. Besides the mentioned complexity result, we formalize Gram-Schmidt’s orthogonalization algorithm and 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.