A Formalization of Berlekamp’s Factorization Algorithm

Jose Divasón, Sebastiaan Joosten, René Thiemann, and Akihisa Yamada

Isabelle Workshop 2016,  2016.


We formalize Berlekamp’s algorithm for factoring polynomials over prime fields in Isabelle/HOL. We first formalize the algorithm by defining a dedicated type for prime fields, and state the initial soundness theorem depending on this type. We then eliminate the type from the statement using the recently added functionality of local type definitions.
In order to efficiently execute Berlekamp’s algorithm, and to employ the algorithm in factorization of integer polynomials,we further generalize and optimize polynomial division algorithms.
The generated code is already used in the formalization for algebraic mnumbers, where it is an ingredient of a modern factorization algorithm for integer polynomials, although currently only as an oracle.




author = "Jose Divas\'on and Sebastiaan Joosten and Ren\'e Thiemann and Akihisa Yamada",
title = "A Formalization of Berlekamp’s Factorization Algorithm",
booktitle = "Isabelle Workshop 2016",
year = 2016
Nach oben scrollen