A manuscript for the Coahuila student chapter of the ACM

A manuscript for the Coahuila student chapter of the ACM

In this note we shall show a solution to a simple problem, and shall use the solution to illustrate quite a few points. Here is the problem.

About a positive number of couples, two things are given

(0) the maximum age among the men equals the maximum age among the women.

Note We did not say "The oldest man has the same age as the oldest woman" because "the oldest man" is an expression that excludes the case that there are two or more men of maximum age. (End of Note)

(1) If two couples engage in a wife swap, the minimum age in the one new combination equals the minimum age in the other new combination.

Note We did not say "... the minimum age in the one new combination equals that in the other". Such a formulation would have been clear enough in conversation, where in case of doubt the other party can ask for clarification, but in writing it should be avoided. Notice

that we can not conclude from (1) that there are two or more couples; the following argument is, indeed, valid in the case of a single couple as well. (End of Note.)

We are now requested to show

(2) In each couple, husband and wife are of the same age.

We begin by formalizing the data and the demonstrandum. We do so for various reasons. One reason is to remove the last possible traces of ambiguity; another reason is to make data and demonstrandum amenable to symbolic manipulation; a final reason is to reduce them to their bare essentials by removal of the irrelevant noise.

Remark A major aspect of all intellectual activity is the selection or creation of the appropriate "language" to talk and reason about the topic at hand. The transition from "natural language" to "formal language" can be viewed as a reduction of the bandwidth and constitutes a major simplification. (End of Remark.)

Let us start with the formalization of the demonstrandum (2); it is the simplest of the three because equality is the only relation on ages that it uses.

Let variable $x$ (and later also $y$ ) range over the couples; the number of couples being positive, $x$ has a finite, nonempty range. We now introduce two functions $f \& m$ (of type: couple → age) with the following meaning:

${f}_{.x} =$ the age of the wife in couple $x$

Note Here we have used the convention of indicating function application explicitly by an infix dot (which is given the highest syntactic binding power). This dot was introduced after the realization that the introduction of invisible operators has very unfortunate consequences, such as ambiguity - for instance, what about $\sin (s + i + n)$ ? An advantage of the application dot is that the role of parentheses can now be confined to syntactic grouping, as in "sin. $(\alpha + \beta)$ ", and is no longer part of function notation, as in the former "sin $(\varphi)$ ". (End of Note.)

That husband and wife in couple x are of the same age can now be expressed by

$$ m. x = f. x $$

but (2) states that such equality holds for all couples. The notational device to render this "for all" is called "universal quantification".

Using it, we now render (2) formally as

(3) $\left\langle {\forall x\therefore m.x = f \cdot x}\right\rangle$ ,

usually read as: "for all $x$ , $m \times$ equals $f{x}^{\prime \prime }$ .

Remark In the quantified expression (3),

variable $x$ is called "the dummy". It is

local to the expression, and its scope is

delineated by the pair of angular brackets.

(Syntactically, dummies in quantified expressions

are strictly analogous to local variables in

block-structured programming languages.)

Omitting these scope delineators is penny-wise

and pound-foolish. (End of Remark.)

In (3), we did allow ourselves a short-hand.

The space between the two colons is reserved

for an explicit description of the range of the

dummy; had we wanted to be more explicit,

we could have written

$$ \langle \forall x: x \in \mathrm {c o u p l e s}: m. x = f. x \rangle $$

but, as we shall see, such explicit range

descriiption in each quanhfied expression

would make what follows very repetitious

and unnecessarily lengthy: since all dummies

in this note range over couples , it suffices

to declare so once (as we have done).

Note We should strive for brevity, but without

Introducing ambiguity or committing the sin

of omission. (End of Note.)

Let us now turn to datum (1); it equates the minimum of one pair with the minimum of another pair, so we need a notation for the minimum of a pair. I propose a downward arrow "↓" as infix operator, i.e. we shall denote the minimum of A and B by "A↓B". It has all the good properties, such as

• $\downarrow$ is idempotent,viz. $A \downarrow A = A$ $\therefore {AD} = {2AE}$ . $\therefore {A}{B} \cap {A}{C} = P$

Remark Some people argue -and not without good reason- that the introduction of infix operators of all sorts was a mistake: infix operators create the need for parentheses. I must confess that I am so used to infix operators (like $+, *, \wedge, =, \equiv$ ) that I think I am old enough to stick to them, but I never introduce a new infix operator without considerable hesitation: for one thing, one has to assign a proper syntactic binding power to it. Infix notation is very tempting for an associative operator: instead of won- dering where to put 'the semantically irrelevant parentheses, one just omits them and writes $A \downarrow B \downarrow C$ . (End of Remark.)

It is unlikely that idempotence, symmetry, and associativity are the only properties of the

minimum operator we need: they fail to distinguish it from all other idempotent, symmetric, and associative operators (such as , for instance, the Greatest Common Divisor). We therefore record its fundamental property

$A \leq B \equiv A = {A\downarrow B}$

Aside As an example of the use of (4) we shall prove $P \downarrow Q \leq P$ . To this end we observe

$$ \begin{array}{l} P \downarrow Q \leq P \ = {(4) \mathrm {w i t h} A, B := P \downarrow Q, P } \ P \downarrow Q = (P \downarrow Q) \downarrow P \ = {\downarrow \mathrm {i s a s s o c i a t i v e a n d s y m m e t r i c} } \ P \downarrow Q = (P \downarrow P) \downarrow Q \ = {\downarrow i s i d e m p o t e n t } \ P \downarrow Q = P \downarrow Q \ = {e q u a l i t y } \ t r u e \ \end{array} $$

(End of A side.)

We now return to (1). Consider two couples x and y . After the wife swap, the minimum age in the new combination con- sisting of the man from x and the woman From y is m.x $\downarrow$ f.y ; the minimum age in the other new combination is p.x $\downarrow$ m.y . And they are equal. Since this holds for any pair of couples, the formal translation of (1) is (5) $\left\langle {\forall x,y : x \neq y : m \cdot x \downarrow {f}_{y} = f \cdot x \downarrow m \cdot y}\right\rangle$

The restriction $x \neq y$ in the range reflects that the natural-language concept "wife swap" is (presumably) only defined between two distinct couples $x$ and $y$ . However, because of the symmetry of $\downarrow$ we can assert

$$ \langle \forall x, y: x = y: m. x \downarrow f. y = f. x \downarrow m. y \rangle , $$

which in combination with (5) yields

(6) $\langle \forall x,y\therefore m \cdot x \downarrow {f}_{y} = f \cdot x \downarrow m \cdot y\rangle$

Remark The derivation of (6) from the previous two formulae is standard predicate calculus; it relies on $x \neq y \lor x = y \equiv$ true. (End of Remark.)

Let us now turn to the formalization of (0). While (1) is about a minimum, which we denoted using a " $\downarrow$ ", (0) is about a maximum, which suggests the use of "↑". But we don't need the maximum of a pair, but the maximum of a whole set -at least a singleton set! - of men and a similar set of women. We need -as in the translation of (2)- a quantification, but this time what could be called a "maximal quantification", and render (0) by

(7) $\left\langle {{\widehat{y}}{1} : m \cdot y}\right\rangle = \left\langle {{\widehat{y}}{2} : p \cdot y}\right\rangle$

where the left-hand side stands for the maximum value that my may reach when y is allowed to

range over the couples. The right-hand side is similarly defined. Note that maximal quantification is well-defined for nonempty, finite range.

Similarly to $P \downarrow Q \leq P$ -as proved in the. Aside-we have for function $p - p = m$ or $p = f - \langle \forall x : p.x \leq \langle {T}_{y} : p.y\rangle \rangle$

In combination with (4) this yields

(8) $\left\langle {\forall x : p.x = p.x \downarrow \left\langle {t}_{y} : p.y\right\rangle \rangle }\right.$

Finally we mention the important property that $\downarrow$ distributes over $\uparrow$ -and the other way round, but we don't need that here -, i.e. for any $q$

(9) $q \downarrow \left\langle {1,y\therefore p \cdot y}\right\rangle = \left\langle {1,y\therefore q \downarrow p \cdot y}\right\rangle$

Note This is closely related to, for instance, the distribution of disjunctio (v", pronounced "or") over universal quantification: for predicate Q and predicate-valued function P we have

$$ Q \vee \langle \forall y: P _ {y} \rangle \equiv \langle \forall y: Q \vee P _ {y} \rangle $$

(End of Note.)

Now we are ready to prove (3), i.e $\left{ {\forall x : m \cdot x = p \cdot x}\right}$ . To this end we observe for arbitrary couple $x$

$$ \begin{array}{l} m. x = f. x \ = {(8) \mathrm {w i t h} p := m \mathrm {a n d} p := p _ {\mathrm {p}} \mathrm {r e s p e c t i v e l y} } \ m \cdot x \downarrow \langle \uparrow y: m \cdot y ^ {\prime} \rangle = p \cdot x \downarrow \langle \uparrow y: f \cdot y \rangle \ = {(\tau) } \ m. x \downarrow \langle \uparrow y: p. y \rangle = f. x \downarrow \langle \uparrow y: m. y \rangle \ = {(9) \mathrm {w i t h} g, p := m. x, f \mathrm {a n d} q, p := p. x, m } \ \langle \uparrow y: m. x \downarrow f. y \rangle = \langle \uparrow y: f. x \downarrow m. y \rangle \ = {() } \ \begin{array}{l} \text {t r u e} \ \hline \end{array} , \ \end{array} $$

and this concludes the proof.

Two comments are in order. In this presentation we have prepared the first step by mentioning (8) first. In practice, everybody familiar with the " $\downarrow$ calculus" knows that formula. But, please, note that anyone that does not know (8) can conclude that something like (8) is needed: our data (6) and (7) are in terms of the infix $\downarrow$ and the quantified $\uparrow$ so these have to be introduced. The next step is purely opportunistic: it exploits (7) without destroying the symmetry. In the next step we use the distribution law any practitioner knows, but, again, note that from the fact that we still have to exploit (6), we can conclude that something like (9) is needed.

Secondly we would like to stress that in the above 4-step calculation we did not

make a single case distinction. The verbal arguments I have seen have to distinguish between a single couple and more couples, and tend to require special precaution to cater for multiple couples of maximum age.

The fact that, in the formal argument, the need for the case analysis does not arise contains an important message for computing science. We all know the programmer's standard excuse after an error in his program showed up: "Oh, but that was a very special case!". Instead of trying to cope in our reasoning with possibly exploding case analyses, we had better learn how to avoid case analysis.

Austin, 29 November 1991

prof. dr. Edsger W. Dgkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188 USA

Sent to: Octavio Juarez Espinosa Gabriel Valerio 1134 Saitillo, Coahuila Mexico CP 25000

Univesidad Autonoma de Coahuila