A formalization of the Berlekamp-Zassenhaus factorization algorithm
Authors:
- Divasón, Jose
- Joosten, Sebastiaan J. C.
- Thiemann, René
- Yamada, Akihisa
Published in: CPP 2017 pp 17–29
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},
bdsk-url-1 = {https://doi.org/10.1145/3018610.3018617},
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}
}