\meta{("dijkstra-comprehensions" "dijkstra and set comprehensions" ("notation") 1455720663)}

Edsger Dijkstra had notably strong opinions about a lot of things, so it
shouldn't be surprising that he had strong opinions about his mathematical
notation.
In one of his many personal notes—in particular, in
\link{https://www.cs.utexas.edu/users/EWD/transcriptions/EWD13xx/EWD1300.html|EWD 1300: The notational conventions I adopted, and why}\ref{ewd}—he
\sidenote
{
  Dijkstra wrote numerous small manuscripts by hand with a fountain
  pen, and all of these were numbered and prefixed with his initials, so
  he could refer to those manuscripts in short. He originally distributed
  them by photocopying them, but they've since been transcribed into
  digital formats.
}
goes to great length to motivate idiosyncracies in his own personal
mathematical notations, such as the use of a visible operator for
function application.\ref{fun}
\sidenote
{
  That operator was a full stop, so that \\( f.x \\) stood for \\( f(x) \\).
  He advocated combining it with the traditional operator function composition,
  so one could use \\( f \\circ g\\,.\\,x \\) to stand for \\( f(g(x)) \\).
}

One interesting feature of his notation—a feature I haven't seen discussed
quite as much—is his unusual set comprehension notation. Instead of the
more traditional

$$ \\\{\\  x^2 \\ \|\\  0 \\leq x \\leq 10 \\ \\\} $$

he would express set-building with

$$ \\langle\\  x : 0 \\leq x \\leq 10 : x^2 \\ \\rangle $$

The first field—in between the bracket and the first colon—is the
variable being quantified over; the second field is the range of
that variable; the third is the expression being used to build the
set.

Aside from the obvious change in delimiters, this notation has
the major advantage of \em{explicit binding} of the variable. Dijkstra noted
that, for example, the following use of traditional set-builder notation
has three possible interpretations, depending on whether \em{x} or
\em{n} or both have been given a value in the surrounding context:

$$ \\\{\\  x ^ n \\ \|\\  x < n \\ \\\} $$

but each of those interpretations would, by necessity, be distinct
in Dijkstra's notation\ref{not},
\sidenote
{
  The first two sets are different subsets of the third, which is the
  infinite set of all powers such that the exponent is strictly
  greater than the root.
}
as it would require you to explicitly indicate
which variables are being newly bound in building that set:

$$
  \\langle\\ x : x < n    : x ^ n \\ \\rangle \\neq
  \\langle\\ n : x < n    : x ^ n \\ \\rangle \\neq
  \\langle\\ x, n : x < n : x ^ n \\ \\rangle
$$

Dijkstra extended this notation to other operations: for example,
his notation for sums, products, maxima, and minima were \em{also}
expressed in this way, with their respective symbols placed just
inside the opening bracket:

$$
  \\langle\\,\\Sigma\\ \\ x : 0 \\leq x \\leq 10 : x^2 \\ \\rangle
  \\equiv \\sum_\{x=0\}^\{10\} x^2
$$

By using the same comprehension notation in these contexts, he
encourages a uniformity and simplicity of syntax,
but also provides two properties that traditional
notations for summation and the like do not have:
one is \em{explicit demarkation of the scope of the variable},
and another is \em{uniformity of syntax for describing the range}.
For example, there can be no ambiguity about
the scope of the summation in the following:

$$ \\langle\\,\\Sigma\\ x : 0 \\leq x \\leq 10 : x^2 + 1\\rangle \\neq
  \\langle\\,\\Sigma\\ x : 0 \\leq x \\leq 10 : x^2 \\rangle + 1
$$

This bit of traditional notation, on the other hand,
\link{http://math.stackexchange.com/questions/363453/notation-what-is-the-scope-of-a-sum|could be ambiguous}
without parenthesization:

$$ \\sum_\{x=0\}^\{10\} x^2 + 1 $$

Dijkstra decided that this notation was useful even for logical quantifiers:

$$ \\langle\\,\\exists\\ \\ x : p(x) : q(x) \\ \\rangle \\equiv \\exists x. p(x) \\wedge q(x) $$

$$ \\langle\\,\\forall\\ \\ y : p(y) : q(y) \\ \\rangle \\equiv \\forall y. p(y) \\implies q(y) $$

Logical quantifiers including a 'range' does seem a bit odd, especially
given that the interpretation of the range term is slightly different
for each operator. On the other hand, Djiktra noted that
it enables some interestingly elegant formulations.
The example Dijkstra gives is the defining property of the
supremum of a set, which in prose could be stated as, "the supremum of
a set is less than some number \\(z\\) if and only if all members of the
set are less than \\(z\\)." In his notation—using the \\(\\uparrow\\)
operator for the supremum—this would be expressed in the following way,
by distributing the \\(<\\) operator into the comprehension:

$$ \\langle\\,\\uparrow\\ i : r(i) : k(i) \\ \\rangle < z \\equiv \\langle\\  \\forall\\ i : r(i) : k(i) < z \\ \\rangle $$

A fomulation in more traditional notation is shorter, but lacks the
symmetry of Dijkstra's presentation:

$$ \\text\{sup\}(S) < z \\equiv \\forall x. x \\in S \\implies x < z $$

This notation will \em{occasionally} crop up outside of Dijkstra's own
usage—indeed, it came to my attention when some coworkers were reading
a paper that used it sans explanation—but mostly has been forgotten. It
does have some interesting advantages, but in general, I suspect it
doesn't have enough advantages to see wider adoption.