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

  1. Divasón, J. 3
  2. Joosten, S. 5
  3. Kunčar, O. 2
  4. Thiemann, R. 4
  5. Yamada, A. 1
  1. 1 National Institute of Informatics
    info

    National Institute of Informatics

    Tokio, Japón

    ROR https://ror.org/04ksd4g47

  2. 2 Technical University Munich
    info

    Technical University Munich

    Múnich, Alemania

    ROR https://ror.org/02kkvpp62

  3. 3 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

  4. 4 University of Innsbruck
    info

    University of Innsbruck

    Innsbruck, Austria

    ROR https://ror.org/054pv6659

  5. 5 University of Twente
    info

    University of Twente

    Enschede, Holanda

    ROR https://ror.org/006hf6230

Mostrar afiliaciones +
Libro:
CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Co-located with POPL 2018

ISBN:

Año de publicación: 2018

Volumen: 2018-January

Páginas: 2-21

Congreso: 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018

Tipo: Aportación congreso

DOI: 10.1145/3167103 SCOPUS: 2-s2.0-85044262846 GOOGLE SCHOLAR

Resumen

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. © 2018 Copyright held by the owner/author(s).