A formalization of the Berlekamp-Zassenhaus factorization algorithm
- Divasón, J. 1
- Joosten, S. 2
- Thiemann, R. 2
- Yamada, A. 2
-
1
Universidad de La Rioja
info
-
2
University of Innsbruck
info
ISBN: 9781450347051
Año de publicación: 2017
Páginas: 17-29
Tipo: Capítulo de Libro
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 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. © 2017 ACM.