Email Gateway (Aug 19 2022 at 12:08): Email Gateway (Aug 19 2022 at 12:08):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I wonder if, by any chance, any of you know anything about work having
been done in Isabelle concerning the efficient computation of the set of
divisors of a natural number or an integer. Specifically, I require an
executable and ideally quite efficient function "divisors (n::int) = {d.
d dvd n}", but obviously, the same for natural numbers would be quite
sufficient as well.
I surveyed the Isabelle library but failed to find anything of the sort.
I also thought about resorting to constructing the set of divisors from
a prime factorisation should I fail to find any formalisation of the set
of divisors. Has a fast, executable prime factorisation function been
implemented in Isabelle? So far, all I could find is the uniqueness of
the prime factorisation.
I should probably add that I am, of course, perfectly aware that there
is no known algorithm for integer factorisation in polynomial time,
which, if I am not mistaken, implies that there is also no known
algorithm for computing the divisors of an integer in polynomial time;
by "efficient", I therefore mean, as it were, "not unnecessarily
inefficient". I am not looking for anything overly fancy such as number
field sieves, just something slightly better than trial division with
all integers from 1 to n.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 12:08):From: Brian Huffman <huffman.brian.c@gmail.com>
Do you need an Isabelle definition that works for code generation, or
would it be sufficient to have something that works in Isabelle
proofs, e.g. a simproc that could rewrite "prime_factorization 60" to
"[2,2,3,5]"?
I don't know of any pre-existing solution for factorization, but if a
simproc is all you need, then you might consider doing something like
what we have for div/mod on integer numerals. (See simprocs
binary_int_div and binary_int_mod in src/HOL/Divides.thy.)
If you have a function defined in Isabelle as "f x == THE y. P x y",
then you can use an external oracle or ML function to compute "y" from
"x". Within Isabelle, you then prove "P x y" and use the uniqueness
theorem to derive "f x = y".
If the uniqueness of prime factorizations is already proved, then we
just need a way to prove in Isabelle that a given factorization is
indeed a prime factorization of a given number. I guess the next step
is to find an efficient way to test for primality in Isabelle. :)
Email Gateway (Aug 19 2022 at 12:09):From: Manuel Eberl <eberlm@in.tum.de>
At the end of the day, I want to write a proof method in Isabelle, so I
would imagine a simproc would do just fine. (albeit a definition would
probably be easier to use)
I had not thought of this kind of approach, so thank you for that
suggestion. As for the primality test, I do remember seeing an
implementation of Eratosthenes' sieve somewhere in HOL/Number_Theory.
Well, I shall look into it, thank you.
Email Gateway (Aug 19 2022 at 12:09):From: Ognjen Maric <ognjen.maric@gmail.com>
How large are your numbers? If the memory from my crypto courses serves
me well, trial division (you can go just up to the square root of n) is
still the most efficient option for reasonably small numbers, e.g. 32-bit.
Cheers,
Ognjen
Email Gateway (Aug 19 2022 at 12:09):From: René Thiemann <rene.thiemann@uibk.ac.at>
At least for square roots, there is an executable algorithm for
floor (sqrt integer) and ceiling (sqrt integer)
(See Sqrt_Babylonian in the development version of the AFP)
Cheers,
René
Email Gateway (Aug 19 2022 at 12:09):From: Manuel Eberl <eberlm@in.tum.de>
Yes, indeed, I think so, too. Although I do not know the latest
developments in number field sieve algorithms; they might have become
better at handling small integers in the mean time. However, I was not
looking for an efficient factorisation algorithm, but for a more
efficient algorithm for the divisors of n than trial division for
/every/ natural number ≤ n. And that is, indeed, possible.
The Haskell arithmoi package, for instance, first computes the prime
factorisation using a combination of some kind of trial division for
small factors and then a number field sieve and then uses that to
generate the divisors, and since the authors of the arithmoi package
generally seem to know their stuff, I would assume that this is indeed
the most efficient way to do it.
So I think that at some point, I will probably implement this in
Isabelle – minus the number field sieve, of course – and until then, I
will stick with the naïve approach.
Thanks for the replies
Cheers
Manuel
Email Gateway (Aug 19 2022 at 12:09):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Manuel,
the upcoming Isabelle release will contain a sieve algorithm in
HOL/Number_Theory/Eratosthenes.thy
I appreciate your efforts to bring more executability to number theory.
Cheers,
Florian
signature.asc
Email Gateway (Aug 19 2022 at 12:09):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
well, that is not what I meant by a "number field sieve". All the same,
it might be useful, but I am not entirely sure.
Do you happen to know whether Eratosthenes's sieve facilitates
factorisation at all? My approach would have been to simply enumerate
ascending integers d and "divide the factor d out of n" as often as
possible; non-prime numbers will then always be divided out zero times,
since their prime factors are divided out before they are reached
themselves.
If one first generates the appropriate number of prime numbers with
Eratosthenes' sieve, one can, of course, avoid unnecessary divisibility
tests, but at the cost of the time and memory overhead of computing the
sieve, so I am not sure whether that is a good tradeoff for practical
situations.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 12:09):From: Ognjen Maric <ognjen.maric@gmail.com>
On 10/19/2013 09:15 AM, Manuel Eberl wrote:
Yes, indeed, I think so, too. Although I do not know the latest
developments in number field sieve algorithms; they might have become
better at handling small integers in the mean time. However, I was not
looking for an efficient factorisation algorithm, but for a more
efficient algorithm for the divisors of n than trial division for
/every/ natural number ≤ n. And that is, indeed, possible.
I'm not sure I follow. Yes, there are asymptotically faster algorithms
than trial division, but that you knew already. I merely said that is
nothing more efficient than trial division (with odd numbers <= sqrt(n))
for factoring a single relatively small number. With "small number"
being I guess anything not used for crypto. I'm not a cryptographer
though, so I could be wrong, but I'm not even sure if you're disagreeing
with me or not.
The Haskell arithmoi package, for instance, first computes the prime
factorisation using a combination of some kind of trial division for
small factors and then a number field sieve and then uses that to
generate the divisors, and since the authors of the arithmoi package
generally seem to know their stuff, I would assume that this is indeed
the most efficient way to do it.
I looked at the code briefly, and yes, the authors seem to know crypto
much better than I do. However, judging by their comments they don't
implement any number field sieves, they use elliptic curve
factorization. Which, according to my crypto course lecture notes,
"performs well for numbers with a medium-sized smallest factor (20-60
digits)".
So I think that at some point, I will probably implement this in
Isabelle – minus the number field sieve, of course – and until then, I
will stick with the naïve approach.
Another option is continued fractions factorization, which are
relatively simple IIRC, and beat trial division asymptotically. But I
think it all really depends on what your application is.
Cheers,
Ognjen
Email Gateway (Aug 19 2022 at 12:09):From: Manuel Eberl <eberlm@in.tum.de>
On 19/10/13 10:38, Ognjen Maric wrote:
I'm not sure I follow. Yes, there are asymptotically faster algorithms
than trial division, but that you knew already. I merely said that is
nothing more efficient than trial division (with odd numbers <= sqrt(n))
for factoring a single relatively small number.
Well my point is that I am not looking for an algorithm to factorise an
integer, but to compute all its divisors. Divisors, not factors! The
prime factors of 10 are 2 and 5, its (positive) divisors are 1, 2, 5,
and 10. Of course, the divisor problem can be reduced to the
factorisation problem, which is why factorisation would also help me.
I looked at the code briefly, and yes, the authors seem to know crypto
much better than I do. However, judging by their comments they don't
implement any number field sieves, they use elliptic curve
factorization. Which, according to my crypto course lecture notes,
"performs well for numbers with a medium-sized smallest factor (20-60
digits)".
Ah yes, indeed they do. But, anyway, my focus of attention, as I already
said, is not on the factorisation, but on the "divisors" function:
http://hackage.haskell.org/package/arithmoi-0.4.0.3/docs/Math-NumberTheory-Primes-Factorisation.html#v:divisors
That is what I want, and as you can see, they compute a prime
factorisation and then compute the set of divisors from that. Which is
what I am planning to do in Isabelle now at some point.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 12:11):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
I am definitely not sure either. You'll find out such things during the
progress of your work…
Florian
signature.asc
Last updated: Apr 24 2024 at 01:07 UTC