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

Jose Divasón, Sebastiaan Joosten, Ondrej Kuncar, René Thiemann, Akihisa Yamada

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademic

    4 Citations (Scopus)
    54 Downloads (Pure)

    Abstract

    Matrix interpretations are widely used in automated complexity analysis. Certifying such analyses boils down to determining the growth rate of An 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.

    Original languageEnglish
    Title of host publicationProceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs
    EditorsAmy Felty, June Andronick
    Pages2-13
    Number of pages12
    ISBN (Electronic)9781450355865
    DOIs
    Publication statusPublished - 8 Jan 2018
    Event7th ACM SIGPLAN International Conference on Certified Programs and Proofs 2018 - Los Angeles, United States
    Duration: 8 Jan 20189 Jan 2018
    Conference number: 7
    https://conf.researchr.org/home/CPP-2018

    Conference

    Conference7th ACM SIGPLAN International Conference on Certified Programs and Proofs 2018
    Abbreviated titleCPP 2018
    CountryUnited States
    CityLos Angeles
    Period8/01/189/01/18
    Internet address

    Fingerprint

    Dive into the research topics of 'Efficient certification of complexity proofs: formalizing the Perron--Frobenius theorem (invited talk paper)'. Together they form a unique fingerprint.

    Cite this