Skip to Content

A formalization of the Berlekamp-Zassenhaus factorization algorithm

Posted on

Authors:

  • Divasón, Jose
  • Joosten, Sebastiaan J. C.
  • Thiemann, René
  • Yamada, Akihisa

Formalisation is online

Published in: CPP 2017 pp 17–29

DOI: 10.1145/3018610.3018617

Paper

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 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.

BibTeX entry:

@inproceedings{Divason17,
 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 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.},
 address = {United States},
 author = {Jose Divas{\'o}n and Sebastiaan Jozef Christiaan Joosten and Ren{\'e} Thiemann and Akihisa Yamada},
 booktitle = {CPP 2017},
 day = {16},
 doi = {10.1145/3018610.3018617},
 isbn = {978-1-4503-4705-1},
 language = {English},
 month = {Jan},
 pages = {17--29},
 publisher = {Association for Computing Machinery},
 title = {A formalization of the Berlekamp-Zassenhaus factorization algorithm},
 year = {2017}
}