__The arithmetic and geometric means once more__

In the following, `x, y, c` are positive.

In EWD1140, I used

(0) (`x+y`)² = (`x−y`)² + 4 · `x` · `y`

to argue that

(1) `x,y` = `c, x+y−c` ,

which does not change `x+y`, increases `x `·` y` provided `c` lies between the initial values of `x` and `y`.

In EWD1171, I used (0) to argue that

(2) `x,y` := `c, x` ·` y/c` ,

which does not change `x `· `y`, decreases `x+y` provided `c` lies between the initial values of `x` and `y`.

In both cases the use of (0) came a little bit as a rabbit and the link between the condition on `c` and the decrease of the distance between `x` and `y` remained informal. Last Thursday, when I asked for an expression that contained both `x+y` and `x `· `y`, my [student] An Thai Nguyen suggested that we look at (`c−x`)·(`c−y`), and this expression indeed plays a central role in the derivations from which all rabbits have been removed.

^{*} _{*} ^{*}

We want to change `x,y` such that (i) their sum is not changed, and (ii) their product is increased. Any assignment satisfying (i) can be written like (1); in order to satisfy (ii) we now observe for any `c`

“(1) increases `x` ·` y`”

= {program semantics, (1)}

`x `· `y` < `c` ·(`x+y−c`)

= {algebra}

(`c−x`)·(`c−y`) < 0 .

We now consider the change of `x,y` such that (iii) their product is not changed, and (iv) their sum is decreased. Any assignment satisfying (iii) can be written like (2); in order to satisfy (iv) as well, we observe for any positive `c`

“(2) increases `x+y`”

= {program semantics, (2)}

`c + x `· `y/c` < `x+y`

= { `c` > 0 }

`c² + x` · `y` < `c `·(`x+y`)

= { algebra }

(`c−x`)·(`c−y`) < 0 .

So, in both cases, the completely forced calculations lead in exactly the same form to the conclusion that `c` should lie between the initial values of `x` and `y`. The secret is that Nguyen’s expression can be rewritten as

`x `·` y − c` ·(`x+y−c`)

and as

(`c² + x `· `y`) − (`c `·` x + c `·` y`) ,

i.e. the difference of two products with equal sums of their factors, and the difference of two sums with equal products of their addenda. I was surprised.

Austin, 10 February 1996

prof.dr. Edsger W.Dijkstra

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712-1188, USA