Reference. Turner, Bird, Eratosthenes: An eternal burning thread
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.
Cite
Cites 19 works (0 here)
External (19)
- "JFP 622" (personal communication) (2024)
- "SASL manual" (personal communication) (2020)
- "Errata" (personal communication) (2018)
- Thinking Functionally with Haskell (2014)
- Coroutine prime number sieve (2014)
- The Genuine Sieve of Eratosthenes (2009)
- Calculating the Sieve of Eratosthenes (2004)
- Total functional programming (2004)
- Proving Pearl: Knuth's Algorithm for Prime Numbers (2003)
- The composite numbers (OEIS A002808) (1999)
- The under-appreciated unfold (1998)
- Lucid, the Dataflow Programming Language (1985)
- SASL language manual, revised November 1983 for inclusion of ZF expressions (1983)
- Recursion Equations as a Programming Language (1982)
- Lucid, a nonprocedural language with iteration (1977)
- Coroutines and networks of parallel processes (1977)
- SASL language manual (revised 1/12/76) (1976)
- SASL language manual (revised 16/9/75) (1975)
- Mémoire sur le nombre de valeurs que peut prendre une fonction quand on y permute les lettres qu’elle renferme (1845)