A formalization of the Berlekamp-Zassenhaus factorization algorithm

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

  • 1 Citations

Abstract

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.
LanguageEnglish
Title of host publicationCPP 2017
Subtitle of host publicationProceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs
PublisherAssociation for Computing Machinery
Pages17-29
Number of pages13
ISBN (Print)978-1-4503-4705-1
DOIs
StatePublished - 2017
Event6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017 - Paris, France
Duration: 16 Jan 201717 Jan 2017
Conference number: 6

Conference

Conference6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017
CountryFrance
CityParis
Period16/01/1717/01/17

Fingerprint

Factorization
Polynomials
Experiments

Cite this

Divasón, J., Joosten, S., Thiemann, R., & Yamada, A. (2017). A formalization of the Berlekamp-Zassenhaus factorization algorithm. In CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (pp. 17-29). Association for Computing Machinery. DOI: 10.1145/3018610.3018617
Divasón, Jose ; Joosten, Sebastiaan ; Thiemann, René ; Yamada, Akihisa. / A formalization of the Berlekamp-Zassenhaus factorization algorithm. CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. Association for Computing Machinery, 2017. pp. 17-29
@inproceedings{89eb74ec87124e8791270c05bca38e89,
title = "A formalization of the Berlekamp-Zassenhaus factorization algorithm",
abstract = "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.",
author = "Jose Divas{\'o}n and Sebastiaan Joosten and Ren{\'e} Thiemann and Akihisa Yamada",
year = "2017",
doi = "10.1145/3018610.3018617",
language = "English",
isbn = "978-1-4503-4705-1",
pages = "17--29",
booktitle = "CPP 2017",
publisher = "Association for Computing Machinery",
address = "United States",

}

Divasón, J, Joosten, S, Thiemann, R & Yamada, A 2017, A formalization of the Berlekamp-Zassenhaus factorization algorithm. in CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. Association for Computing Machinery, pp. 17-29, 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, 16/01/17. DOI: 10.1145/3018610.3018617

A formalization of the Berlekamp-Zassenhaus factorization algorithm. / Divasón, Jose; Joosten, Sebastiaan; Thiemann, René; Yamada, Akihisa.

CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. Association for Computing Machinery, 2017. p. 17-29.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

TY - GEN

T1 - A formalization of the Berlekamp-Zassenhaus factorization algorithm

AU - Divasón,Jose

AU - Joosten,Sebastiaan

AU - Thiemann,René

AU - Yamada,Akihisa

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

U2 - 10.1145/3018610.3018617

DO - 10.1145/3018610.3018617

M3 - Conference contribution

SN - 978-1-4503-4705-1

SP - 17

EP - 29

BT - CPP 2017

PB - Association for Computing Machinery

ER -

Divasón J, Joosten S, Thiemann R, Yamada A. A formalization of the Berlekamp-Zassenhaus factorization algorithm. In CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. Association for Computing Machinery. 2017. p. 17-29. Available from, DOI: 10.1145/3018610.3018617