gdritter repos when-computer / a4ee348
Revised and published Dijkstra notation post Getty Ritter 8 years ago
2 changed file(s) with 54 addition(s) and 27 deletion(s). Collapse all Expand all
11 \meta{("dijkstra-comprehensions" "dijkstra and set comprehensions" ("notation"))}
22
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.
46 In one of his many personal notes—in particular, in
57 \link{https://www.cs.utexas.edu/users/EWD/transcriptions/EWD13xx/EWD1300.html|EWD 1300: The notational conventions I adopted, and why}\ref{ewd}—he
68 \sidenote
810 Dijkstra wrote numerous small manuscripts by hand with a fountain
911 pen, and all of these were numbered and prefixed with his initials, so
1012 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.
1215 }
1316 goes to great length to motivate idiosyncracies in his own personal
1417 mathematical notations, such as the use of a visible operator for
2124 }
2225
2326 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
2529
2630 $$ \\\{\\ x^2 \\ \|\\ 0 \\leq x \\leq 10 \\ \\\} $$
2731
3135
3236 The first field—in between the bracket and the first colon—is the
3337 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
3539 set.
3640
3741 Aside from the obvious change in delimiters, this notation has
3842 the major advantage of \em{explicit binding} of the variable. Dijkstra noted
3943 that, for example, the following use of traditional set-builder notation
4044 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:
4346
4447 $$ \\\{\\ x ^ n \\ \|\\ x < n \\ \\\} $$
4548
5255 greater than the root.
5356 }
5457 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:
5759
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 $$
5965
6066 Dijkstra extended this notation to other operations: for example,
6167 his notation for sums, products, maxima, and minima were \em{also}
6268 expressed in this way, with their respective symbols placed just
6369 inside the opening bracket:
6470
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 $$
6675
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:
7396
7497 $$ \\langle\\,\\exists\\ \\ x : p(x) : q(x) \\ \\rangle \\equiv \\exists x. p(x) \\wedge q(x) $$
7598
7699 $$ \\langle\\,\\forall\\ \\ y : p(y) : q(y) \\ \\rangle \\equiv \\forall y. p(y) \\implies q(y) $$
77100
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
81106 supremum of a set, which in prose could be stated as, "the supremum of
82107 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:
84111
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 $$
86113
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:
88116
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 $$
90118
91119 This notation will \em{occasionally} crop up outside of Dijkstra's own
92120 usage—indeed, it came to my attention when some coworkers were reading
93121 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.
1 ../drafts/dijkstra-notation.telml