Correcting Bird's Proof of the Sieve of Eratosthenes: A Proof about Infinite Lists
2025-02-08
This paper corrects an erroneous proof by Richard Bird in his book *Thinking Functionally with Haskell* concerning the Sieve of Eratosthenes. Bird presents a circular, list-based implementation, but his proof hint is flawed. The authors provide a complete correctness proof by introducing new lemmas and appealing to a weakening of Bertrand's Postulate. The connection between this algorithm and David Turner's vision of "Total Functional Programming" is also explored.