Re: [isabelle] Computing divisors


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

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


On 19/10/13 09:29, Florian Haftmann wrote:
> Hi Manuel,
>> 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.
> 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

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.