Tobias Rothmann (Jul 07 2023 at 19:56): Tobias Rothmann (Jul 07 2023 at 19:56):Hi,
I am trying to factorize polynomials over a finite field Fp (p is prime) into irreducible parts.
I am aware of the Berlekamp-Zassenhaus formalization, which covers integer polynomials, real polynomials, and square-free polynomials over finite fields, but I couldn't find a formalization for non-square-free polynomials over finite fields.
Additionally, there seems to be no general formalization for an algorithm that separates a polynomial over a finite field into square-free parts, the Yun algorithm works only on a Field with characteristic 0, which doesn't hold for Fp (where char(Fp)=p).
Although the mathematical literature commonly refers to the conversion into square-free parts as "easily done", I find the formalization of such algorithms (namely the "Square-free factorization" algorithm and the "Elimination of Repeated Factors" algorithm) quite time-intensive, and hence would greatly appreciate any help :)
Side note:
If you know how to compute all roots (in the sense of x for \<phi>(x) = 0) of a polynomial over a finite field, that would also solve the problem for me :)
Manuel Eberl (Jul 10 2023 at 10:38):Maybe try asking René Thiemann by email. He might know, but I don't think he reads Zulip much. I do think he's on holiday right now though, so you might not get an answer that quickly.
Tobias Rothmann (Jul 12 2023 at 08:52):Thanks for the hint, I'll contact him :)
Yong Kiam (Sep 28 2023 at 04:22):(I'm really late to the answer here) did you get an answer to this? if not I believe Berlekamp-Zassenhaus can already do what you want, for example, https://en.wikipedia.org/wiki/Cantor%E2%80%93Zassenhaus_algorithm (see first line in Background section)
Manuel Eberl (Sep 29 2023 at 11:28):I think so, too, but you need to do a square free factorisation first
Tobias Rothmann (Sep 29 2023 at 13:57):Yong Kiam said:
(I'm really late to the answer here) did you get an answer to this? if not I believe Berlekamp-Zassenhaus can already do what you want, for example, https://en.wikipedia.org/wiki/Cantor%E2%80%93Zassenhaus_algorithm (see first line in Background section)
Hi thanks for the answer! :)
As Manuel said, I'm looking for "non square-free" factorization and the first line you're referring to says "square-free polynomial", right?
The Cantor–Zassenhaus algorithm takes as input a square-free polynomial
Emin Karayel (Sep 29 2023 at 14:12):The trick to check whether a polynomial is square-free is to compute the gcd of it with its formal derivative.
Emin Karayel (Sep 29 2023 at 14:13):E.g. if f has a square factor g then g will divide both f and f'.
Emin Karayel (Sep 29 2023 at 14:14):I'm not sure whether you're using HOL-Algebra (I had defined formal polynomial derivates for them "https://www.isa-afp.org/theories/finite_fields/#Formal_Polynomial_Derivatives" )
Emin Karayel (Sep 29 2023 at 14:14):There is also a library for formal derivatives in HOL-Computational_Algebra (if you're using the type-based approach)
Emin Karayel (Sep 29 2023 at 14:15):It's called pderiv (defined in "https://isabelle.in.tum.de/library/HOL/HOL-Computational_Algebra/Polynomial.html")
Emin Karayel (Sep 29 2023 at 14:27):By repeatedly dividing by gcd(f,f') the polynomial can be split into a product of square-free polynomials.
Tobias Rothmann (Sep 29 2023 at 14:39):Hi thanks for the answer!
Basically yes I think, but I think there is one more step with taking the p-th root (I think due to something with the characteristic of the Field being non-zero?).
See the ERF (Elimination of Repeated Factors) algorithm here: https://carleton.ca/math/wp-content/uploads/Factoring-Polynomials-over-Finite-Fields_Melissa-Scott.pdf
Seems like this algorithm has to be formalized at some point haha...
Luckily I already got some help from @Katharina Kreuzer who's trying to formalize the ERF in some spare time (thanks a lot again BTW :) ).
Emin Karayel (Sep 29 2023 at 14:49):Tobias Rothmann said:
Hi thanks for the answer!
Basically yes I think, but I think there is one more step with taking the p-th root (I think due to something with the characteristic of the Field being non-zero?).
See the ERF (Elimination of Repeated Factors) algorithm here: https://carleton.ca/math/wp-content/uploads/Factoring-Polynomials-over-Finite-Fields_Melissa-Scott.pdf
Seems like this algorithm has to be formalized at some point haha...
Luckily I already got some help from Katharina Kreuzer who's trying to formalize the ERF in some spare time (thanks a lot again BTW :) ).
Sounds good. Let me know if it works - and nice project btw. :)
Tobias Rothmann (Sep 29 2023 at 14:54):Emin Karayel said:
Tobias Rothmann said:
Hi thanks for the answer!
Basically yes I think, but I think there is one more step with taking the p-th root (I think due to something with the characteristic of the Field being non-zero?).
See the ERF (Elimination of Repeated Factors) algorithm here: https://carleton.ca/math/wp-content/uploads/Factoring-Polynomials-over-Finite-Fields_Melissa-Scott.pdf
Seems like this algorithm has to be formalized at some point haha...
Luckily I already got some help from Katharina Kreuzer who's trying to formalize the ERF in some spare time (thanks a lot again BTW :) ).Sounds good. Let me know if it works - and nice project btw. :)
Sure! And thanks a lot :)
Yong Kiam (Oct 02 2023 at 01:04):Tobias Rothmann said:
Yong Kiam said:
(I'm really late to the answer here) did you get an answer to this? if not I believe Berlekamp-Zassenhaus can already do what you want, for example, https://en.wikipedia.org/wiki/Cantor%E2%80%93Zassenhaus_algorithm (see first line in Background section)
Hi thanks for the answer! :)
As Manuel said, I'm looking for "non square-free" factorization and the first line you're referring to says "square-free polynomial", right?The Cantor–Zassenhaus algorithm takes as input a square-free polynomial
ah sorry I hadn't checked the Zulip for a bit, I should have quoted this part of the Wikipedia sentence, which is what @Emin Karayel said
(algorithms exist for efficiently factoring arbitrary polynomials into a product of polynomials satisfying these conditions, for instance, f ( x ) / gcd ( f ( x ) , f ′ ( x ) ) {\displaystyle f(x)/\gcd(f(x),f'(x))} is a squarefree polynomial with the same factors as f ( x ) f(x),
It's a bit more difficult than that in finite characteristic, I fear, since taking the derivative might kill some or all of the coefficients in the polynomial. For example, in characteristic the derivative of is and therefore dividing out the GCD of the polynomial and its derivative would just give us .
Manuel Eberl (Oct 05 2023 at 13:31):The ERF algorithm linked above detects this problem and fixes it. At least if I understood things correctly – I only skimmed it briefly.
Manuel Eberl (Dec 05 2023 at 10:17):Just for the sake of completeness, this is now in the AFP:
https://www.isa-afp.org/entries/Perfect_Fields.html
https://www.isa-afp.org/entries/Elimination_Of_Repeated_Factors.html
Last updated: May 06 2024 at 16:21 UTC