The Factorization Algorithm of Berlekamp and Zassenhaus

  1. Jose Divasón,
  2. Akihisa Yamada
  3. Sebastiaan Joosten
  4. René Thiemann
Revista:
Archive of Formal Proofs

ISSN: 2150-914x

Año de publicación: 2016

Páginas: 1-481

Tipo: Artículo

GOOGLE SCHOLAR lock_openAcceso abierto editor
Repositorio institucional: lock_openAcceso abierto Editor

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 integer ring modulo p^k, 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.