The Factorization Algorithm of Berlekamp and Zassenhaus. 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.
Keywords for this software
References in zbMATH (referenced in 9 articles )
Showing results 1 to 9 of 9.
- Divasón, Jose; Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa: A verified implementation of the Berlekamp-Zassenhaus factorization algorithm (2020)
- Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa: A verified implementation of algebraic numbers in Isabelle/HOL (2020)
- Thiemann, René; Bottesch, Ralph; Divasón, Jose; Haslbeck, Max W.; Joosten, Sebastiaan J. C.; Yamada, Akihisa: Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL (2020)
- Chan, Hing-Lun; Norrish, Michael: Classification of finite fields with applications (2019)
- Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definition in higher-order logic (2019)
- Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
- Divasón, Jose; Joosten, Sebastiaan; Thiemann, René; Yamada, Akihisa: A formalization of the LLL basis reduction algorithm (2018)
- Zhan, Bohua; Haslbeck, Maximilian P. L.: Verifying asymptotic time complexity of imperative programs in Isabelle (2018)
- Kunčar, Ondřej; Popescu, Andrei: Comprehending Isabelle/HOL’s consistency (2017)