Conversation
| (eratosthenes_sieve.go n sieve 2).toList.mergeSort | ||
| where | ||
| go (n : Nat) (sieve : Std.HashSet Nat) (curr : Nat) := | ||
| if curr < n |
There was a problem hiding this comment.
This should only go up to sqrt n if possible.
There was a problem hiding this comment.
This is not available without batteries. I could copy this over though.
There was a problem hiding this comment.
You can just check for curr * curr < n.
| if curr < n | ||
| then | ||
| if curr ∈ sieve | ||
| then eratosthenes_sieve.go n (sieve.filter (fun x => (x = curr ∨ x % curr != 0))) (curr + 1) |
There was a problem hiding this comment.
I'm not sure that this has the right asymptotic complexity. The filtering step takes time proportional to the number of remaining elements in sieve. In the usual sieve of Eratosthenes, you iterate from curr^2 to n with step size curr, so the time taken is proportional to something like (n - curr^2)/curr, which I think is faster.
There was a problem hiding this comment.
In fact, I think that this is the same fundamental difference that is described in section 2 of https://www.cs.hmc.edu/~oneill/papers/Sieve-JFP.pdf.
2 participants
This PR implements the solution for task 96 using a sieve construction. I currently struggle a bit with the best definition for the primes that make the proofs simple.