×

A verified implementation of the Berlekamp-Zassenhaus factorization algorithm. (English) Zbl 1469.68165

Summary: We formally verify 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 factorization in the prime field \(\mathrm{GF}(p)\) and then performs computations in the ring of integers 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 locales and local type definitions. Through experiments we verify that our algorithm factors polynomials of degree up to 500 within seconds.

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
03B35 Mechanization of proofs and logical operations
12-08 Computational methods for problems pertaining to field theory
13P05 Polynomials, factorization in commutative rings
68V20 Formalization of mathematics in connection with theorem provers
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abbott, J., Bounds on factors in \(Z[x]\), J. Symb. Comput., 50, 532-563 (2013) · Zbl 1295.12010 · doi:10.1016/j.jsc.2012.09.004
[2] Axler, SJ, Linear Algebra Done Right. Undergraduate Texts in Mathematics (1997), Berlin: Springer, Berlin · Zbl 0886.15001
[3] Ballarin, C., Locales: a module system for mathematical theories, J. Autom. Reason., 52, 2, 123-153 (2014) · Zbl 1315.68218 · doi:10.1007/s10817-013-9284-7
[4] Barthe, G., Grégoire, B., Heraud, S., Olmedo, F., Béguelin, S.Z.: Verified indifferentiable hashing into elliptic curves. In: Degano, P., Guttman, J.D. (eds.) Principles of Security and Trust. POST 2012, Volume 7215 of LNCS, pp. 209-228. Springer, Berlin (2012) · Zbl 1354.94021
[5] Berlekamp, ER, Factoring polynomials over finite fields, Bell Syst. Tech. J., 46, 8, 1853-1859 (1967) · Zbl 0166.04901 · doi:10.1002/j.1538-7305.1967.tb03174.x
[6] Blanchette, J.C., Meier, F., Popescu, A., Traytel, D.: Foundational nonuniform (co)datatypes for higher-order logic. In: ACM/IEEE Symposium on Logic in Computer Science, LICS 32, pp. 1-12. IEEE Computer Society (2017). Cross-type induction is explained in Appendix D of the extended report version at http://matryoshka.gforge.inria.fr/pubs/nonuniform_report.pdf · Zbl 1495.68238
[7] Bottesch, R., Haslbeck, M.W., Thiemann, R.: A verified efficient implementation of the LLL basis reduction algorithm. In: Barthe, G., Sutcliffe, G., Veanes, M. (eds.) Logic for Programming, Artificial Intelligence and Reasoning. LPAR 22, Volume 57 of EPiC Series in Computing, pp. 164-180. EasyChair (2018) · Zbl 1409.68252
[8] Cantor, DG; Zassenhaus, H., A new algorithm for factoring polynomials over finite fields, Math. Comput., 36, 154, 587-592 (1981) · Zbl 0493.12024 · doi:10.1090/S0025-5718-1981-0606517-5
[9] Cerlienco, L.; Mignotte, M.; Piras, F., Computing the measure of a polynomial, J. Symb. Comput., 4, 1, 21-33 (1987) · Zbl 0629.12002 · doi:10.1016/S0747-7171(87)80050-0
[10] Divasón, J., Joosten, S.J.C., Thiemann, R., Yamada, A.: A formalization of the Berlekamp-Zassenhaus factorization algorithm. In: Bertot, Y., Vafeiadis, V. (eds.) Certified Programs and Proofs. CPP 2017, pp. 17-29. ACM (2017) · Zbl 1469.68165
[11] Divasón, J., Joosten, S.J.C., Thiemann, R., Yamada, A.: A formalization of the LLL basis reduction algorithm. In: Avigad, J., Mahboubi, A. (eds.) Interactive Theorem Proving. ITP 2018, Volume 10895 of LNCS, pp. 160-177. Springer, Berlin (2018) · Zbl 1468.68287
[12] Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) Functional and Logic Programming. FLOPS 2010, Volume 6009 of LNCS, pp. 103-117. Springer, Berlin (2010) · Zbl 1284.68131
[13] Harrison, J., The HOL light theory of Euclidean space, J. Autom. Reason., 50, 2, 173-190 (2013) · Zbl 1260.68373 · doi:10.1007/s10817-012-9250-9
[14] van Hoeij, M., Factoring polynomials and the knapsack problem, J. Number Theory, 95, 2, 167-189 (2002) · Zbl 1081.11080 · doi:10.1016/S0022-314X(01)92763-5
[15] Huffman, B., Kunčar, O.: Lifting and transfer: a modular design for quotients in Isabelle/HOL. In: Certified Programs and Proofs. CPP 2013, Volume 8307 of LNCS, pp. 131-146. Springer, Berlin (2013) · Zbl 1426.68284
[16] Karatsuba, A.; Ofman, Y., Multiplication of multidigit numbers on automata, Sov. Phys. Dokl., 7, 7, 595-596 (1963)
[17] Kirkels, B.: Irreducibility certificates for polynomials with integer coefficients. Master’s thesis, Radboud Universiteit Nijmegen (2004)
[18] Knuth, DE, The Art of Computer Programming, Volume 2: Seminumerical Algorithms (1998), Reading: Addison-Wesley, Reading · Zbl 0895.65001
[19] Kobayashi, H., Suzuki, H., Ono, Y.: Formalization of Hensel’s lemma. In: Hurd, J., Smith, E., Darbari, A. (eds.) Theorem Proving in Higher Order Logics: Emerging Trends Proceedings, pp. 114-118. Oxford University Computing Laboratory (2005)
[20] Krauss, A.: Recursive definitions of monadic functions. In: Bove, A., Komendantskaya, E., Niqui, M. (eds.) Partiality and Recursion in Interactive Theorem Provers. PAR 2010, Volume 43 of EPTCS, pp. 1-13 (2010)
[21] Kunčar, O.; Popescu, A., From types to sets by local type definition in higher-order logic, J. Autom. Reason., 62, 2, 237-260 (2019) · Zbl 1468.68295 · doi:10.1007/s10817-018-9464-6
[22] Lee, H.: Vector spaces. Archive of Formal Proofs, Formal proof development. http://isa-afp.org/entries/VectorSpace.html (2014)
[23] Lenstra, AK; Lenstra, HW; Lovász, L., Factoring polynomials with rational coefficients, Math. Ann., 261, 515-534 (1982) · Zbl 0488.12001 · doi:10.1007/BF01457454
[24] Lochbihler, A.: Fast machine words in Isabelle/HOL. In: Avigad, J., Mahboubi, A. (eds.) Interactive Theorem Proving. ITP 2018, Volume 10895 of LNCS, pp. 388-410. Springer, Berlin (2018) · Zbl 1511.68324
[25] Maple 2017.3. Maplesoft, a division of Waterloo Maple Inc. Waterloo (2017)
[26] Martin-Dorel, É.; Hanrot, G.; Mayero, M.; Théry, L., Formally verified certificate checkers for hardest-to-round computation, J. Autom. Reason., 54, 1, 1-29 (2015) · Zbl 1315.68222 · doi:10.1007/s10817-014-9312-2
[27] Mignotte, M., An inequality about factors of polynomials, Math. Comput., 28, 128, 1153-1157 (1974) · Zbl 0299.12101 · doi:10.1090/S0025-5718-1974-0354624-3
[28] Miola, A.; Yun, DY, Computational aspects of Hensel-type univariate polynomial greatest common divisor algorithms, ACM SIGSAM Bull., 8, 3, 46-54 (1974) · doi:10.1145/1086837.1086844
[29] Nipkow, T.; Paulson, L.; Wenzel, M., Isabelle/HOL—A Proof Assistant for Higher-Order Logic, Volume 2283 of LNCS (2002), Berlin: Springer, Berlin · Zbl 0994.68131
[30] Thiemann, R.: Computing n-th roots using the Babylonian method. Archive of Formal Proofs, Formal proof development. http://isa-afp.org/entries/Sqrt_Babylonian.html (2013)
[31] Thiemann, R., Yamada, A.: Algebraic numbers in Isabelle/HOL. In: Blanchette, J., Merz, S. (eds.) Interactive Theorem Proving. ITP 2016, Volume 9807 of LNCS, pp. 391-408. Springer, Berlin (2016) · Zbl 1478.68443
[32] Thiemann, R., Yamada, A.: Formalizing Jordan normal forms in Isabelle/HOL. In: Avigad, J., Chlipala, A. (eds.) Certified Programs and Proofs. CPP 2016, pp. 88-99. ACM (2016)
[33] von zur Gathen, J.; Gerhard, J., Modern Computer Algebra (2013), Cambridge: Cambridge University Press, Cambridge · Zbl 1277.68002
[34] Mathematica Version 11.2. Wolfram Research, Inc. Champaign (2017)
[35] Yun, D.Y.: On square-free decomposition algorithms. In: Symbolic and Algebraic Computation. SYMSAC 1976, pp. 26-35. ACM (1976) · Zbl 0498.13006
[36] Zassenhaus, H., On Hensel factorization, I, J. Number Theory, 1, 3, 291-311 (1969) · Zbl 0188.33703 · doi:10.1016/0022-314X(69)90047-X
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.