https://www.cambridge.org/core/journals/journal-of-functional-programming/article/turner-bird-eratosthenes-an-eternal-burning-thread/32E2EDF5D5EAEC95F13D313BC97B86F0 Skip to main content Accessibility help We use cookies to distinguish you from other users and to provide you with a better experience on our websites. Close this message to accept cookies or find out how to manage your cookie settings. Close cookie message Login Alert Cancel Log in x x Discover Content Products and Services Register Log In (0) Cart [ ] Search --------------------------------------------------------------------- * Browse * Services * Open research Institution Login [ ] Search Menu links 1. Browse 1. Subjects 1. Subjects (A-D) 1. Anthropology 2. Archaeology 3. Area Studies 4. Art 5. Chemistry 6. Classical Studies 7. Computer Science 8. Drama, Theatre, Performance Studies 2. Subjects (E-K) 1. Earth and Environmental Science 2. Economics 3. Education 4. Engineering 5. English Language Teaching - Resources for Teachers 6. Film, Media, Mass Communication 7. General Science 8. Geography 9. History 3. Subjects (L-O) 1. Language and Linguistics 2. Law 3. Life Sciences 4. Literature 5. Management 6. Materials Science 7. Mathematics 8. Medicine 9. Music 10. Nutrition 4. Subjects (P-Z) 1. Philosophy 2. Physics and Astronomy 3. Politics and International Relations 4. Psychiatry 5. Psychology 6. Religion 7. Social Science Research Methods 8. Sociology 9. Statistics and Probability 2. Open access 1. All open access publishing 1. Open access 2. Open access journals 3. Research open journals 4. Journals containing open access 5. Open access articles 6. Open access books 7. Open access Elements 3. Journals 1. Explore 1. All journal subjects 2. Search journals 2. Open access 1. Open access journals 2. Research open journals 3. Journals containing open access 4. Open access articles 3. Collections 1. Cambridge Forum 2. Cambridge Law Reports Collection 3. Cambridge Prisms 4. Research Directions 4. Books 1. Explore 1. Books 2. Open access books 3. New books 4. Flip it Open 2. Collections 1. Cambridge Companions 2. Cambridge Editions 3. Cambridge Histories 4. Cambridge Library Collection 5. Cambridge Shakespeare 6. Cambridge Handbooks 3. Collections (cont.) 1. Dispute Settlement Reports Online 2. Flip it Open 3. Hemingway Letters 4. Shakespeare Survey 5. Stahl Online 6. The Correspondence of Isaac Newton 5. Elements 1. Explore 1. About Elements 2. Elements series 3. Open access Elements 4. New Elements 2. Subjects (A-E) 1. Anthropology 2. Archaeology 3. Classical Studies 4. Computer Science 5. Drama, Theatre, Performance Studies 6. Earth and Environmental Sciences 7. Economics 8. Education 9. Engineering 3. Subjects (F-O) 1. Film, Media, Mass Communication 2. History 3. Language and Linguistics 4. Law 5. Life Sciences 6. Literature 7. Management 8. Mathematics 9. Medicine 10. Music 4. Subjects (P-Z) 1. Philosophy 2. Physics and Astronomy 3. Politics and International Relations 4. Psychology 5. Religion 6. Sociology 7. Statistics and Probability 6. Textbooks 1. Explore 1. Cambridge Higher Education 2. Title list 3. New titles 7. Collections 1. Book collections 1. Cambridge Companions 2. Cambridge Editions 3. Cambridge Histories 4. Cambridge Library Collection 5. Cambridge Shakespeare 6. Cambridge Handbooks 2. Book collections (cont.) 1. Dispute Settlement Reports Online 2. Flip it Open 3. Hemingway Letters 4. Shakespeare Survey 5. Stahl Online 6. The Correspondence of Isaac Newton 3. Journal collections 1. Cambridge Forum 2. Cambridge Law Reports Collection 3. Cambridge Prisms 4. Research Directions 4. Series 1. All series 8. Partners 1. Partners 1. Agenda Publishing 2. Amsterdam University Press 3. Anthem Press 4. Boydell & Brewer 5. Bristol University Press 6. Edinburgh University Press 7. Emirates Center for Strategic Studies and Research 8. Facet Publishing 2. Partners (cont.) 1. Foundation Books 2. Intersentia 3. ISEAS-Yusof Ishak Institute 4. Jagiellonian University Press 5. Royal Economic Society 6. Unisa Press 7. The University of Adelaide Press 8. Wits University Press 2. Services 1. About 1. About Cambridge Core 1. About 2. Accessibility 3. CrossMark policy 4. Ethical Standards 2. Environment and sustainability 1. Environment and sustainability 2. Reducing print 3. Journals moving to online only 3. Guides 1. User guides 2. User Guides and Videos 3. Support Videos 4. Training 4. Help 1. Cambridge Core help 2. Contact us 3. Technical support 2. Agents 1. Services for agents 1. Services for agents 2. Journals for agents 3. Books for agents 4. Price list 3. Authors 1. Journals 1. Journals 2. Journal publishing statistics 3. Corresponding author 4. Seeking permission to use copyrighted material 5. Publishing supplementary material 6. Writing an effective abstract 7. Journal production - FAQs 2. Journals (cont.) 1. Author affiliations 2. Co-reviewing policy 3. Digital Author Publishing Agreement - FAQs 4. Anonymising your manuscript 5. Publishing open access 6. Converting your article to open access 7. Publishing Open Access - webinars 3. Journals (cont.) 1. Preparing and submitting your paper 2. Publishing an accepted paper 3. Promoting your published paper 4. Measuring impact 5. Journals artwork guide 6. Using ORCID 4. Books 1. Books 2. Marketing your book 3. Author guides for Cambridge Elements 4. Corporates 1. Corporates 1. Commercial reprints 2. Advertising 3. Sponsorship 4. Book special sales 5. Contact us 5. Editors 1. Information 1. Journal development 2. Peer review for editors 3. Open access for editors 4. Policies and guidelines 2. Resources 1. The editor's role 2. Open research for editors 3. Engagement and promotion 4. Blogging 5. Social media 6. Librarians 1. Information 1. Open Access for Librarians 2. Transformative agreements 3. Transformative Agreements - FAQs 4. Evidence based acquisition 5. ebook news & updates 6. Cambridge libraries of the world podcast 7. Purchasing models 8. Journals Publishing Updates 2. Products 1. Cambridge frontlist 2. Cambridge journals digital archive 3. Hot topics 4. Other digital products 5. Perpetual access products 6. Price list 7. Developing country programme 8. New content 3. Tools 1. Eligibility checker 2. Transformative agreements 3. KBART 4. MARC records 5. Using MARCEdit for MARC records 6. Inbound OpenURL specifications 7. COUNTER report types 4. Resources 1. Catalogues and resources 2. Making the most of your EBA 3. Posters 4. Leaflets and brochures 5. Additional resources 6. Find my sales contact 7. Webinars 8. Read and publish resources 7. Peer review 1. Peer review 1. How to peer review journal articles 2. How to peer review book proposals 3. How to peer review Registered Reports 4. Peer review FAQs 5. Ethics in peer review 6. Online peer review systems 7. A guide to Publons 8. Publishing ethics 1. Journals 1. Publishing ethics guidelines for journals 2. Core editorial policies for journals 3. Authorship and contributorship for journals 4. Affiliations for journals 5. Research ethics for journals 6. Competing interests and funding for journals 2. Journals (cont.) 1. Data and supporting evidence for journals 2. Misconduct for journals 3. Corrections, retractions and removals for journals 4. Versions and adaptations for journals 5. Libel, defamation and freedom of expression 6. Business ethics journals 3. Books 1. Publishing ethics guidelines for books 2. Core editorial policies for books 3. Authorship and contributorship for books 4. Affiliations for books 5. Research ethics for books 6. Competing interests and funding for books 4. Books (cont.) 1. Data and supporting evidence for books 2. Misconduct for books 3. Corrections, retractions and removals for books 4. Versions and adaptations for books 5. Libel, defamation and freedom of expression 6. Business ethics books 9. Publishing partners 1. Publishing partners 1. Publishing partnerships 2. Partner books 3. eBook publishing partnerships 4. Journal publishing partnerships 2. Publishing partners (cont.) 1. Journals publishing 2. Customer support 3. Membership Services 4. Our Team 3. Open research 1. Open access policies 1. Open access policies 1. Open research 2. Open access policies 3. Cambridge University Press and Plan S 4. Text and data mining 5. Preprint policy 6. Social sharing 2. Journals 1. Open access journals 2. Gold Open Access journals 3. Transformative journals 4. Green Open Access policy for journals 5. Transparent pricing policy for journals 3. Books and Elements 1. Open access books 2. Gold open access books 3. Green Open Access policy for books 4. Open access Elements 2. Open access publishing 1. About open access 1. Open research 2. Open Access Week 3. What is open access? 4. Open access glossary 5. Open access myths 6. Hybrid Open Access FAQs 7. Eligibility checker 2. Open access resources 1. Open access resources 2. Benefits of open access 3. Creative commons licences 4. Funder policies and mandates 5. Article type definitions 6. Convert your article to Open Access 7. Open access video resources 3. Open research initiatives 1. Research transparency 1. Transparency and openness 2. Open Practice Badges 3. OA organisations, initiatives & directories 4. Registered Reports 5. Annotation for Transparent Inquiry (ATI) 2. Journal flips 1. Open access journal flips 2. OA Journal Flip FAQs 3. Flip it Open 1. Flip it Open 2. Flip it Open FAQs 4. Open access funding 1. Open access funding 1. Funding open access publication 2. Cambridge Open Equity Initiative 3. Completing a RightsLink (open access) transaction 5. Cambridge Open Engage 1. Cambridge Open Engage 1. Cambridge Open Engage 2. Partner With Us 3. Branded Hubs 4. Event Workspaces 5. Partner Resources 6. APSA Preprints 7. APSA Preprints FAQs Hostname: page-component-745bb68f8f-f46jp Total loading time: 0 Render date: 2025-02-07T11:10:17.622Z Has data issue: false hasContentIssue false * Home * >Journals * >Journal of Functional Programming * >Volume 35 * >Turner, Bird, Eratosthenes: An eternal burning thread * English * Francais [journal-of] Journal of Functional Programming --------------------------------------------------------------------- Article contents * Abstract * Introduction * The Genuine Sieve, using lists * The Approx Lemma * Proving the Sieve of Eratosthenes correct * 5 Conclusion * Conflicts of interest * Supplementary material * Footnotes * References Turner, Bird, Eratosthenes: An eternal burning thread Part of: JFP Functional Pearls Published online by Cambridge University Press: 05 February 2025 JEREMY GIBBONS Open the ORCID record for JEREMY GIBBONS [Opens in a new window] [svg]Show author details --------------------------------------------------------------------- JEREMY GIBBONS* Affiliation: Department of Computer Science, University of Oxford, Oxford, UK (e-mail: jeremy.gibbons@cs.ox.ac.uk) ----------------------------------------------------------------- * Article * Supplementary materials * Discussions * Metrics Article contents * Abstract * Introduction * The Genuine Sieve, using lists * The Approx Lemma * Proving the Sieve of Eratosthenes correct * 5 Conclusion * Conflicts of interest * Supplementary material * Footnotes * References [save-pdf-i] Save PDF [pdf-downlo]Save PDF (0.13 mb) [pdf-downlo]View PDF [Opens in a new window] [dropbox-ic] Save to Dropbox [google-dri] Save to Google Drive [svg] Save to Kindle [close-icon] [share-icon] Share [close-icon] [cite-icon] Cite [rights-ico]Rights & Permissions [Opens in a new window] --------------------------------------------------------------------- Abstract Functional programmers have many things for which to thank the late David Turner: design decisions he made in his languages SASL, KRC, and Miranda over the last 50 years are still influential and inspirational now. In particular, Turner was a strong advocate of lazy evaluation and of list comprehensions. As an illustration of these techniques, he popularized a one-line recursive "sieve" to generate the infinite list of prime numbers. Turner called this algorithm The Sieve of Eratosthenes. In a lovely paper called "The Genuine Sieve of Eratosthenes", Melissa O'Neill argued that Turner's program is not in fact a faithful implementation of the algorithm, and gave a detailed presentation using priority queues of the real thing. She included a variation by Richard Bird, which uses only lists but makes clever use of circular programming. Bird describes his circular program again in his textbook "Thinking Functionally with Haskell", and sets its proof of correctness as an exercise. In particular, why is this circular program productive? Unfortunately, Bird's hint for a solution is incorrect. So what should a proof look like? One of the last projects Turner worked on was the notion of "Total Functional Programming". He observed that most programs are already structurally recursive or corecursive, therefore guaranteed respectively terminating or productive; he conjectured that "with more practice we will find this is always true". We explore Bird's circular Sieve of Eratosthenes as a challenge problem for Turner's Total Functional Programming. --------------------------------------------------------------------- Video Abstract --------------------------------------------------------------------- Type Functional Pearl Information Journal of Functional Programming , Volume 35 , 2025 , e5 DOI: https://doi.org/10.1017/S0956796824000194 [Opens in a new window] Check for updates Creative Commons Creative Common License - CCCreative Common License - BYCreative Common License - NCCreative Common License - SA This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:// creativecommons.org/licenses/by-nc-sa/4.0/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited. Copyright (c) The Author(s), 2025. Published by Cambridge University Press 1 Introduction The late David Turner had great taste in language design and programming. In particular, he was a strong advocate for lazy evaluation and list comprehensions. One example program that he introduced in order to illustrate these techniques (Turner, Reference Turner1976, Reference Turner, Darlington, Henderson and Turner1982) is a one-line recursive "sieve" to generate the infinite list of prime numbers: [gif] That is, sieve takes a stream of candidate primes, initially the "plural" naturals (those greater than one); the head p of this stream is a prime, and the subsequent primes are obtained by removing all multiples of p from the candidates and sieving what remains. It's also a nice unfold (Gibbons & Jones, Reference Gibbons and Jones1998; Meertens, Reference Meertens2004). Turner called this algorithm "The Sieve of Eratosthenes". Unfortunately, as O'Neill (Reference O'Neill2009) observes, this nifty program is not in fact faithful to Eratosthenes. The problem is that for each prime p, every remaining candidate is tested for divisibility by p. O'Neill calls this algorithm "trial division", and argues that the Genuine Sieve of Eratosthenes should eliminate every multiple of p without reconsidering all the candidates in between. That is, at most every other natural number should be tested when eliminating multiples of 2, at most one in every three for multiples of 3, and so on. As an additional optimization, it suffices to eliminate multiples of p starting with p ^2, since by that point all composite numbers with a smaller nontrivial factor will already have been eliminated. O'Neill's paper presents a purely functional implementation of the Genuine Sieve of Eratosthenes. The tricky bit is keeping track of all the eliminations when generating an unbounded stream of primes, since obviously one can't eliminate all the multiples of one prime before moving on to the next prime. Her solution is to maintain a priority queue of iterators. Indeed, the main argument of her paper is that functional programmers are often too quick to use lists, when other data structures such as priority queues might be more appropriate. O'Neill's functional pearl was published in the Journal of Functional Programming, when Richard Bird was the handling editor for Functional Pearls. The paper includes an epilogue that presents a purely list-based but circular implementation of the Genuine Sieve, contributed by Bird during the editing process. Bird describes his circular program again in his textbook "Thinking Functionally with Haskell" (Bird, Reference Bird2014),Footnote ^* and sets as an exercise its proof of correctness, specifically productivity. Unfortunately, Bird's hint for a solution is incorrect. One of the last projects Turner worked on was the notion of "Total Functional Programming" (Turner, Reference Turner2004), "designed to exclude the possibility of non-termination". He observed that most programs are already structurally recursive or corecursive, therefore guaranteed respectively terminating or productive; he conjectured that "with more practice we will find this is always true". But it seems that it is not always so easy. In particular, Bird's circular Sieve of Eratosthenes is apparently productive; but it is not clear how it might fit within Turner's vision for Total Functional Programming. In this paper, we take on this challenge. What should Bird's proof hint have said? 2 The Genuine Sieve, using lists Bird's program appears in Section 9.2 of his book (Bird, Reference Bird2014), henceforth "TFWH". It deals with lists, but in this paper these will be infinite, sorted, duplicate-free streams, representing infinite sets--in this case, sets of natural numbers. In particular, the program involves no empty or partial lists, only properly infinite ones (but our proofs later will have to deal with partial lists as well). The prime numbers are what you get by eliminating the composite numbers from the plural naturals, and the composite numbers are the proper multiples of the primes. So the program is cleverly circular: [gif] where [gif] For later convenience, we have slightly refactored the program as presented by Bird, naming the components makeP and makeC. In particular, primes is a fixpoint of [gif] ${makeP}{\;.\;}{makeC}$ . Here, # ${(\mathbin{\backslash\mskip-2mu\backslash})}$ is the obvious implementation of list difference of strictly increasing streams, hence representing set difference: [gif] and [gif] ${\textit{multiples}\;\textit{p}}$ generates the multiples of p starting with # ${\textit{p}^{2}}$ : [gif] Thus, the composites are obtained by merging together the infinite stream of infinite streams [gif] ${[ [ \mathrm{4},\mathrm{6}\ mathinner{\ldotp\ldotp}],[ \mathrm{9},\mathrm{12}\mathinner{\ldotp\ ldotp}],[ \mathrm{25},\mathrm{30}\mathinner{\ldotp\ldotp}],\mathinner {\ldots}]}$ . You might think that you could have defined instead [gif] ${\textit{makeP}\;\textit{cs}\;=\;[ \mathrm{2}\mathinner{\ldotp \ldotp}]\mathbin{\backslash\mskip-2mu\backslash}\textit{cs}}$ , but this doesn't work: this won't compute the first prime without first computing some composites, and you can't compute any composites without at least the first prime. So using this in the definition of primes would be unproductive. Somewhat surprisingly, it suffices to "prime the pump" just with 2; everything else flows freely from there. Now for mergeAll, which represents the union of a set of sets. Here is the obvious implementation of merge, which merges two strictly increasing streams into one, hence representing set union: [gif] Then mergeAll is basically a stream fold with merge. You might think you could define this simply by [gif] ${\textit{mergeAll}\;(\textit {xs}\mathbin{:}\textit{xss})\;=\;\textit{merge}\;\textit{xs}\;(\ textit{mergeAll}\;\textit{xss})}$ , but again this would be unproductive. After all, you can't merge the infinite stream of sorted streams [gif] ${[ [ \mathrm{5},\mathrm{6}\mathinner{\ldotp\ ldotp}],[ \mathrm{4},\mathrm{5}\mathinner{\ldotp\ldotp}],[ \mathrm {3},\mathrm{4}\mathinner{\ldotp\ldotp}],\mathinner{\ldots}]}$ into a single sorted stream: there is no least element with which to start. Instead, we have to make the assumption that we have a sorted stream of sorted streams; then the binary merge can exploit the fact that the head of the left stream is the head of the result, without needing to examine the right stream. So, we define: [gif] This program is now productive, and primes yields the infinite sequence of prime numbers, using the genuine algorithm of Eratosthenes. Incidentally, although it is faithful, O'Neill (Reference O'Neill2009 ) points out that this program is not asymptotically optimal. After all, it is basically simulating her priority queues using nothing but ordered lists, incurring a logarithmic penalty. But that has no bearing on this paper. 3 The Approx Lemma Bird uses his circular program as an illustration of the Approx Lemma . Define [gif] Then we have Lemma 1 (Approx Lemma). For finite, partial, or infinite lists xs, ys , [gif] Note that [gif] ${\textit{approx}\;\mathrm{0}\;\textit{xs}}$ is undefined; the function [gif] ${\textit{approx}\;\textit{n}}$ preserves the outermost n constructors of a list, but then truncates anything deeper and replaces it with # ${\bot }$ (the undefined value), returning a partial list if the input was longer. That is, the lemma states that two lists are equal if (and of course only if) all their partial approximations agree. So to prove that primes does indeed produce the prime numbers, it suffices to prove that [gif] for all n, where # ${\textit{p}_{\textit{j}}}$ is the jth prime (we take [gif] ${\textit{p}_{\mathrm{1}}\;=\;\mathrm{2}}$ , counting the primes starting from one, for consistency with TFWH). Bird therefore defines [gif] and claims that [gif] To prove the claim, he observes that it is necessary for [gif] ${\ textit{crs}\;\textit{n}}$ to be well defined at least up to the first composite number greater than # ${\textit{p}_{\textit{n}\mathbin{+}\ mathrm{1}}}$ , because only then does [gif] ${\textit{crs}\;\textit {n}}$ deliver enough composite numbers to supply [gif] ${\textit{prs} \;(\textit{n}\mathbin{+}\mathrm{1})}$ , which will in turn supply [gif] ${\textit{crs}\;(\textit{n}\mathbin{+}\mathrm{1})}$ , and so on. It is what Bird calls a "non-trivial result in Number Theory" that [gif] ${\textit{p}_{\textit{n}\mathbin{+}\mathrm{1}}\mathbin{<} (\textit{p}_{\textit{n}})^{2}}$ , which places an upper bound on the composites required: it therefore suffices that [gif] where # ${\textit{c}_{j}}$ is the jth composite number (so [gif] ${\ textit{c}_{1}\;=\;\mathrm{4}}$ ) and [gif] ${\textit{c}_{m}\;=\;(\ textit{p}_{\textit{n}})^{2}}$ . Completing the proof is set as Exercise 9.I of TFWH, and Answer 9.I gives a hint about using induction to show that [gif] ${\textit{crs}\;(\textit{n}\mathbin{+}\ mathrm{1})}$ is the result of merging [gif] ${\textit{crs}\;\textit {n}}$ with [gif] ${\textit{multiples}\;\textit{p}_{\textit{n}\mathbin {+}\mathrm{1}}}$ .Footnote ^+ Unfortunately, the hint in Answer 9.I is at best unhelpful. For instance, it implies that [gif] ${\textit{crs}\;\mathrm{2}}$ (which equals [gif] ${\mathrm{4}\mathbin{:}\mathrm{6}\mathbin{:}\mathrm{8}\ mathbin{:}\mathrm{9}\mathbin{:}\bot }$ ) could be constructed from # ${\textit{crs}\;\mathrm{1}}$ (which equals [gif] ${\mathrm{4}\mathbin {:}\bot }$ ) and [gif] ${\textit{multiples}\;\mathrm{3}}$ (which equals [gif] ${[ \mathrm{9},\mathrm{12}\mathinner{\ldotp\ldotp}]}$ ). But where do the 6 and 8 come from? Nevertheless, the claim in Exercise 9.I is valid: the program is productive. What should the hint for the proof have been? 4 Proving the Sieve of Eratosthenes correct Here is a direct and non-recursive specification of the primes and composites: [gif] By convention, 1 is considered neither prime nor composite (Sloane, Reference Sloane1999). The interesting question is not really the elements of the lists, but productivity--that is, not so much showing that [gif] ${\textit {primes}_{\textit{spec}}}$ is a fixed point of [gif] ${makeP}{\;.\;} {makeC}$ , but that it is the least fixed point. So we state the following lemma without proof: Lemma 2 (relating specification and implementation) [gif] We will prove that [gif] ${\textit{primes}\;=\;\textit{primes}_{\ textit{spec}}}$ . 4.1 Approximations We will need two variations on approx, using a predicate instead of a count for termination: [gif] In words, [gif] ${\textit{approxWhile}\;\textit{p}\;\textit{xs}}$ gives the longest approximation to xs all of whose elements satisfy p , and [gif] ${\textit{approxUntil}\;\textit{p}\;\textit{xs}}$ gives the shortest approximation to xs containing an element satisfying p (or xs itself, if no element satisfies p). That is, approxUntil p stops with and includes the first element that satisfies p, whereas approxWhile p stops with and excludes the first element that fails to satisfy p. Our lists will be strictly increasing, and we will use an upper bound for approxWhile and a lower bound for approxUntil; for example, [gif] For integer x, we write " [gif] ${\textit{x}\in \textit{xs}}$ " when [gif] ${\textit{x}\;=\;\textit{xs}\mathbin{!!}\textit{n}}$ for some n , and say then that "xs is defined at least as far as x". 4.2 Properties of approximation The two functions approxWhile and approx are related by: Lemma 3 (introducing approxWhile). For strictly increasing, partial or infinite xs, [gif] provided that xs is defined at least as far as [gif] ${\textit{xs}\ mathbin{!!}\textit{n}}$ . Moreover, approxWhile and approxUntil are related by: Lemma 4 (approxWhile and approxUntil). For strictly increasing, partial or infinite xs with [gif] ${\textit{x}\in \textit{xs}}$ , [gif] and approxWhile and set difference by: Lemma 5 (approxWhile of difference). For strictly increasing, partial or infinite [gif] ${\textit{xs},\textit{ys}}$ with [gif] ${\textit{y} \in \textit{ys}}$ , [gif] ${\textit{x}\in (\textit{xs}\mathbin{\ backslash\mskip-2mu\backslash}\textit{ys})}$ , and [gif] ${\textit{x} \mathbin{<}\textit{y}}$ , [gif] and mergeAll and approx by: Lemma 6 (mergeAll and approx). For [gif] ${\textit{n}\geq \mathrm{0}} $ and partial or infinite strictly increasing list xss of properly infinite, strictly increasing lists, defined at least as far as [gif] ${\textit{xss}\mathbin{!!}\textit{n}}$ , [gif] Proof. By induction on n. Base case. For [gif] ${\textit{n}\;=\;\mathrm{0}}$ , we have [gif] Inductive step. Let [gif] ${\textit{n}\geq \mathrm{0}}$ and [gif] ${\ textit{b}\;=\;\textit{head}\;(\textit{xss}\mathbin{!!}\textit{n})}$ and assume as inductive hypothesis that [gif] Note the following property of merge and approxUntil: [gif] for infinite [gif] ${\textit{xs},\textit{ys}}$ with [gif] ${\textit {b}\in \textit{ys}}$ , since merge becomes undefined as soon as either argument does. Then we have [gif] 4.3 Bertrand's Postulate Bird's "non-trivial result in Number Theory" is Bertrand's Postulate (Bertrand, Reference Bertrand1845), which states that [gif] ${\textit {p}_{\textit{n}\mathbin{+}\mathrm{1}}\mathbin{<}\mathrm{2}\times\ textit{p}_{\textit{n}}}$ for [gif] ${\textit{n}\mathbin{>}\mathrm{0}} $ . For our purposes, the weakening [gif] ${\textit{p}_{\textit{n}\ mathbin{+}\mathrm{1}}\mathbin{<}(\textit{p}_{\textit{n}})^{2}}$ suffices; this is the key fact that makes Bird's program productive. We encapsulate this in the following proposition: Proposition 7 (number theory.) For [gif] ${\textit{n}\geq \mathrm{0}} $ , [gif] Informally, truncating the composites at [gif] ${(\textit{p}_{\textit {n}})^{2}}$ provides enough input for makeP to generate the primes at least as far as # ${\textit{p}_{\textit{n}\mathbin{+}\mathrm{1}}}$ . Proof of Proposition 7. For [gif] ${\textit{n}\geq \mathrm{1}}$ , [gif] The step invoking Lemma 5 is not valid when [gif] ${\textit{n}\;=\;\ mathrm{0}}$ , because # ${\textit{p}_{\mathrm{0}}}$ is undefined, and hence so too is the set difference. Nevertheless, the overall proposition [gif] still holds in that case, both sides being equal to [gif] ${\mathrm {2}\mathbin{:}\bot }$ . 4.4 Completing the proof We prove the following result: Proposition 8 (approximations). For all n, [gif] Proof. By induction on n. Base case. When [gif] ${\textit{n}\;=\;\mathrm{0}}$ , both equations trivially hold, because [gif] ${\textit{approx}\;\mathrm{0}}$ and # $ {\textit{p}_{\mathrm{0}}}$ are undefined. When [gif] ${\textit{n}\;= \;\mathrm{1}}$ , both equations hold by inspection. Inductive step. We now consider the case [gif] ${\textit{n}\mathbin {+}\mathrm{1}}$ with [gif] ${\textit{n}\mathbin{>}\mathrm{0}}$ . Assume the inductive hypothesis [gif] Note that the second equation implies that [gif] ${\textit {composites}}$ is defined at least as far as [gif] ${(\textit{p}_{\ textit{n}})^{2}}$ . Therefore, by Proposition 7, also [gif] ${\textit {makeP}\;(\textit{approxWhile}\;(\leq (\textit{p}_{\textit{n}})^{2}) \;\textit{composites})} $ is defined at least as far as # ${\textit {p}_{\textit{n}\mathbin{+}\mathrm{1}}}$ . We refer to these facts as " [gif] ${(\textit{p}_{\textit{n}})^{2}}$ is present in composites" and " # ${\textit{p}_{\textit{n}\mathbin{+}\mathrm{1}}}$ is present in primes" below. Then we have: [gif] For the two steps marked # ${(\mathbin{\ast})}$ , we switch freely between [gif] ${\textit{makeP}\;\textit{cs}\;=\;\mathrm{2}\mathbin{:} ([ \mathrm{3}\mathinner{\ldotp\ldotp}]\mathbin{\backslash\mskip-2mu\ backslash}\textit{cs})}$ and [gif] ${[ \mathrm{2}\mathinner{\ldotp\ ldotp}]\mathbin{\backslash\mskip-2mu\backslash}\textit{cs}}$ for different values of * ${\textit{cs}}$ ; this is sound, because in both cases cs is defined at least as far as its head, namely 4. This deals with the first equation. In particular, primes is defined at least as far as # ${\textit{p}_{\textit{n}\mathbin{+}\mathrm{1}}}$ . For the second equation, let [gif] ${\textit{b}\;=\;(\textit{p}_{\ textit{n}\mathbin{+}\mathrm{1}})^{2}}$ , so that [gif] Then [gif] In particular, b is in composites; therefore also [gif] by Lemma 4, dealing with the second equation too. Finally, we have: Theorem 9 (the primes program is correct). [gif] Proof. A direct corollary of Proposition 8, by Lemma 1. This completes the proof of correctness of Bird's program. 5 Conclusion Total Functional Programming: As discussed in the introduction, David Turner's ambition (Turner, Reference Turner2004) was for future programming languages that were "designed to exclude the possibility of non-termination". He observed that most programs are already structurally recursive or corecursive, therefore guaranteed respectively terminating or productive, and conjectured that "with more practice we will find this is always true". He explicitly admits in that paper that "rewriting the well known sieve of Eratosthenes program [by which he means trial division] in this discipline involves coding in some bound on the distance from one prime to the next". We have coded that bound by appeal to a weakening of Bertrand's Postulate (Proposition 7)--but Turner's vision would require that appeal at least to be acknowledged by the totality checker. One could go as far as full dependent types, in which case the relevant assumption can be formally expressed as a theorem. But still, one would either have to prove the theorem--a decidedly non-trivial matter (Thery, Reference Thery2003)--or accept it as an unverified axiom; Turner said that he was "interested in finding something simpler" than full dependent types. Much as I find Turner's vision for total functional programming appealing, I fear that we are still some way off, even after 20 years of "more practice". However, I would be delighted to be shown to be unnecessarily pessimistic. Trial division: Turner popularized the trial division algorithm in various publications; I believe that the earliest of these is the SASL Manual. Interestingly, SASL changed from eager semantics (Turner, Reference Turner1975) to lazy semantics (Turner, Reference Turner1976); the primes program appears only in the later of those two documents, despite them both having the same technical report number. (List comprehensions appeared with KRC (Turner, Reference Turner, Darlington, Henderson and Turner1982), originally called "ZF expressions", apparently being retrofitted to SASL the following year (Turner, Reference Turner1983); the 1976 primes program was written instead with a filter.) Turner (Reference Turner2020) acknowledged that the program appeared in a famous paper by Kahn & MacQueen ( Reference Kahn and MacQueen1977): Did I see a preprint of that in 1976? I don't recall but it's possible, in which case my contribution was to express the idea using recursion and lazy lists. The program also appeared in papers about the dataflow language Lucid; for example, Ashcroft & Wadge (Reference Ashcroft and Wadge 1977) again attribute it to Kahn. Kahn & MacQueen (Reference Kahn and MacQueen1977) in turn credit it to McIlroy (Reference McIlroy1968). McIlroy (Reference McIlroy2014) recordsFootnote ^++ : For examples in a talk at the Cambridge Computing Laboratory (1968) I cooked up some interesting coroutine-based programs. One, a prime-number sieve, became a classic, spread by word of mouth. Turner (Reference Turner1976), Kahn & MacQueen (Reference Kahn and MacQueen1977), and Wadge & Ashcroft (Reference Wadge and Ashcroft1985 ) call the trial division algorithm "The Sieve of Eratosthenes", but McIlroy (Reference McIlroy1968, Reference McIlroy2014) does not. Proofs about infinite lists: In developing this proof, we also considered an ApproxWhile Lemma, analogous to the Approx Lemma (Lemma 1): Lemma (ApproxWhile Lemma). For any infinite sequence [gif] ${{b}_{0}\ mathbin{<}{b}_{1}\mathbin{<}\mathinner{\,.\,}}$ of integer bounds, and two lists [gif] ${\textit{xs},\textit{ys}}$ of integers, whether finite, partial, or infinite, [gif] But this is much less general: the elements must now be ordered; and moreover, the bounds must grow without limit, so it doesn't hold universally for rationals, or pairs, or strings. Note that we used naturality of approx in the proof of Proposition 8; the corresponding property of approxWhile is not so straightforward. Perhaps it is possible to phrase a proof in terms solely of approxWhile without using approx? We have not pursued this further. Bird's exercise: What of TFWH (Bird, Reference Bird2014)? This paper was prompted by a series of ten emails from Francisco Lieberich (Lieberich, Reference Lieberich2018) pointing out this and other errors in the book. Recall that Bird's hint towards the proof implies that [gif] ${\textit{crs}\;\mathrm{2}\;=\;\mathrm{4}\mathbin{:}\ mathrm{6}\mathbin{:}\mathrm{8}\mathbin{:}\mathrm{9}\mathbin{:}\bot }$ can be obtained by merging [gif] ${\textit{crs}\;\mathrm{1}\;=\;\ mathrm{4}\mathbin{:}\bot }$ and [gif] ${\textit{multiples}\;\mathrm {3}\;=\;[ \mathrm{9},\mathrm{12}\mathinner{\ldotp\ldotp}]}$ . In fact, a more helpful hint that Bird could have given is that # ${\ textit{crs}\;\mathrm{2}}$ can be constructed from # ${\textit{crs}\;\ mathrm{1}}$ alone, without needing [gif] ${\textit{multiples}\;\ mathrm{3}}$ at all: [gif] ${\textit{crs}\;\mathrm{2}\;=\;\textit {makeC}\;(\textit{makeP}\;(\textit{crs}\;\mathrm{1}))}$ . This doesn't quite work for higher values, because the right-hand side is too productive: [gif] ${\textit{makeC}\;(\textit{makeP}\;(\textit {crs}\;\mathrm{2}))}$ yields the composites up to 49, whereas # ${\ textit{crs}\;\mathrm{3}}$ needs composites only up to [gif] ${(\ textit{p}_{\mathrm{3}})^{2}\;=\;\mathrm{25}}$ . A tighter but still sufficient condition is [gif] I have added that observation to the errata for the book (Bird, Reference Bird2014). Nevertheless, the margin of TFWH is too narrow to contain the proof presented here, so I still have no appropriate correction to apply. Acknowledgements I am grateful for helpful comments on this work throughout its gestation, from members of the Algebra of Programming research group at Oxford (especially Geraint Jones, Guillaume Boisseau, and Zhixuan Yang) and IFIP Working Group 2.1 (especially Tom Schrijvers), and from the anonymous JFP reviewers. Thanks are due to Francisco Lieberich for alerting me to the error in TFWH, among many other errors. And of course this paper couldn't have happened without the seminal contributions of David Turner and Richard Bird. Conflicts of interest None. Supplementary material For supplementary material for this article, please visit https:// doi.org/10.1017/S0956796824000194. --------------------------------------------------------------------- Footnotes * JFP doesn't list O'Neill's paper as a Pearl, but this was a production error (Tranah Reference Tranah2024). + Incidentally, there is a typo in TFWH: the body of the chapter, the exercise, and its solution all have " ${\textit{m}\;=\;(\textit{p}_{\ textit{n}})^{2}}$ " instead of " ${\textit{c}_{m}\;=\;(\textit{p}_{\ textit{n}})^{2}}$ ". ++ Turner was an undergraduate at Oxford before starting his DPhil there in 1969, so it seems unlikely that he was present at McIlroy's talk in Cambridge. I conjecture that Turner learnt of the program via someone who did attend--perhaps Christopher Strachey, Turner's original DPhil supervisor. --------------------------------------------------------------------- References Ashcroft, E. A. & Wadge, W. W. (1977) Lucid, a nonprocedural language with iteration. Comm. ACM. 20(7), 519-526.CrossRefGoogle Scholar Bertrand, J. (1845) Memoire sur le nombre de valeurs que peut prendre une fonction quand on y permute les lettres qu'elle renferme. J. l'Ecole Royale Polytech. 18 (Cahier 30), 123-140. In French; see also https://en.wikipedia.org/wiki/Bertrand's_postulate.Google Scholar Bird, R. (2014) Thinking Functionally with Haskell. Cambridge University. https://www.cs.ox.ac.uk/publications/books/functional/. CrossRefGoogle Scholar Gibbons, J. & Jones, G. (1998) The under-appreciated unfold. In International Conference on Functional Programming. Baltimore, Maryland, pp. 273-279.CrossRefGoogle Scholar Kahn, G. & MacQueen, D. B. (1977) Coroutines and networks of parallel processes. In IFIP Congress. IFIP, pp. 993-998.Google Scholar Lieberich, F. (2018) "Errata". Personal communication (email).Google Scholar McIlroy, M. D. (1968) Coroutines. Internal report. Bell Telephone Laboratories. Murray Hill, New Jersey. http://www.iq0.com/notes/ coroutine.html.Google Scholar McIlroy, M. D. (2014) Coroutine prime number sieve. https:// www.cs.dartmouth.edu/doug/sieve/sieve.pdf.Google Scholar Meertens, L. (2004) Calculating the Sieve of Eratosthenes. J. Funct. Program. 14(6), 759-763.CrossRefGoogle Scholar O'Neill, M. E. (2009) The genuine Sieve of Eratosthenes. J. Funct. Program. 19(1), 95-105.CrossRefGoogle Scholar Sloane, N. (1999) The composite numbers. In The On-Line Encyclopedia of Integer Sequences. https://oeis.org/A002808.Google Scholar Thery, L. (2003) Proving pearl: Knuth's algorithm for prime numbers. In Theorem Proving in Higher Order Logic. Springer, pp. 304-318. CrossRefGoogle Scholar Tranah, D. (2024) "JFP 622". Personal communication (email).Google Scholar Turner, D. A. (1975) SASL language manual. Technical Report CS/75/1. University of St Andrews, Dept of Computational Science. Revised 16/9 /75.Google Scholar Turner, D. A. (1976) SASL language manual. Technical Report CS/75/1. University of St Andrews, Dept of Computational Science. Revised 1/12 /76.Google Scholar Turner, D. A. (1982) Recursion equations as a programming language. In Functional Programming and its Applications, Darlington, J., Henderson, P. & Turner, D. A. (eds). Cambridge University, pp. 1-28. CrossRefGoogle Scholar Turner, D. A. (1983) SASL language manual, "revised November 1983 for inclusion of ZF expressions". Technical report.Google Scholar Turner, D. A. (2004) Total functional programming. J. Univers. Comput. Sci. 10(7), 751-768.Google Scholar Turner, D. A. (2020) "SASL manual". Personal communication (email). Google Scholar Wadge, W. W. & Ashcroft, E. A. (1985) Lucid, the Dataflow Programming Language. Academic.Google Scholar [svg] Gibbons supplementary material Gibbons supplementary material Download Gibbons supplementary material(Video) Video 18.7 MB Submit a response --------------------------------------------------------------------- Discussions No Discussions have been published for this article. [svg] You have Access [svg] Open access Cited by Loading... [svg] Cited by * Crossref logo 0 * Google Scholar logo No CrossRef data available. Google Scholar Citations View all Google Scholar citations for this article. x Cambridge University Press Our Site * Accessibility * Contact & Help * Legal Notices Our Platforms * Cambridge Core * Cambridge Open Engage * Cambridge Higher Education Our Products * Journals * Books * Elements * Textbooks * Courseware Join us online * * * * * Location [GBR ] Please choose a valid location. Update Legal Information * Rights & Permissions * Copyright * Privacy Notice * Terms of Use * Cookies Policy Cambridge University Press 2025 Cancel Confirm x Save article to Kindle To send this article to your Kindle, first ensure no-reply@cambridge.org is added to your Approved Personal Document E-mail List under your Personal Document Settings on the Manage Your Content and Devices page of your Amazon account. Then enter the 'name' part of your Kindle email address below. Find out more about sending to your Kindle. Find out more about saving to your Kindle. Note you can select to save to either the @free.kindle.com or @kindle.com variations. '@free.kindle.com' emails are free but can only be saved to your device when it is connected to wi-fi. '@kindle.com' emails can be delivered even when you are not connected to wi-fi, but note that service fees apply. Find out more about the Kindle Personal Document Service. Turner, Bird, Eratosthenes: An eternal burning thread * Volume 35 * JEREMY GIBBONS ^(a1) * DOI: https://doi.org/10.1017/S0956796824000194 Your Kindle email address [ ] Please provide your Kindle email. (*)@free.kindle.com ( )@kindle.com (service fees apply) Available formats [ ] PDF Please select a format to save. [ ] By using this service, you agree that you will only keep content for personal use, and will not openly distribute them via Dropbox, Google Drive or other file sharing services Please confirm that you accept the terms of use. Cancel Save x Save article to Dropbox To save this article to your Dropbox account, please select one or more formats and confirm that you agree to abide by our usage policies. If this is the first time you used this feature, you will be asked to authorise Cambridge Core to connect with your Dropbox account. Find out more about saving content to Dropbox. Turner, Bird, Eratosthenes: An eternal burning thread * Volume 35 * JEREMY GIBBONS ^(a1) * DOI: https://doi.org/10.1017/S0956796824000194 Available formats [ ] PDF Please select a format to save. [ ] By using this service, you agree that you will only keep content for personal use, and will not openly distribute them via Dropbox, Google Drive or other file sharing services Please confirm that you accept the terms of use. Cancel Save x Save article to Google Drive To save this article to your Google Drive account, please select one or more formats and confirm that you agree to abide by our usage policies. If this is the first time you used this feature, you will be asked to authorise Cambridge Core to connect with your Google Drive account. Find out more about saving content to Google Drive. Turner, Bird, Eratosthenes: An eternal burning thread * Volume 35 * JEREMY GIBBONS ^(a1) * DOI: https://doi.org/10.1017/S0956796824000194 Available formats [ ] PDF Please select a format to save. [ ] By using this service, you agree that you will only keep content for personal use, and will not openly distribute them via Dropbox, Google Drive or other file sharing services Please confirm that you accept the terms of use. Cancel Save x x Reply to: Submit a response Title * [ ] Please enter a title for your response. Contents * Contents help Close Contents help - No HTML tags allowed - Web page URLs will display as text only - Lines and paragraphs break automatically - Attachments, images or tables are not permitted [ ] [ ] [ ] [ ] [ ] Please enter your response. --------------------------------------------------------------------- Your details First name * [ ] Please enter your first name. Last name * [ ] Please enter your last name. Email * Email help Close Email help Your email address will be used in order to notify you when your comment has been reviewed by the moderator and in case the author(s) of the article or the moderator need to contact you directly. [ ] Please enter a valid email address. Occupation [ ] Please enter your occupation. Affiliation [ ] Please enter any affiliation. [Add contributor] --------------------------------------------------------------------- You have entered the maximum number of contributors --------------------------------------------------------------------- Conflicting interests Do you have any conflicting interests? * Conflicting interests help Close Conflicting interests help Please list any fees and grants from, employment by, consultancy for, shared ownership in or any close relationship with, at any time over the preceding 36 months, any organisation whose interests may be affected by the publication of the response. Please also list any non-financial associations or interests (personal, professional, political, institutional, religious or other) that a reasonable reader would want to know about in relation to the submitted work. This pertains to all the authors of the piece, their spouses or partners. ( ) Yes (*) No [ ] [ ] More information * [ ] Please enter details of the conflict of interest or select 'No'. --------------------------------------------------------------------- [ ] Please tick the box to confirm you agree to our Terms of use. * Please accept terms of use. [ ] Please tick the box to confirm you agree that your name, comment and conflicts of interest (if accepted) will be visible on the website and your comment may be printed in the journal at the Editor's discretion. * Please confirm you agree that your details will be displayed. --------------------------------------------------------------------- [Submit]