Skip to Content

Efficient certification of complexity proofs: formalizing the Perron–Frobenius theorem (invited talk paper)

Posted on

Authors:

  • Divasón, Jose
  • Joosten, Sebastiaan J. C.
  • Kuncar, Ondrej
  • Thiemann, René
  • Yamada, Akihisa

Published in: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs pp 2–13

DOI: 10.1145/3167103

Paper

Abstract:

Matrix interpretations are widely used in automated complexity analysis. Certifying such analyses boils down to determining the growth rate of $A^n$ for a fixed non-negative rational matrix $A$. A direct solution for this task involves the computation of all eigenvalues of $A$, which often leads to expensive algebraic number computations.

In this work we formalize the Perron–Frobenius theorem. We utilize the theorem to avoid most of the algebraic numbers needed for certifying complexity analysis, so that our new algorithm only needs the rational arithmetic when certifying complexity proofs that existing tools can find. To cover the theorem in its full extent, we establish a connection between two different Isabelle/HOL libraries on matrices, enabling an easy exchange of theorems between both libraries. This connection crucially relies on the transfer mechanism in combination with local type definitions, being a non-trivial case study for these Isabelle tools.

BibTeX entry:

@inproceedings{Divason18a,
 abstract = {Matrix interpretations are widely used in automated complexity analysis. Certifying such analyses boils down to determining the growth rate of $A^n$ for a fixed non-negative rational matrix $A$. A direct solution for this task involves the computation of all eigenvalues of $A$, which often leads to expensive algebraic number computations.

In this work we formalize the Perron--Frobenius theorem. We utilize the theorem to avoid most of the algebraic numbers needed for certifying complexity analysis, so that our new algorithm only needs the rational arithmetic when certifying complexity proofs that existing tools can find. To cover the theorem in its full extent, we establish a connection between two different Isabelle/HOL libraries on matrices, enabling an easy exchange of theorems between both libraries. This connection crucially relies on the transfer mechanism in combination with local type definitions, being a non-trivial case study for these Isabelle tools.},
 author = {Jose Divas{\'o}n and Sebastiaan Jozef Christiaan Joosten and Ondrej Kuncar and Ren{\'e} Thiemann and Akihisa Yamada},
 bdsk-url-1 = {https://doi.org/10.1145/3167103},
 booktitle = {Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs},
 doi = {10.1145/3167103},
 language = {English},
 month = {Jan},
 pages = {2--13},
 title = {Efficient certification of complexity proofs: formalizing the Perron--Frobenius theorem (invited talk paper)},
 year = {2018}
}