The Factorization Algorithm of Berlekamp and Zassenhaus

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

ISSN: 2150-914x

Année de publication: 2016

Pages: 1-481

Type: Article

GOOGLE SCHOLAR lock_openAccès ouvert editor
Dépôt institutionnel: lock_openAccès ouvert Editor

Résumé

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.