A formula is worth a thousand pictures (dedicated to Charles Antony Richard Hoare)

A formula is worth a thousand pictures

by

Edsger W. Dgkstra

Dedicated to

Charles Antony Richard Hoare

A formula is worth a thousand pictures

This note describes an experiment in calculational geometry, in particular in using the triangle calculus, which was hoped to be an effective weapon against case analysis. In this experiment, it was. The effective and reliable exploitation of symmetry presented another challenge; we believe to have met it successfully. Eventually the experiment produced a surprising theorem we had never seen before.

In either picture we see 7 points so situated that they give rise to 6 collinear triples. They have been partitioned into what we call the 4 "primary" points $a,b,c,d$ and the 3 secondary" points $p,q,r$ ; while each primary point occurs in 3 collinear triples, each secondary point occurs in only 2 of them. Please note that we have named the points consistently in the sense that in either picture $p$ corresponds

to the pairing (ad) (bc), q to (ab) (cd) and r. to (ac) (bd) . For the following theorem we want a proof that is independent of how the 7 points are otherwise situated in the plane.

Theorem The secondary points are not collinear if no triple of primary points is collinear.

If so happens that for any 3 points $x, y, z$ ( $x, y, z$ are collinear) $\equiv$ (0 = area of $\triangle xyz$ ), so the whole theorem can be formulated in terms of areas being 0 or not. The purpose of this note is to explore whether we can prove the theorem elegantly not in terms of the boolean function "collinear" but in terms of the real function "area". (Manipulating areas allows us to take more of the structure of the Euclidean plane into account than the notion of collinearity would have done; moreover, signed areas have been shown to be a valuable tool in eliminating case analyses generated by the distinction in side/outside.)

We shall use $a,b,c,d,h,k,p,q,r,x,y,z$ to identify variables of type point and ${\Delta xyz}$ to denote in formulae the area of triangle xyz.

(We know that we can only do this as long as we avoid multiletter names.) For a while we put the theorem aside and focus our attention on what seem the relevant properties of areas of triangles. The creation of a full-blown axiom system falling outside the scope of this paper, we'll just postulate some simple properties that seem useful. We distinguish three types of properties.

Our first postulate has to do with the signs of areas. It states that for all $x,y,z$

(0) ${\Delta xyz} = {\Delta y}{z}{1} \land {\Delta xyz} = - {\Delta z}{y}{1}$

i.e., subjecting the arguments to an odd permutation changes the sign of the area. This is not a purely notational question, it has a mathematical consequence, viz.

$x = y \Rightarrow {\Delta xyz} = 0$

i.e., the area of a triangle with two coinciding vertices is zero.

Note We have considered to formulate this consequence as

$$ x = y \vee y = z \vee z = x \Rightarrow \Delta x y z = 0 $$

but have decided against this elaborate formula-

tion, hoping that the reader will supply the appeals to (o). This is a decision very similar to the one we took in the predicate calculus of not spending separate steps on symmetry and associativity of the logical operators. (End of Note)

For the next postulate - the additive one we shall give three different formulations, which thanks to (0) are completely equivalent. They differ, however, in their "symbol dynamics" and in the symmetries they suggest.

The first formulation is completely symmetric in the four points: for all points $x,y,z,h$

$\left( 2\right) {\Delta xyz} + {\Delta hzy} + {\Delta zhx} + {\Delta yxh} = 0$

(For any pair of triples in the above, the shared points occur in the same two positions, but interchanged.)

In the next formulation of the same postulate, one point -here $h$ - plays a special role:

${\Delta xyz} = {\Delta h{yz}} + {\Delta xh}z + {\Delta xyz}$

The symbol dynamics" here are that the triples of the right-hand side are formed by replacing

a fourth point.

In the final formulation, the four points are separated into two pairs, viz. $(x,y)$ versus $(h,k)$ :

$\left( {2}^{n}\right) \cdot \Delta = {h}^{2} + {\Delta h} \cdot \Delta = - {h}^{2} + {\Delta h} \cdot \Delta$

Please note how the triples have been taken from the cycle (xhyk)

An immediate consequence of the additive postulate (2) - most easily derived from (2")- is lemma

(3) ${\Delta xyz} = 0 \Rightarrow {\Delta xhy} + {\Delta yhz} = {\Delta xhz}$

This is an important lemma because it provides a way of exploiting the collinearity of $x,y,z$ and then equates an expression containing $y$ to an expression without

Our final postulate is a multiplicative one. With a high infix dot denoting multiplication we could postulate that for all $h,k,x,y,z$ :

$$ \begin{array}{r l} {\Delta x y z} & {= 0 \Rightarrow} \ {(\Delta h x y) \cdot (\Delta k x z)} & {= (\Delta k x y) \cdot (\Delta h x z)} \end{array} $$

It's charm is that it does not matter at all. if some of the points coincide, but we found it

painful to use: with 5 points the symbol dynamics really becomes complicated. In the current con- text we found it more convenient to use in- instead that for all $x,y,z$

$\Rightarrow \Delta {xyz} = 0 \land x \neq 2$ (4)

$$ \langle \exists \lambda : \langle \forall h: \Delta h x y = \lambda \cdot \Delta h x z \rangle \rangle $$

This is better disentangled than the previous 5 - point postulate because it makes clear that there is a relevant quantity - viz. the $\lambda$ that does the job - that only depends on the triple $x,y,z\ldots$

Note We did not name the function whose value equals that λ , nor did we define it by means of an operator, say

$$ \lambda = x y: x z $$

because in this investigation we are not in the business of introducing partial functions. (End of Note)

The time has come to try whether we can now prove our original theorem, which we rephrase more formally as follows.

Theorem We are given 4 primary points $a,b,c,d$ and 3 secondary points, satisfying

(5) (i) ${\Delta apd} = 0$

(ii) ${\Delta bpc} = 0$

(6) (i) ${\Delta aqb} = 0$

(ii) ${\Delta c} = 0$

(7) (i) $\bigtriangleup {arc} = 0$

(ii) ${\Delta brd} = 0$

(8) (i) $\triangle bcd \neq 0$

(ii) ${\Delta cda} \neq 0$

(iii) ${\Delta dab} \neq 0$

$\left( {iv}\right) {\Delta abc} \neq 0$

$\therefore \Delta = {PQ}$

(End of Theorem)

We intend to prove the theorem in two steps. In the first step we hope to express $\triangle pqr$ in terms of $\triangle bcd$ , $\triangle cda$ , $\triangle dab$ , $\triangle abc$ , and in the second step we hope to show that thanks to (8) this expression differs from 0.

Before embarking in more detail on this project, we observe that in order to apply (4) we have to know that two points are distinct. Thanks to (the contrapositive of) (1), the conclusion that two points differ can be drawn from the fact that a triangle area differs from 0 . Drawing this latter conclusion from (8), we conclude

(9) the primary points $a,b,c,d$ are all distinct.

We have to relate the "secondary triangle" $\Delta p q r$ to the 4 "primary triangles" mentioned in (8), and we propose to do so in 3 steps, in each step reducing the number of secondary points by 1.

The first transition, i.e., to triples with 2. condary points, is easy: applying (2") with xyz := pqra , we get

(10) ${\Delta pqr} = {\Delta aqr} + {\Delta par} + {\Delta pqa}\;$ ,

the choice of "a" having been arbitrary: any of

For the remaining transitions we now proceed for the time being with 1 of the new triangles in (10), say $\Delta aqr$ , and now consider the transition to triples with 1 secondary point only. The pair $aq$ occurs in (6,i), the pair $ar$ in (7,i); arbitrarily we choose to concentrate on the former. Because on account of (6,i) and (9) we have

$$ \Delta a g b = 0 \land a \neq b $$

we can conclude from (4) with ${xyz} \mathrel{\text{:=}} {aqb}$ the existence of a $\lambda$ such that

$$ \langle \forall h: \Delta h a q = \lambda \cdot \Delta h a b \rangle $$

Instantiating this in turn with $h := r$ , $h := c$ ,

$h \mathrel{\text{:=}} d$ ,we conclude that there is a $\lambda$ satisfying

(11) (i) ${\Delta r}{a}{q} = \lambda \cdot {\Delta r}{a}{b}$ (ii) ${\Delta caq} = \lambda \cdot {\Delta cab}\;$ i.e., ${\Delta qac} = - \lambda \cdot {\Delta abc}$ (iii) ${\Delta daq} = \lambda \cdot {\Delta dab}$

(The other possible instantiations of $h$ give results that are known or -in the case $h := p$ not helpful because we are trying to get rid of secondary points.) From the last 2 equalities we can eliminate $q$ -the only secondary point occurring in them! - by observing

$$ \begin{array}{l} \lambda \cdot (\Delta d a b - \Delta a b c) \ = {(1 1, i i) a n d (1 1, i i) } \ \Delta d a q + \Delta q a c \ = {(3) \mathrm {w i t h} x y z h := d q c a \mathrm {a n d} (6, 1 1) } \ \Delta d a c \ = \left{ \begin{array}{l} (0) \end{array} \right} \ \Delta c d a \ \end{array} $$

Because -see (8)- $\Delta cda\neq 0$ , the above tells us that $\Delta dab - \Delta abc$ differs from O and that we may divide by it. Eliminating with the above $\lambda$ from (11,i) yields

(12) ${\Delta rag} = \left( {{\Delta rab} \cdot \left( {{\Delta cda}}\right) /\left( {{\Delta c}{lab} - {\Delta abc}}\right) }\right)$ ,

which leaves us with the obligation of eliminating $r$ (the last secondary point at the right-hand side) from ${\Delta rab}.$

For the last transition, the occurrence of r in $\Delta$ rab points us to (7), and arbitrarily we select(7,i)to begin with.Because of(7,i)and (9)we have

$$ \Delta \operatorname {a r c} = 0 \land a \neq c $$

and can conclude from (4) with ${xyz} \mathrel{\text{:=}}$ arc the existence of a $\mu$ such that

$$ \langle \forall h: \Delta h a r = \mu \cdot \Delta h a c \rangle $$

Instantiating this with $h = b$ and $h = d$ - the

(13) (i) ${\Delta bar} = \mu \cdot {\Delta bac}\;$ i.e., ${\Delta rab} = \mu \cdot {\Delta abc}$ (ii) ${\Delta dar} = {\mu }^{ \circ }{\Delta dac}\;i.e.,\;{\Delta dar} = {\mu }^{ \circ }{\Delta cda}$

Now we observe

$$ \begin{array}{l} \mu^ {\bullet} (\Delta c d a + \Delta a b c) \ = {1 3 } \ \Delta d a r + \Delta r a b \ = {(3) \mathrm {w i t h} x y z h := d r b a \mathrm {a n d} (7, i i) } \ \Delta d a b \ \end{array} $$

Again, because of (8), ${\Delta dab} \neq 0$ and the above tells us that ${\Delta cda} + {\Delta abc}$ differs from 0 ; solving the above for $\mu$ and substituting this solution in(13,i) yields

(14) ${\Delta rab} = \left( {{\Delta abc} \cdot \left( {{\Delta dab}}\right) /\left( {{\Delta cda} + {\Delta abc}}\right) }\right.$

and now elimination of 3ab from (12) and

$$ (1 5) \quad \Delta a q r = \frac {(\Delta a b c) \cdot (\Delta d a b) \cdot (\Delta c d a)}{(\Delta c d a + \Delta a b c) \cdot (\Delta d a b - \Delta a b c)} $$

For the computation - see (10) of $\Delta$ par and $\Delta$ pqa we would like to reuse the above calculation of $\Delta$ aqr, but before we are going to do so, we introduce 4 abbreviations, viz.

$$ \begin{array}{l} (1 6) \quad A = \triangle d c b \quad B = \triangle c d a \ C = \Delta b a d D = \Delta a b c \ \end{array} $$

which allow us to shorten (15) to

$$ (1 7) \quad \Delta a q r = \frac {D \cdot C \cdot B}{(B + D) \cdot (C + D)} $$

To reuse the computation of $\Delta aq$ for that of $\Delta$ par,we look for a substitution

(i) transforms ${\Delta agr}$ into(-) ${\Delta par}$ ,and (ii) leaves the antecedent of the theorem, i.e., (s) through (8) unchanged.

We can achieve (i) by the interchange $p,q = q,p$ and then (ii) by extending it into the substitu-

tion $p,q,b,d \mathrel{\text{:=}} q,p,d,b$ (thus interchanging (5) and (6)). The invariance of (16) is obtained by the simultaneous substitution

$$ A, B, C, D := - A, - D, - C, - B $$

The substitution transforms $\Delta$ aqr into $-\Delta$ par and thus we derive from (17)

$$ (8) \quad \Delta p a r = \frac {B \cdot C \cdot D}{(D + B) \cdot (C + B)} $$

To compute $\Delta {pqa}$ from (17) we similarly perform the substitution $p,r,c,d \mathrel{\text{:=}} r,p,d,c$ which in the theorem only interchanges (5) and (7), and transforms $\Delta$ aqr into $- {\Delta pqa}$ , while (16) is maintained by the simultaneous substitution

$$ A, B, C, D := - A, - B, - D, - C $$

Thus we derive from (17)

$$ (1 9) \quad \Delta p q a = \frac {C \cdot D \cdot B}{(B + C) \cdot (D + C)} $$

$$ \mathrm {C o l l e c t i n g} \quad (1 0), (1 7), (1 8), (1 9) \quad \mathrm {w e g e t} $$

$$ \Delta p q r = \frac {B \cdot C \cdot D \cdot ((B + C) + (D + C) + (B + D))}{(B + D) \cdot (C + D) \cdot (B + C)} $$

from (2') and (16) we have

$A + B + C + D = 0$

and we can for instance simplify the result to

(21) $\bigtriangleup {p q r} = \frac{2 \cdot A \cdot B \cdot C \cdot D}{\left( {A + B}\right) \cdot \left( {A + C}\right) \cdot \left( {A + D}\right) }$

(Note that thanks to (20) the denominator of (21) is symmetric in $A,B,C,D$ as well.)

With (8) and (16)

Epiogue

When, in the early 80s, our calculational argu- ments began to take the shape now known as "the Fegen format", in which an expression is essentially subjected to a sequence of value-preserving or monotonic transformations, all sorts of people (in particular people with prior exposure to logic) said "But you cannot do that! In proofs of any sophistication the logical dependency graph is much more compi- plicated than a linear arrangement, etc. etc." But, not liking logical spaghetti -and still remembering the goto -controversy! - we ignored these protests and became happier and happier

with our calculational style.

But as soon as I turned to formal geometry, I observed that logical spaghetti returned in my own work! In those days, my efforts were heavily influenced by David Hilbert's work in that area, and since that time I harbour the lurking suspicion that the tradition of logical spaghetti could very well have been started by the historical accident that, in his other- wise pioneering work on the axiomatization of geometry, Hilbert stayed too close to Euclid to reap the full benefit of calculation. The issue is of some significance, because if my suspicion is correct, formal logic's bad name isn't really deserved, but mainly caused by the accident that, for once, Hilbert has not been sufficiently radical. Hence my interest in geometrical experiments that, though totally elementary, depart from Euclid's style.

The example has been chosen because I ex- pected that it would not be completely trivial: if this theorem were false, there would be a counterexample to Sylvester's conjecture that for a finite set of distinct, noncollinear points in the Euclidean plane, there exists a straight line through exactly two of them. Furthermore

I expected an interesting competition between the 4 - fold symmetry among the primary points and the 3 - fold symmetry among the secondary points.

What have we learned from this exercise?

The concept of the signed area has (again) proved its value in avoiding the case distinctions that pictorial arguments tend to engender. (In deriving (10) we gave a special role to the primary point "a", formally an irrelevant choice, pictorially a bothering question.)

The technique of introducing a neutral terminology -here $a,b,c,d,p,q,r^{\prime}$ and listing separately -here (5), (6), (7) - the relevant relations between the named entities has (again) been convenient. This technique was flexible enough for the painless accommodation of the two competing symmetries. (The technique is very similar to what I am used to in lattice calculus, viz. that of naming extreme solutions and listing their defining properties instead of using the special symbols $\mu$ and $\nu$ .)

• The introduction of abbreviations, though from some mathematical point of view perhaps an almost empty gesture, can be of great practical significance. (I am thinking about the introduction of $A,B,C,D$ ,without which the

the reuses of the earlier calculation of (15) would have been most painful).

The question what to name can be of great importance. The reader may have wondered about the choices made in (16): why not just name the $\Delta$ -expressions mentioned in (8)? But with that latter choice we would have had $A + C = B + D$ instead of the symmetric (20), and the denominator of (21) would have been ugly.

• Exploitation of symmetry - often done in a hand-waving manner can be captured crisply by invariances under substitutions.

Acknowledgement

I thank the Tuesday Afternoon Clubs of Austin and Eindhoven for their perceptive critical comments.

Nuenen, 23 June 1999

pror. dr Edsger W. Dgksta

Department of Computer Sciences The University of Texas at Austin

Austin, TX 78712 - 1188

USA