50847534

⎕io←0 throughout.

I was re-reading A Mathematician’s Apology before recommending it to Suki Tekverk, our summer intern, and came across a statement that the number of primes less than 1e9 is 50847478 (§14, page 23). The function pco from the dfns workspace does computations on primes; ¯1 pco n is the number of primes less than n:

      )copy dfns pco

      ¯1 pco 1e9
50847534

The two numbers 50847478 and 50847534 cannot both be correct. A search of 50847478 on the internet reveals that it is incorrect and that 50847534 is correct. 50847478 is erroneously cited in various textbooks and even has a name, Bertelsen’s number, memorably described by MathWorld as “an erroneous name erroneously given the erroneous value of π(1e9) = 50847478.”

Although several internet sources give 50847534 as the number of primes less than 1e9, they don’t provide a proof. Relying on them would be doing the same thing — arguing from authority — that led other authors astray, even if it is the authority of the mighty internet. Besides, I’d already given Suki, an aspiring mathematician, the standard spiel about the importance of proof.

How do you prove the 50847534 number? One way is to prove correct a program that produces it. Proving pco correct seems daunting — it has 103 lines and two large tables. Therefore, I wrote a function from scratch to compute the number of primes less than , a function written in a way that facilitates proof.

sieve←{
  b←⍵⍴{∧⌿↑(×/⍵)⍴¨~⍵↑¨1}2 3 5
  b[⍳6⌊⍵]←(6⌊⍵)⍴0 0 1 1 0 1
  49≥⍵:b
  p←3↓{⍵/⍳⍴⍵}∇⌈⍵*0.5
  m←1+⌊(⍵-1+p×p)÷2×p
  b ⊣ p {b[⍺×⍺+2×⍳⍵]←0}¨ m
}

      +/ sieve 1e9
50847534

sieve ⍵ produces a boolean vector b with length such that b/⍳⍴b are all the primes less than . It implements the sieve of Eratosthenes: mark as not-prime multiples of each prime less than ⍵*0.5; this latter list of primes obtains by applying the function recursively to ⌈⍵*0.5. Some obvious optimizations are implemented:

  • Multiples of 2 3 5 are marked by initializing b with ⍵⍴{∧⌿↑(×/⍵)⍴¨~⍵↑¨1}2 3 5 rather than with ⍵⍴1.
  • Subsequently, only odd multiples of primes > 5 are marked.
  • Multiples of a prime to be marked start at its square.

Further examples:

      +/∘sieve¨ ⍳10
0 0 0 1 2 2 3 3 4 4

      +/∘sieve¨ 10*⍳10
0 4 25 168 1229 9592 78498 664579 5761455 50847534

There are other functions which are much easier to prove correct, for example, sieve1←{2=+⌿0=(⍳3⌈⍵)∘.|⍳⍵}. However, sieve1 requires O(⍵*2) space and sieve1 1e9 cannot produce a result with current technology. (Hmm, a provably correct program that cannot produce the desired result …)

We can test that sieve is consistent with pco and that pco is self-consistent. pco is a model of the p: primitive function in J. Its cases are:
   pco n   the n-th prime
¯1 pco n   the number of primes less than n
 1 pco n   1 iff n is prime
 2 pco n   the prime factors and exponents of n
 3 pco n   the prime factorization of n
¯4 pco n   the next prime < n
 4 pco n   the next prime > n
10 pco r,s a boolean vector b such that r+b/⍳⍴b are the primes in the half-open interval [r,s).

      ¯1 pco 10*⍳10      ⍝ the number of primes < 1e0 1e1 ... 1e9
0 4 25 168 1229 9592 78498 664579 5761455 50847534

      +/ 10 pco 0 1e9    ⍝ sum of the sieve between 0 and 1e9
50847534
                         ⍝ sum of sums of 10 sieves
                         ⍝ each of size 1e8 from 0 to 1e9
      +/ t← {+/10 pco ⍵+0 1e8}¨ 1e8×⍳10
50847534
                         ⍝ sum of sums of 1000 sieves
                         ⍝ each of size 1e6 from 0 to 1e9
      +/ s← {+/10 pco ⍵+0 1e6}¨ 1e6×⍳1000
50847534

      t ≡ +/ 10 100 ⍴ s
1
                         ⍝ sum of sums of sieves with 1000 randomly
                         ⍝ chosen end-points, from 0 to 1e9
      +/ 2 {+/10 pco ⍺,⍵}/ 0,({⍵[⍋⍵]}1000?1e9),1e9
50847534

      ¯1 pco 1e9         ⍝ the number of primes < 1e9
50847534
      pco 50847534       ⍝ the 50847534-th prime
1000000007
      ¯4 pco 1000000007  ⍝ the next prime < 1000000007
999999937
      4 pco 999999937    ⍝ the next prime > 999999937
1000000007     
      4 pco 1e9          ⍝ the next prime > 1e9
1000000007

                         ⍝ are 999999937 1000000007 primes?
      1 pco 999999937 1000000007
1 1
                         ⍝ which of 999999930 ... 1000000009
                         ⍝ are prime?
      1 pco 999999930+4 20⍴⍳80
0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 0 1

      +/∘sieve¨ 999999937 1000000007 ∘.+ ¯1 0 1
50847533 50847533 50847534
50847534 50847534 50847535

Constructions

Suki Tekverk, a summer intern, spent the last two weeks here studying APL. She will be a high school senior next September and is adept in math, so in addition to APL we also considered some math problems, proofs, and proof techniques, including the following:

Given line segments x and y, construct (using compass and straight-edge) line segments for the following values:
   x+y
   x-y
   x×y
   x÷y

The first two are immediate. Constructing the last two are straightforward if you are also given 1 (or some other reference length from which to construct 1). Can you construct x×y and x÷y without 1?

Constructing x÷y is impossible if you are not given 1 : From x and y alone you can not determine how they compare to 1. If you can construct x÷y, then you can construct x÷x and therefore relate x and y to 1, contradicting the previous statement.

Can you construct x×y without 1? I got stuck (and lazy) and posed the question to the J Chat Forum, and received a solution from Raul Miller in less than half an hour. Miller’s proof recast in terms similar to that for x÷y is as follows:

From x and y alone you can not determine how they compare to 1. If you can construct x×y, then you can construct x×x, whence:
   if x<x×x then x>1
   if x=x×x then x=1
   if x>x×x then x<1
contradicting the previous statement.

I last thought about this problem in my first year of college many decades ago. At the time Norman M. (a classmate) argued that there must be a 1 and then did the construction for x÷y using 1. I recall he said “there must be a 1” in the sense of “1 has to exist if x and y exist” rather than that “you have to use a 1 in the construction” or “you can not construct x÷y without using 1”. I don’t remember what we did with x×y; before Miller’s message I had some doubt that perhaps we were able to construct x×y without using 1 all those years ago. (Norman went on to get a Ph.D. at MIT and other great things.)

The Story of a Summer Intern

by Suki Tekverk

As a born and raised New Yorker, I thought I had seen it all, but two short weeks spent in Vancouver with Roger Hui and his family proved me very wrong! I went from being at the top of the totem pole to one of the most clueless people around. Luckily, these new experiences provoked new paths of thought and ultimately left me more prepared to face the world than I was when my plane shakily landed in this foreign place.

Upon my arrival, I was greeted by Stella, Roger’s wife, and their children, Nicholas and Rachel, who promptly made me a sign for my bedroom door, making me feel right at home.

The next morning, I went right to work, unsuccessfully writing a dfn for the Fibonacci sequence. After struggling for at least 40 minutes, Roger showed me a solution. This solution was nearly the exact definition of the Fibonacci sequence, setting a precedent for the uncomplicated and direct solutions that ensued. Over the next week we ripped through a Monty Hall simulation, recursive Peano addition and multiplication, recursive and non-recursive binomial coefficients, the Cantor set, the Sierpinski Carpet and more. Over this week, I not only discovered new realms of mathematics but also ate foreign food, hiked through a canyon, watched a Chinese film, made cookies, went to a horse ranch, listened to an orchestra performance, experienced sugar withdrawal and saw a sunset on a mountain. This was just the first week.

The main focus of week two was proofs. At first, I was skeptical of the value of writing proofs in APL as opposed to writing them on paper, but being able to run each step of the proof was quite useful. I started with proof by induction, then by contradiction. After learning the basics I proved the sum of an arithmetic series, sum of geometric series, sum of integers, sum of odd integers and sum of binomial coefficients. This week showed me how closely APL and mathematical notation align. However, I am still annoyed by the fact that the order of operations isn’t how I learnt it in school; it will take some getting used to. My next task will be buying a Windows computer for APL.

Overall, these two weeks in Vancouver were a great learning experience on many levels. Coding in APL has led me to consider possible career options as well as help me understand the nature of the language. Living in a city so far away from home made me question things I considered commonplace and forced me to realize that New York is only a small part of a much larger world.

Loops, Folds and Tuples

For-loops
Given an initial state defined by a number of variables, a for-loop iterates through its argument array modifying the state.

    A←... ⋄ B←... ⋄ C←...       ⍝ initial state
    :For item :In items         ⍝ iterating through array "items"
        A←A ... item            ⍝ new value for A depending on item
        C←C ... A ... item      ⍝ new value for C depending on A and item
        ...                     ⍝ state updated
    :EndFor
    A B C                       ⍝ final state

In the above example the state comprises just three variables. In general, it may be arbitrarily complex, as can the interactions between its various components within the body of the loop.

Dfns
Dfns don’t have for-loops. Instead, we can use reduction (or “fold”) with an accumulating vector “tuple” of values representing the state. Here is the D-equivalent of the above code:

    ⊃{                      ⍝ next item is ⍺
        (A B C)←⍵           ⍝ named items of tuple ⍵
        A∆←A ... ⍺          ⍝ new value for A depending on item ⍺
        C∆←C ... A∆ ... ⍺   ⍝ new value for C depending on A∆ and item ⍺
        ...                 ⍝ ...
        A∆ B C∆             ⍝ "successor" tuple (A and C changed)
    }/(⌽items),⊂A B C       ⍝ for each item and initial state tuple A B C

In this coding, the accumulating tuple arrives as the right argument (⍵) of the operand function, with the next “loop item” on the left (⍺). Notice how the items vector is reversed (⌽items) so that the items arrive in index-order in the right-to-left reduction.

If you prefer your accumulator to be on the left, you can replace the primitive reduction operator (/) with Phil Last’s foldl operator, which also presents its loop items in index-order:

    foldl←{⊃⍺⍺⍨/(⌽⍵),⊂⍺}    ⍝ fold left

then:

    A B C {                 ⍝ final state from initial state (left argument)
        (A B C)←⍺           ⍝ named items of tuple ⍺
        A∆←A ... ⍵          ⍝ new value for A depending on item ⍵
        C∆←C ... A∆ ... ⍵   ⍝ new value for C depending on A∆ and item ⍵
        A∆ B C∆             ⍝ successor tuple (A and C changed)
    } foldl items

If the number of elements in the state tuple is large, it can become unwieldy to name each on entry and exit to the operand function. In this case it simplifies the code to name the indices of the tuple vector, together with an at operator to denote the items of its successor:

    T ← (...) (...) ...         ⍝ intitial state tuple T
    A B C D ... ← ⍳⍴T           ⍝ A B C D ... are tuple item "names"

    T {                         ⍝ final state from initial state (left argument)
        A∆←(A⊃⍺) ... ⍵          ⍝ new value for A depending on item ⍵
        C∆←(C⊃⍺) ... A∆ ... ⍵   ⍝ new value for C depending on A∆ and item ⍵
        A∆ C∆(⊣at A C)⍺         ⍝ successor tuple (A and C changed)
    } foldl items

where:

    at←{A⊣A[⍵⍵]←⍺ ⍺⍺(A←⍵)[⍵⍵]}   ⍝ (⍺ ⍺⍺ ⍵) at ⍵⍵ in ⍵

There is some discussion about providing a primitive operator @ for at in Dyalog V16.

Examples
Function kk illustrates naming tuple elements (S E K Q) at the start of the operand function.
Function scc accesses tuple elements using named indices (C L X x S) and an at operator.

Tuples: a postscript
We might define a “tuple” in APL as a vector in which we think of each item as having a name, rather than an index position.

    bob         ⍝ Tuple: name gender age
┌───┬─┬──┐
│Bob│M│39│
└───┴─┴──┘

    folk        ⍝ Vector of tuples
┌──────────┬────────────┬──────────┬────────────┬─
│┌───┬─┬──┐│┌─────┬─┬──┐│┌───┬─┬──┐│┌─────┬─┬──┐│
││Bob│M│39│││Carol│F│31│││Ted│M│31│││Alice│F│32││ ...
│└───┴─┴──┘│└─────┴─┴──┘│└───┴─┴──┘│└─────┴─┴──┘│
└──────────┴────────────┴──────────┴────────────┴─

    ↓⍉↑ folk    ⍝ Tuple of vectors
┌─────────────────────────┬────────┬───────────────┐
│┌───┬─────┬───┬─────┬─   │MFMF ...│39 31 31 32 ...│
││Bob│Carol│Ted│Alice│ ...│        │               │
│└───┴─────┴───┴─────┴─   │        │               │
└─────────────────────────┴────────┴───────────────┘

    ⍪∘↑¨ ↓⍉↑ folk   ⍝ Tuple of matrices
┌─────┬─┬──┐
│Bob  │M│39│
│Carol│F│31│
│Ted  │M│31│
│Alice│F│32│
 ...   . ..
└─────┴─┴──┘

APLers sometimes talk about “inverted files”. In this sense, a “regular” file is a vector-of-tuples and an inverted file (or more recently: “column store”) is a tuple-of-vectors (or matrices).

Type Comments

I’ve taken to commenting the closing brace of my inner dfns with a home-grown type notation pinched from the Functional Programming community:

    dref←{                  ⍝ Value for name ⍵ in dictionary ⍺ 
        names values←⍺      ⍝ dictionary pair
        (names⍳⊂⍵)⊃values   ⍝ value corresponding to name ⍵
    }                       ⍝ :: Value ← Dict ∇ Name

I keep changing my mind about whether the result type should be to the left (Value ← ...) or to the right (... → Value). The FP crowd favours → Value but I’m coming around to Value ← because:

* In contrast to (say) Haskell, APL’s function/argument sequences associate right.
* Value ← mirrors the result pattern in a tradfn header and so looks familiar.
* The type of function composition f∘g is simpler this way round.

Such comments serve as an aide-mémoire when I later come to read the code though, with some ingenuity, the notation might possibly be extended to a more formal system, which could have value to a compiler or code-checker. We would need:

Glyphs for Dyalog’s three primitive atomic data types. For no particularly good reason, I’ve been using:

# number
' character
. ref

Glyphs for a few generic (polymorphic) types. These could be just regular lower-case letters a b c … though I currently prefer greek letters:

⍺ ∊ ⍳ ⍴ ⍵ ...

Some constructors for type expressions. This is the most contentious part. For what it’s worth, I’ve been using:

::  is of type ...
∇  function
∇∇  operator
←  returns
[⍺] vector of ⍺s
{⍺} optional left argument ⍺

For example:

foo :: ⍵ ← {⍺} ∇ ⍵

implies:
- foo is an ambi-valent function whose
- result is of the same type () as its right argument and whose
- optional left argument may be of a different type ().

I can abstract/name type expressions with (capitalised) identifiers using :=. For example:

Dict   := [Name][Value]        ⍝ dictionary name and value vectors
Eval   := Expr ← Dict ∇ Expr   ⍝ expression reduction
List ⍵ := '∘' | ⍵ (List ⍵)     ⍝ recursive pairs. See
list
Name   := ⍞                    ⍝ primitive type: character vector

The type: character vector ['] is used so frequently that the three glyphs fuse into: . This means that a vector-of-character-vectors, also a common type, is [⍞].

Primitive and derived function types.
If we’re not too nit-picky and ignore issues such as single extension and rank conformability, we can give at least hints for the types of some primitive functions and operators.

 ⍳ :: # ← ⍺ ∇ ⍺              ⍝ dyadic index-of
 ⍴ :: ⍺ ← [#] ∇ ⍺            ⍝ reshape (also take, transpose, ...)

The three forms of primitive composition have interesting types:

∘ :: ⍴ ← {⍺} (⍴ ← {⍺} ∇ ⍳) ∇∇ (⍳ ← ∇ ⍵ ) ⍵     ⍝ {⍺}f∘g ⍵
:: ⍴ ←                 ⍺ ∇∇ (⍴ ← ⍺ ∇ ⍵ ) ⍵   ⍝ A∘g ⍵
:: ⍴ ←      ((⍴ ← ⍺ ∇ ⍵) ∇∇ ⍵ )⍺             ⍝ (f∘B)⍵

It follows that:

f :: ⍴ ← {⍺} ∇ ⍳
g :: ⍳ ←     ∇ ⍵
=> f∘g :: ⍴ ← {⍺} ∇ ⍵          ⍝ intermediate type ⍳ cancels out

and for trains:

A :: ⍳                  ⍝ A is an array of type ⍳
f :: ⍳ ← {⍺} ∇ ⍵
g :: ⍴ ← {⍳} ∇ ∊
h :: ∊ ← {⍺} ∇ ⍵
=> f g h :: ⍴ ← {⍺} ∇ ⍵        ⍝ fgh fork
=> A g h :: ⍴ ←     ∇ ⍵        ⍝ Agh fork
=>   g h :: ⍴ ← {⍺} ∇ ⍵        ⍝ gh atop

For a more substantial example, search function joy for :: and := in a recent download of dfns.dws.

Muse:
This notation is not yet complete or rigorous enough to be of much use to a compiler but there may already be enough to allow the writing of a dfn, which checks its own and others internal consistency. In the long term, if a notation similar to this evolved into something useful, it might be attractive to allow optional type specification as part of the function definition: without the comment symbol:

    dref←{                  ⍝ Value for name ⍵ in dictionary ⍺ 
        names values←⍺      ⍝ dictionary pair
        (names⍳⊂⍵)⊃values   ⍝ value corresponding to name ⍵
    } :: Value ← Dict ∇ Name

Response to Name Colouring for Dfns

This post contains comments to John Scholes’ post on name colouring; please continue to post any further comments with the original post.

This is a very interesting topic – as the discussion has already showed, there are many different needs. It seems to me that some of the suggestions that have been made are forms of highlighting that you would want to turn on briefly in order to search for something specific or highlight structures while editing code. For example:

  • to verify the structure (highlight the matching parenthesis or bracket, or rainbow colouring of parentheses/brackets)
  • highlight all uses of a particular name or small group of names.

I don’t think I would really want any of these enabled for any length of time; some of them can probably work very well if they are turned on and off as the cursor moves through the text (when on a parenthesis, highlight the other half of the pair, when on a name, highlight all uses of that name, etc).

Making it easier to read statements through highlighting of “kinds” feels more like something that I might well want to have enabled all the time. However, I find colouring to be quite distracting – it breaks the flow for me. I would certainly want the colours to be as calm as possible for the most common kinds, getting more exciting for the “exotic ones”. So I would suggest:

 Array
 Function
 MonOp
 DyOp

For example:

   r←(foo dop 1 2 3) mat hoo mop vec

I find that syntax colouring is much more effective in a bold font:

   r←(foo dop 1 2 3) mat hoo mop vec 

But…looking at the above, I personally find the colours to be quite distracting; they make it hard for me to read the expression as a “sentence”. How about if we experiment with emphasis instead, for example we could make functions italic, monadic operators bold, and dyadic operators both.

   r←(foo dop 1 2 3) mat hoo mop vec

This is very subjective of course, but this is much more readable to me than the coloured version.

Further comments with the original post please.