Correction de la preuve de Bird du crible d'Ératosthène : une preuve sur les listes infinies
2025-02-08
Cet article corrige une preuve erronée de Richard Bird dans son livre *Thinking Functionally with Haskell* concernant le crible d'Ératosthène. Bird présente une implémentation circulaire basée sur des listes, mais son indice de preuve est erroné. Les auteurs fournissent une preuve de correction complète en introduisant de nouveaux lemmes et en faisant appel à un affaiblissement du postulat de Bertrand. La connexion entre cet algorithme et la vision de David Turner de la « programmation fonctionnelle totale » est également explorée.