| 1 | 1 |
\meta{("dijkstra-comprehensions" "dijkstra and set comprehensions" ("notation"))}
|
| 2 | 2 |
|
| 3 | |
Edsger Dijkstra was \em{really} opinionated about his notation.
|
| 3 |
Edsger Dijkstra had notably strong opinions about a lot of things, so it
|
| 4 |
shouldn't be surprising that he had strong opinions about his mathematical
|
| 5 |
notation.
|
| 4 | 6 |
In one of his many personal notes—in particular, in
|
| 5 | 7 |
\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 | 8 |
\sidenote
|
|
| 8 | 10 |
Dijkstra wrote numerous small manuscripts by hand with a fountain
|
| 9 | 11 |
pen, and all of these were numbered and prefixed with his initials, so
|
| 10 | 12 |
he could refer to those manuscripts in short. He originally distributed
|
| 11 | |
them by photocopying them, but they've since been widely transcribed.
|
| 13 |
them by photocopying them, but they've since been transcribed into
|
| 14 |
digital formats.
|
| 12 | 15 |
}
|
| 13 | 16 |
goes to great length to motivate idiosyncracies in his own personal
|
| 14 | 17 |
mathematical notations, such as the use of a visible operator for
|
|
| 21 | 24 |
}
|
| 22 | 25 |
|
| 23 | 26 |
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
|
| 27 |
quite as much—is his unusual set comprehension notation. Instead of the
|
| 28 |
more traditional
|
| 25 | 29 |
|
| 26 | 30 |
$$ \\\{\\ x^2 \\ \|\\ 0 \\leq x \\leq 10 \\ \\\} $$
|
| 27 | 31 |
|
|
| 31 | 35 |
|
| 32 | 36 |
The first field—in between the bracket and the first colon—is the
|
| 33 | 37 |
variable being quantified over; the second field is the range of
|
| 34 | |
the variable; the third is the expression being used to build the
|
| 38 |
that variable; the third is the expression being used to build the
|
| 35 | 39 |
set.
|
| 36 | 40 |
|
| 37 | 41 |
Aside from the obvious change in delimiters, this notation has
|
| 38 | 42 |
the major advantage of \em{explicit binding} of the variable. Dijkstra noted
|
| 39 | 43 |
that, for example, the following use of traditional set-builder notation
|
| 40 | 44 |
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:
|
| 45 |
\em{n} or both have been given a value in the surrounding context:
|
| 43 | 46 |
|
| 44 | 47 |
$$ \\\{\\ x ^ n \\ \|\\ x < n \\ \\\} $$
|
| 45 | 48 |
|
|
| 52 | 55 |
greater than the root.
|
| 53 | 56 |
}
|
| 54 | 57 |
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:
|
| 58 |
which variables are being newly bound in building that set:
|
| 57 | 59 |
|
| 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 $$
|
| 60 |
$$
|
| 61 |
\\langle\\ x : x < n : x ^ n \\ \\rangle \\neq
|
| 62 |
\\langle\\ n : x < n : x ^ n \\ \\rangle \\neq
|
| 63 |
\\langle\\ x, n : x < n : x ^ n \\ \\rangle
|
| 64 |
$$
|
| 59 | 65 |
|
| 60 | 66 |
Dijkstra extended this notation to other operations: for example,
|
| 61 | 67 |
his notation for sums, products, maxima, and minima were \em{also}
|
| 62 | 68 |
expressed in this way, with their respective symbols placed just
|
| 63 | 69 |
inside the opening bracket:
|
| 64 | 70 |
|
| 65 | |
$$ \\langle\\,\\Sigma\\ \\ x : 0 \\leq x \\leq 10 : x^2 \\ \\rangle \\equiv \\sum_\{x=0\}^\{10\} x^2 $$
|
| 71 |
$$
|
| 72 |
\\langle\\,\\Sigma\\ \\ x : 0 \\leq x \\leq 10 : x^2 \\ \\rangle
|
| 73 |
\\equiv \\sum_\{x=0\}^\{10\} x^2
|
| 74 |
$$
|
| 66 | 75 |
|
| 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:
|
| 76 |
By using the same comprehension notation in these contexts, he
|
| 77 |
encourages a uniformity and simplicity of syntax,
|
| 78 |
but also provides two properties that traditional
|
| 79 |
notations for summation and the like do not have:
|
| 80 |
one is \em{explicit demarkation of the scope of the variable},
|
| 81 |
and another is \em{uniformity of syntax for describing the range}.
|
| 82 |
For example, there can be no ambiguity about
|
| 83 |
the scope of the summation in the following:
|
| 84 |
|
| 85 |
$$ \\langle\\,\\Sigma\\ x : 0 \\leq x \\leq 10 : x^2 + 1\\rangle \\neq
|
| 86 |
\\langle\\,\\Sigma\\ x : 0 \\leq x \\leq 10 : x^2 \\rangle + 1
|
| 87 |
$$
|
| 88 |
|
| 89 |
This bit of traditional notation, on the other hand,
|
| 90 |
\link{http://math.stackexchange.com/questions/363453/notation-what-is-the-scope-of-a-sum|could be ambiguous}
|
| 91 |
without parenthesization:
|
| 92 |
|
| 93 |
$$ \\sum_\{x=0\}^\{10\} x^2 + 1 $$
|
| 94 |
|
| 95 |
Dijkstra decided that this notation was useful even for logical quantifiers:
|
| 73 | 96 |
|
| 74 | 97 |
$$ \\langle\\,\\exists\\ \\ x : p(x) : q(x) \\ \\rangle \\equiv \\exists x. p(x) \\wedge q(x) $$
|
| 75 | 98 |
|
| 76 | 99 |
$$ \\langle\\,\\forall\\ \\ y : p(y) : q(y) \\ \\rangle \\equiv \\forall y. p(y) \\implies q(y) $$
|
| 77 | 100 |
|
| 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
|
| 101 |
Logical quantifiers including a 'range' does seem a bit odd, especially
|
| 102 |
given that the interpretation of the range term is slightly different
|
| 103 |
for each operator. On the other hand, Djiktra noted that
|
| 104 |
it enables some interestingly elegant formulations.
|
| 105 |
The example Dijkstra gives is the defining property of the
|
| 81 | 106 |
supremum of a set, which in prose could be stated as, "the supremum of
|
| 82 | 107 |
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
|
| 108 |
set are less than \\(z\\)." In his notation—using the \\(\\uparrow\\)
|
| 109 |
operator for the supremum—this would be expressed in the following way,
|
| 110 |
by distributing the \\(<\\) operator into the comprehension:
|
| 84 | 111 |
|
| 85 | |
$$ \\langle\\,\\uparrow\\ i : r(i) : k(i) \\ \\rangle \\sqsubseteq z \\equiv \\langle\\ \\forall\\ i : r(i) : k(i) \\sqsubseteq z \\ \\rangle $$
|
| 112 |
$$ \\langle\\,\\uparrow\\ i : r(i) : k(i) \\ \\rangle < z \\equiv \\langle\\ \\forall\\ i : r(i) : k(i) < z \\ \\rangle $$
|
| 86 | 113 |
|
| 87 | |
In a more traditional notation, this would look more like
|
| 114 |
A fomulation in more traditional notation is shorter, but lacks the
|
| 115 |
symmetry of Dijkstra's presentation:
|
| 88 | 116 |
|
| 89 | |
$$ \\text\{sup\} \\\{\\ k(i) \\ \|\\ r(i) \\ \\\} \\sqsubseteq z \\equiv \\forall i. r(i) \\Rightarrow (k(i) \\sqsubseteq z)$$
|
| 117 |
$$ \\text\{sup\}(S) < z \\equiv \\forall x. x \\in S \\implies x < z $$
|
| 90 | 118 |
|
| 91 | 119 |
This notation will \em{occasionally} crop up outside of Dijkstra's own
|
| 92 | 120 |
usage—indeed, it came to my attention when some coworkers were reading
|
| 93 | 121 |
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.
|
| 122 |
does have some interesting advantages, but in general, I suspect it
|
| 123 |
doesn't have enough advantages to see wider adoption.
|