On the selection of dummies: a notational freedom

On the selection of dummies: a notational freedom

The following theorem is so well-known that it is often used subconsciously.

Theorem 0 For all $J,W,P,X$ of the appropriate types $\left( 0\right) \Rightarrow \left\lbrack {\left( 1\right) \equiv \left( 2\right) }\right\rbrack$ with

(0) $\omega \in W \equiv \left( {\underline{E}{j} : j \in J : \left\lbrack {w = {X}_{j}}\right\rbrack }\right)$ (1) $\left( {\underline{E}j : j \in J : P\left( {X,j}\right) }\right)$ (2) $\left( {{Ew} : w \in W : P.w}\right)$

Proof We observe

(2)

(1)

(End of Proof.)

$$ \begin{array}{l} = {(0) } \ (E _ {w}: (E _ {j}: j \in J: [ w = X, j ]): P _ {w}) \ = {\mathrm {t r a d i n g} \mathrm {a n d u n n e s t i n g} } \ (E w, j: j \in J \land [ w = X, j ] \land P. w) \ = {\mathrm {t r a d i n g a n d n e s t i n g} } \ (E j: j \in J: (E w: [ w = X _ {j} ]: P _ {w})) \ = {\mathrm {o n e - p o i n t r u l e} } \ \end{array} $$

The analogous theorem, obtained by replacing in (1) and (2) the existential quantifications by universal ones, follows from the above.

An advantage of (2) over (1) is that it is a little bit simpler; with more expressions of type (1) or $P(X_{j})$ written as an expression with several occurrences of $X_{j}$ , the advantage can be quite marked.

The above admits a straightforward generaliza- tion to a function $P$ defined on pairs:

$$ (3) \Rightarrow [ (4) \equiv (5) ] \quad w i t h $$

(3) $w \in W \equiv \left( {\underline{E}j : j \in J : \left\lbrack {w = \left( {{X}{j},{Y}{j}}\right) }\right\rbrack }\right)$ for all $w$ (4) $\left( {\underline{\mathrm{E}}j : j \in J : P.\left( {{X}{i},j,{Y}{j}}\right) }\right)$ (5) $\left( {{E}_{W} : w \in W : P,w}\right)$

and, comparing (4) and (5), one might think the gain greater, but this is an illusion if $P\left( {{X}{j},{Y}{j}}\right)$ is written out as an expression in ${X}{j}$ and ${Y}{j}$ . Using the selectors $\pi$ and $\mu$ ,defined by

(6) $w = \left( {{\pi }{.}w,{\mu }{.}w}\right) \;$ for all pairs $w\;\therefore$ expression (5) is then more honestly rendered (7) $\left( {E{w}_{1} : w \in W : P\left( {{\pi .w},{\mu .w}}\right) }\right)$

which is of exactly the same structure as (4):

This time, however, most of the lost advantage can be regained by increasing the number of

dummies, thanks to the following theorem.

Theorem 1 $\left\lbrack {\left( 5\right) \equiv \left( 8\right) }\right\rbrack$ with

(8) $\left( {E{p}_{q} : \left( {p,q}\right) \in W : P\left( {p,q}\right) }\right)$

Proof We observe

(8)

$$ \begin{array}{l} = {\mathrm {o n e - p o i n t r u l e} } \ (E _ {p, q}: (E _ {W}: [ (p, q) = w ]: w \in W): P _ {(p, q)}) \ = {\mathrm {t r a d i n g a n d u n n e s t i n g} } \ (E _ {p, q}, w: [ (p, q) = w ] \land w \in W \land P. (p, q)) \ = {(6) } \ (E p, q, w: [ (p, q) = (\pi . w, \mu . w) ] \land w \in W \land P. (p, q)) \ = {\mathrm {p a i r - f o r m i n g}, \mathrm {s e e N o t e b e l o w} } \ (E _ {p, q, w}: [ p = \pi , w ] \land [ q = \mu , w ] \land w \in W \land P (p, q)) \ = {\mathrm {t r a d i n g} \mathrm {a n d n e s t i n g} } \ (E w: w \in W: (E p: [ p = \pi . w ]: (E q: [ q = \mu . w ]: P (p, q))) \ = {\mathrm {o n e - p o i n t} r u l e, \mathrm {t w i c e} } \ (E w: w \in W: P. (\pi . w, \mu . w)) \ = {6 } \ (5) \ \end{array} $$

Note From pair-forming we have used the

$$ a x i o m s $$

$$ \begin{array}{l} [ (a, b) = (c, d) \equiv (a = c, b = d) ] \ [ (a, b) ] = [ a ] \wedge [ b ]. \ (E n d o f N o t e.) \ (E n d o f P r o o f.) \ \end{array} $$

Since often the range, being constant, is not

repeated during longer calculations, we should compare $(Ej: P(X_{j}, Y_{j}))$ with $(Ep,q: P(p,q))$ ; the gain can be significant.

Note that the introduction of two dummies p,q instead of the one w is quite similar to the template for formal parameters as, for instance, in SASL. The function inc that increases each element of a sequence by 1 has two alternative definitions:

$$ i n c. w = 1 + h e a d. w: i n c. (t a i l. w) $$

$$ \operatorname {i n c.} (p: q) = 1 + p: \operatorname {i n c.} q $$

The theorems are familiar, the proofs are straightforward. This note has been written to draw attention to the notational freedom they imply. Had Carel S. Schohen and I been more aware of that freedom and its significance, several of the proofs in our book would have been more crisp.

Inks Lake State Park, 6 October 1989

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