General
This site provides supporting material for the paper Formalization of the Berlekamp-Zassenhaus Factorization Algorithm by José Divasón, Sebastiaan Joosten, René Thiemann and Akihisa Yamada.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 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.
Formalization
The formalization is part of the Archive of Formal Proofs, revision c57b0e9b0d65, which compiles with Isabelle revision 03057a8fdd1f.
Experimental results
One can rerun the experimental results as follows:
- Generate the directory ~/Code and either open Tests.thy in Isabelle to generate the required Haskell sources or copy them from the Code directory in the archive. If you have trouble with this step, or do not wish to install Isabelle, you can download the directory Code as a zip.
- Inspect the path of the constant binary within the file Code/Mathematica.hs whether it matches your Mathematica installation. Otherwise you can deactivate the Mathematica experiments by disabling the external factorization in experimental_data/run_experiment.sh.
- Compile the Haskell code with GHC: ghc --make Main -O2
- Download and unzip the experiments and go to this directory, from which you run the script run_experiments.sh. This will generate results and runtimes for each polynomial.
- Run run_comparisonTime.sh to get the runtimes in a nicer format.
All results can also be inspected in the following table. You can click in each column, to view the input polynomial and the computed factorizations, resp. The timing informations have been obtained on a computer running macOS Sierra 10.12 on a 6-core Intel Xeon E5 processor at 3.5 Ghz.