Korrektur von Birds Beweis des Sieb des Eratosthenes: Ein Beweis über unendliche Listen
2025-02-08
Dieser Artikel korrigiert einen fehlerhaften Beweis von Richard Bird in seinem Buch *Thinking Functionally with Haskell* zum Sieb des Eratosthenes. Bird präsentiert eine kreisförmige, listenbasierte Implementierung, aber sein Beweisansatz ist fehlerhaft. Die Autoren liefern einen vollständigen Korrektheitsbeweis, indem sie neue Lemmas einführen und sich auf eine Abschwächung des Bertrandschen Postulats berufen. Der Zusammenhang zwischen diesem Algorithmus und David Turners Vision der „Total Functional Programming“ wird ebenfalls untersucht.