| 1 |
\meta{("dijkstra-comprehensions" "dijkstra and set comprehensions" ("notation"))}
|
| 2 |
|
| 3 |
Edsger Dijkstra was \em{really} opinionated about his notation.
|
| 4 |
In one of his many personal notes—in particular, in
|
| 5 |
\link{https://www.cs.utexas.edu/users/EWD/transcriptions/EWD13xx/EWD1300.html|EWD 1300: The notational conventions I adopted, and why}\ref{ewd}—he
|
| 6 |
\sidenote
|
| 7 |
{
|
| 8 |
Dijkstra wrote numerous small manuscripts by hand with a fountain
|
| 9 |
pen, and all of these were numbered and prefixed with his initials, so
|
| 10 |
he could refer to those manuscripts in short. He originally distributed
|
| 11 |
them by photocopying them, but they've since been widely transcribed.
|
| 12 |
}
|
| 13 |
goes to great length to motivate idiosyncracies in his own personal
|
| 14 |
mathematical notations, such as the use of a visible operator for
|
| 15 |
function application.\ref{fun}
|
| 16 |
\sidenote
|
| 17 |
{
|
| 18 |
That operator was a full stop, so that \\( f.x \\) stood for \\( f(x) \\).
|
| 19 |
He advocated combining it with the traditional operator function composition,
|
| 20 |
so one could use \\( f \\circ g\\,.\\,x \\) to stand for \\( f(g(x)) \\).
|
| 21 |
}
|
| 22 |
|
| 23 |
One interesting feature of his notation—a feature I haven't seen discussed
|
| 24 |
as much—is his unusual set comprehension notation. Instead of the more traditional
|
| 25 |
|
| 26 |
$$ \\\{\\ x^2 \\ \|\\ 0 \\leq x \\leq 10 \\ \\\} $$
|
| 27 |
|
| 28 |
he would express set-building with
|
| 29 |
|
| 30 |
$$ \\langle\\ x : 0 \\leq x \\leq 10 : x^2 \\ \\rangle $$
|
| 31 |
|
| 32 |
The first field—in between the bracket and the first colon—is the
|
| 33 |
variable being quantified over; the second field is the range of
|
| 34 |
the variable; the third is the expression being used to build the
|
| 35 |
set.
|
| 36 |
|
| 37 |
Aside from the obvious change in delimiters, this notation has
|
| 38 |
the major advantage of \em{explicit binding} of the variable. Dijkstra noted
|
| 39 |
that, for example, the following use of traditional set-builder notation
|
| 40 |
has three possible interpretations, depending on whether \em{x} or
|
| 41 |
\em{n} or both have been given a value in the surrounding context or
|
| 42 |
not:
|
| 43 |
|
| 44 |
$$ \\\{\\ x ^ n \\ \|\\ x < n \\ \\\} $$
|
| 45 |
|
| 46 |
but each of those interpretations would, by necessity, be distinct
|
| 47 |
in Dijkstra's notation\ref{not},
|
| 48 |
\sidenote
|
| 49 |
{
|
| 50 |
The first two sets are different subsets of the third, which is the
|
| 51 |
infinite set of all powers such that the exponent is strictly
|
| 52 |
greater than the root.
|
| 53 |
}
|
| 54 |
as it would require you to explicitly indicate
|
| 55 |
which variables are being newly bound in building that set, and
|
| 56 |
therefore explicitly omit any other variables:
|
| 57 |
|
| 58 |
$$ \\langle\\ x : x < n : x ^ n \\ \\rangle \\neq \\langle\\ n : x < n : x ^ n \\ \\rangle \\neq \\langle\\ x, n : x < n : x ^ n \\ \\rangle $$
|
| 59 |
|
| 60 |
Dijkstra extended this notation to other operations: for example,
|
| 61 |
his notation for sums, products, maxima, and minima were \em{also}
|
| 62 |
expressed in this way, with their respective symbols placed just
|
| 63 |
inside the opening bracket:
|
| 64 |
|
| 65 |
$$ \\langle\\,\\Sigma\\ \\ x : 0 \\leq x \\leq 10 : x^2 \\ \\rangle \\equiv \\sum_\{x=0\}^\{10\} x^2 $$
|
| 66 |
|
| 67 |
By applying the same notation here, he brings in a uniformity of
|
| 68 |
expression, and also provides two properties that traditional
|
| 69 |
notation for summation and the like do not have: one is \em{explicit demarkation
|
| 70 |
of the scope of the variable}, and another is \em{uniformity of
|
| 71 |
syntax for describing the range}. Dijkstra decided that this
|
| 72 |
notation was useful even for logical quantifiers:
|
| 73 |
|
| 74 |
$$ \\langle\\,\\exists\\ \\ x : p(x) : q(x) \\ \\rangle \\equiv \\exists x. p(x) \\wedge q(x) $$
|
| 75 |
|
| 76 |
$$ \\langle\\,\\forall\\ \\ y : p(y) : q(y) \\ \\rangle \\equiv \\forall y. p(y) \\implies q(y) $$
|
| 77 |
|
| 78 |
Including the same notation for expressing the 'range' seems a bit odd,
|
| 79 |
but it does enable some rather elegant formulations of certain
|
| 80 |
equations. The example Dijkstra gives is the defining property of the
|
| 81 |
supremum of a set, which in prose could be stated as, "the supremum of
|
| 82 |
a set is less than some number \\(z\\) if and only if all members of the
|
| 83 |
set are less than \\(z\\)." In his notation, this would be expressed as
|
| 84 |
|
| 85 |
$$ \\langle\\,\\uparrow\\ i : r(i) : k(i) \\ \\rangle \\sqsubseteq z \\equiv \\langle\\ \\forall\\ i : r(i) : k(i) \\sqsubseteq z \\ \\rangle $$
|
| 86 |
|
| 87 |
In a more traditional notation, this would look more like
|
| 88 |
|
| 89 |
$$ \\text\{sup\} \\\{\\ k(i) \\ \|\\ r(i) \\ \\\} \\sqsubseteq z \\equiv \\forall i. r(i) \\Rightarrow (k(i) \\sqsubseteq z)$$
|
| 90 |
|
| 91 |
This notation will \em{occasionally} crop up outside of Dijkstra's own
|
| 92 |
usage—indeed, it came to my attention when some coworkers were reading
|
| 93 |
a paper that used it sans explanation—but mostly has been forgotten. It
|
| 94 |
does have some interesting advantages, and it's not \em{quite} as obtuse
|
| 95 |
and opaque as some other niche notations like
|
| 96 |
\link{http://blog.plover.com/math/PM.html|Peano's use of dots in lieu of parentheses}.
|
| 97 |
Still, I suspect that it will probably remain a curiosity.
|