The Factorization Algorithm of Berlekamp and Zassenhaus

Jose Divasón 🌐, Sebastiaan J. C. Joosten 📧, René Thiemann 🌐 and Akihisa Yamada 📧

October 14, 2016

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

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.

License

BSD License

History

April 12, 2024
Added interface to simplify usage of generated code.

Topics

Related publications

  • Divasón, J., Joosten, S. J. C., Thiemann, R., & Yamada, A. (2019). A Verified Implementation of the Berlekamp–Zassenhaus Factorization Algorithm. Journal of Automated Reasoning, 64(4), 699–735. https://doi.org/10.1007/s10817-019-09526-y
  • von zur Gathen, J., & Gerhard, J. (2013). Modern Computer Algebra. https://doi.org/10.1017/cbo9781139856065
  • Wikipedia

Session Berlekamp_Zassenhaus