How subtypes should enter the picture

How subtypes should enter the picture

In June 1992, I completed EWD1123 "The unification of three calculi", which was written for educational purposes. It's use in the classroom, however, revealed that its elliptic introduction of the traditional boolean domain as subtype of the boolean structures was at least utterly confusing. The main purpose of this note is to remedy that situation; the fact that its title does not refer to boolean scalars and structures reflects my belief that the remedy is more generally applicable.

A proper treatment would consist of the following ingredients.

the traditional boolean domain ${\mathrm{true},\mathrm{false}} ,$ together with its operators $\equiv \Rightarrow \Leftarrow \land \lor \neg$ is assumed to be known; we call it the domain of the "boolean scalars" in order to distinguish it from the boolean structures to be introduced shortly. - the "everywhere operator", applied by surrounding the argument by a pair of square brackets, is a function from the boolean structures to the boolean scalars - on boolean structures the infix operator

$\frac{d}{dt}$ is introduced with the properties

(0) $\left\lbrack {x \doteq y}\right\rbrack \equiv x = y$

$\stackrel{\bullet}{=}$ is associative and symmetric; note that the symmetry of $\stackrel{\cdot}{=}$

$$ (x \dot {=} y) = (y \dot {=} x) $$

can be expressed -thanks to (0) and the associativity of $\overset{\cdot}{\mathrm{f}} = -$ as

$$ [ x \equiv y \equiv y \equiv x ] \quad , $$

from which it follows that $y \equiv y$ ,is (for any $y$ ) the neutral element of $p \equiv ;$ we denote it by true

$$ [ x \stackrel {\bullet} {=} t r u e \stackrel {\bullet} {=} x ] $$

is postulated to be symmetric, associative, and idempotent and to distribute over

analogously to EWD1123, $\Rightarrow ,\Leftarrow ,\rightarrow$ and the constant false are introduced, and the properties of the everywhere operator are given -i.e. some derived and some postulated such as

$$ [ t r u e ] \equiv t r u e $$

$$ [ \mathbf {f a l s e} ] \equiv \mathbf {f a l s e} $$

$$ [ x \wedge y ] \equiv [ x ] \wedge [ y ] $$

• next we observe a one-to-one correspondence between theorems about boolean scalars and boolean structures , e.g. we have in scalars

$$ x \wedge (x \vee y) \equiv x \vee f a l s e $$

as we have in structures

$$ [ x \dot {x} (x \dot {v} y) \dot {=} x \dot {v} f a s e ] \quad , $$

and this is the moment that we yield to the temptation to omit all the dots: we overload $\equiv \wedge \vee$ etc., we also make no longer a distinction between the boolean calars true and false and the constant boolean structures" true and false, which we now write as true and false respectively. By thus embedding the boolean calars in the boolean structures, we have made the former a subtype of the latter, very much in the way in which the integers can be made a subtype of the reals. Not only have we simplified our notation, we have also embellished properties, e.g. [ ] is now idempotent, and it distributes over $\wedge$ .

Austin, 4 October 1993

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