In his 1963 paper `On the design of machine independent programming languages' Dijkstra explained why he wanted to avoid using case distinctions in the design of a programming language. For example, a programming language that allows a procedure to call another procedure but not itself was unneeded sophistication according to Dijkstra. Such a restriction not only complicates the definition of the language (by introducing a case distinction), it also complicates the task of implementing the language. Details are presented in my `Dijkstra's Rallying Cry ...' article. See also my previous post on the case distinctions of Irons and Feurzeig.
Almost 20 years later, Dijkstra explained why case distinctions are preferably also avoided when reasoning mathematically. Consider the following example:
- Let each of the 15 edges of a complete 6-graph be either red or blue.
- 3 of the nodes form a "monochrome triangle" when the 3 edges connecting them are of the same color.
- Prove the existence of at least one monochrome triangle.
It is very tempting to start the proof by taking an arbitrary node and giving it a name X and to then enumerate over different cases as follows:
Among the 5 edges meeting X, one of the two colors, say red, dominates. Let XP, XQ, and XR be three red edges.
+ Case 1: Triangle PQR has a red edge, PQ say. Then triangle XPQ is monochrome red.
+ Case 2: Triangle PQR has no red edge. Then triangle PQR is monochrome blue.
Dijkstra was unsatisfied with the above proof because it destroys the intrinsic symmetries of the problem. Saying that the color red dominates over the color blue destroys the symmetry between the two colors. Furthermore, naming one node X and another node P destroys the symmetry between the nodes as well.
To exploit the aforementioned symmetries, Dijkstra introduced the following definitions:
- Call two edges of different color and having one node in common a "mixed V" meeting at that node.
- Call a triangle "bichrome" if it is not a monochrome triangle.
In this particular problem there is no need to distinguish between the nodes (and giving them a unique name). Just take an arbitrary node, notice that it has 5 edges, and hence, note that at most 2*3 = 6 mixed V's meet at that node. Continue as follows:
- Since there are 6 nodes, there are at most 6*6 = 36 mixed V's.
- Each mixed V occurs in one bichrome triangle.
- Each bichrome triangle contains two mixed V's.
- Hence, there are at most 36/2 = 18 bichrome triangles.
- The total number of distinct triangles is (6*5*4) / (3*2*1) = 20.
Hence, there are at least 20 - 18 = 2 monochrome triangles.
Dijkstra's point is that by recognizing and exploiting the symmetries of the problem at hand, the proof becomes simpler and hence easier to conduct. The word "simpler" here refers to less case distinctions (and hence to "generality"). The word "easier" refers to the virtue that the proof has less of an invitation to visualization. (My personal experience is that I have indeed had to draw much less in order to understand Dijkstra's proof compared with the first proof.)
To summarize in Dijkstra's own words:
Being of equal or of different colour are the only functions that are invariant under colour inversion --- note that, accordingly, in the last proof the colours themselves are not mentioned at all! --- ; furthermore somewhere the topology of the complete 6-graph has to be taken into account, hence the notion of a V, hence the mixed V. [...] Similarly the last proof fully maintains the symmetry between the nodes (to the extent that they too remain anonymous). Its final virtue is that it is much less of an invitation to visualization. [EWD803, p.21]