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:

where

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 ${makeP}{\;.\;}{makeC}$ .

Here, ${(\mathbin{\backslash\mskip-2mu\backslash})}$ is the obvious implementation of list difference of strictly increasing streams, hence representing set difference:

and ${\textit{multiples}\;\textit{p}}$ generates the multiples of p starting with ${\textit{p}^{2}}$ :

Thus, the composites are obtained by merging together the infinite stream of infinite streams ${[ [ \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 ${\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:

Then mergeAll is basically a stream fold with merge. You might think you could define this simply by ${\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 ${[ [ \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:

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

Then we have

Lemma 1 (Approx Lemma). For finite, partial, or infinite lists xs, ys,

Note that ${\textit{approx}\;\mathrm{0}\;\textit{xs}}$ is undefined; the function ${\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

for all n, where ${\textit{p}_{\textit{j}}}$ is the jth prime (we take ${\textit{p}_{\mathrm{1}}\;=\;\mathrm{2}}$ , counting the primes starting from one, for consistency with TFWH). Bird therefore defines

and claims that

To prove the claim, he observes that it is necessary for ${\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 ${\textit{crs}\;\textit{n}}$ deliver enough composite numbers to supply ${\textit{prs}\;(\textit{n}\mathbin{+}\mathrm{1})}$ , which will in turn supply ${\textit{crs}\;(\textit{n}\mathbin{+}\mathrm{1})}$ , and so on. It is what Bird calls a “non-trivial result in Number Theory” that ${\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

where ${\textit{c}_{j}}$ is the jth composite number (so ${\textit{c}_{1}\;=\;\mathrm{4}}$ ) and ${\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 ${\textit{crs}\;(\textit{n}\mathbin{+}\mathrm{1})}$ is the result of merging ${\textit{crs}\;\textit{n}}$ with ${\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 ${\textit{crs}\;\mathrm{2}}$ (which equals ${\mathrm{4}\mathbin{:}\mathrm{6}\mathbin{:}\mathrm{8}\mathbin{:}\mathrm{9}\mathbin{:}\bot }$ ) could be constructed from ${\textit{crs}\;\mathrm{1}}$ (which equals ${\mathrm{4}\mathbin{:}\bot }$ ) and ${\textit{multiples}\;\mathrm{3}}$ (which equals ${[ \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:

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 ${\textit{primes}_{\textit{spec}}}$ is a fixed point of ${makeP}{\;.\;}{makeC}$ , but that it is the least fixed point. So we state the following lemma without proof:

Lemma 2 (relating specification and implementation)

We will prove that ${\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:

In words, ${\textit{approxWhile}\;\textit{p}\;\textit{xs}}$ gives the longest approximation to xs all of whose elements satisfy p, and ${\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,

For integer x, we write “ ${\textit{x}\in \textit{xs}}$ ” when ${\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,

provided that xs is defined at least as far as ${\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 ${\textit{x}\in \textit{xs}}$ ,

and approxWhile and set difference by:

Lemma 5 (approxWhile of difference). For strictly increasing, partial or infinite ${\textit{xs},\textit{ys}}$ with ${\textit{y}\in \textit{ys}}$ , ${\textit{x}\in (\textit{xs}\mathbin{\backslash\mskip-2mu\backslash}\textit{ys})}$ , and ${\textit{x}\mathbin{<}\textit{y}}$ ,

and mergeAll and approx by:

Lemma 6 (mergeAll and approx). For ${\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 ${\textit{xss}\mathbin{!!}\textit{n}}$ ,

Proof. By induction on n.

Base case. For ${\textit{n}\;=\;\mathrm{0}}$ , we have

Inductive step. Let ${\textit{n}\geq \mathrm{0}}$ and ${\textit{b}\;=\;\textit{head}\;(\textit{xss}\mathbin{!!}\textit{n})}$ and assume as inductive hypothesis that

Note the following property of merge and approxUntil:

for infinite ${\textit{xs},\textit{ys}}$ with ${\textit{b}\in \textit{ys}}$ , since merge becomes undefined as soon as either argument does. Then we have

4.3 Bertrand’s Postulate

Bird’s “non-trivial result in Number Theory” is Bertrand’s Postulate (Bertrand, Reference Bertrand1845), which states that ${\textit{p}_{\textit{n}\mathbin{+}\mathrm{1}}\mathbin{<}\mathrm{2}\times\textit{p}_{\textit{n}}}$ for ${\textit{n}\mathbin{>}\mathrm{0}}$ . For our purposes, the weakening ${\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 ${\textit{n}\geq \mathrm{0}}$ ,

Informally, truncating the composites at ${(\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 ${\textit{n}\geq \mathrm{1}}$ ,

The step invoking Lemma 5 is not valid when ${\textit{n}\;=\;\mathrm{0}}$ , because ${\textit{p}_{\mathrm{0}}}$ is undefined, and hence so too is the set difference. Nevertheless, the overall proposition

still holds in that case, both sides being equal to ${\mathrm{2}\mathbin{:}\bot }$ .

4.4 Completing the proof

We prove the following result:

Proposition 8 (approximations). For all n,

Proof. By induction on n.

Base case. When ${\textit{n}\;=\;\mathrm{0}}$ , both equations trivially hold, because ${\textit{approx}\;\mathrm{0}}$ and ${\textit{p}_{\mathrm{0}}}$ are undefined. When ${\textit{n}\;=\;\mathrm{1}}$ , both equations hold by inspection.

Inductive step. We now consider the case ${\textit{n}\mathbin{+}\mathrm{1}}$ with ${\textit{n}\mathbin{>}\mathrm{0}}$ . Assume the inductive hypothesis

Note that the second equation implies that ${\textit{composites}}$ is defined at least as far as ${(\textit{p}_{\textit{n}})^{2}}$ . Therefore, by Proposition 7, also ${\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 “ ${(\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:

For the two steps marked ${(\mathbin{\ast})}$ , we switch freely between ${\textit{makeP}\;\textit{cs}\;=\;\mathrm{2}\mathbin{:}([ \mathrm{3}\mathinner{\ldotp\ldotp}]\mathbin{\backslash\mskip-2mu\backslash}\textit{cs})}$ and ${[ \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 ${\textit{b}\;=\;(\textit{p}_{\textit{n}\mathbin{+}\mathrm{1}})^{2}}$ , so that

Then

In particular, b is in composites; therefore also

by Lemma 4, dealing with the second equation too.

Finally, we have:

Theorem 9 (the primes program is correct).

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 (Théry, Reference Théry2003)—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):

The program also appeared in papers about the dataflow language Lucid; for example, Ashcroft & Wadge (Reference Ashcroft and Wadge1977) again attribute it to Kahn. Kahn & MacQueen (Reference Kahn and MacQueen1977) in turn credit it to McIlroy (Reference McIlroy1968). McIlroy (Reference McIlroy2014) recordsFootnote ^‡ :

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):

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 ${\textit{crs}\;\mathrm{2}\;=\;\mathrm{4}\mathbin{:}\mathrm{6}\mathbin{:}\mathrm{8}\mathbin{:}\mathrm{9}\mathbin{:}\bot }$ can be obtained by merging ${\textit{crs}\;\mathrm{1}\;=\;\mathrm{4}\mathbin{:}\bot }$ and ${\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 ${\textit{multiples}\;\mathrm{3}}$ at all: ${\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: ${\textit{makeC}\;(\textit{makeP}\;(\textit{crs}\;\mathrm{2}))}$ yields the composites up to 49, whereas ${\textit{crs}\;\mathrm{3}}$ needs composites only up to ${(\textit{p}_{\mathrm{3}})^{2}\;=\;\mathrm{25}}$ . A tighter but still sufficient condition is

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.