A formalization of the Berlekamp-Zassenhaus factorization algorithm

  1. Divasón, J. 1
  2. Joosten, S. 2
  3. Thiemann, R. 2
  4. Yamada, A. 2
  1. 1 Universidad de La Rioja
    info

    Universidad de La Rioja

    Logroño, España

    ROR https://ror.org/0553yr311

  2. 2 University of Innsbruck
    info

    University of Innsbruck

    Innsbruck, Austria

    ROR https://ror.org/054pv6659

Libro:
CPP 2017 - Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs

ISBN: 9781450347051

Año de publicación: 2017

Páginas: 17-29

Tipo: Capítulo de Libro

DOI: 10.1145/3018610.3018617 SCOPUS: 2-s2.0-85014995357 WoS: WOS:000405305600004 GOOGLE SCHOLAR

Resumen

We formalize the Berlekamp-Zassenhaus algorithm for factoring square-free integer polynomials in Isabelle/HOL. We further adapt an existing formalization of Yun's square-free factorization algorithm to integer polynomials, and thus provide an efficient and certified factorization algorithm for arbitrary univariate polynomials. The algorithm first performs a factorization in the prime field GF(p) and then performs computations in the ring of integers modulo pk, where both p and k are determined at runtime. Since a natural modeling of these structures via dependent types is not possible in Isabelle/HOL, we formalize the whole algorithm using Isabelle's recent addition of local type definitions. Through experiments we verify that our algorithm factors polynomials of degree 100 within seconds. © 2017 ACM.