The everywhere operator once more

The everywhere operator once more.

Let $X, Y, Z$ be boolean functions defined on some space; let $M, N$ be integer functions defined on that same space; let that same space be the understood range of the dummy $s$ . Then, for instance, the equality of the functions $X$ and $Y$ would be expressed by

$$ (\mathrm {H} s:: \quad X. s \equiv Y. s) \quad ; $$

similarly, $M$ and $N$ being the same function would be expressed by

$$ (\underline {{A}} s: \quad M. s = N. s) $$

M being everywhere less than N would be given by (As: M.s < N.s)

Besides functions denoted by identifiers, we allow functions denoted by expressions; when applied (to $s$ ), these function expressions are enclosed by parentheses. They are defined as one would expect, e.g.

$$ \begin{array}{l} (A s: \quad (\neg X). s \equiv \neg X. s) \ (\overline {{A}} s: \quad (X \vee Y). s \equiv X. s \vee Y. s) \ (\mathrm {A s}: \quad (X \wedge Y). s \equiv X. s \wedge Y. s) \ (\mathrm {A s}: \quad (X \Leftarrow Y). s \equiv X. s \Leftarrow Y. s) \ (A s: \quad (X \equiv Y). s \equiv X. s \equiv Y. s) \ (\bar {A} s: \quad (M + N). s = M. s + N. s) \ \end{array} $$

$$ (\mathrm {A s}: (M < N). s \equiv M. s < N. s) $$

Note that we also allow constants in function expressions, e.g.

$$ \begin{array}{l} (H) s: ((\mathrm {t r u e}). s \equiv \mathrm {t r u e}) \ (\underline {{\underline {{A}}}} s: \quad (X \equiv f a l s e). s \equiv X. s \equiv f a l s e) \ (\underline {{A}} s: \quad (N + 2). s = N. s + 2) \ \end{array} $$

Function expressions enable us to reduce the number of function applications, e.g. instead of rendering the symmetry of the conjunction by

$$ (\mathrm {A s}: X. s \wedge Y. s \equiv Y. s \wedge X. s) $$

we can write

$$ (\underline {{A}} s: (X \wedge Y). s \equiv (Y \wedge X). s) $$

or even

$$ (*) \quad (\underline {{A}} s: \quad (X \wedge Y \equiv Y \wedge X). s) $$

With a sufficiently rich repertoire of function

Similarly, $M$ and $N$ being the same function would be expressed by $\left\lbrack {M = N}\right\rbrack$ .

Notice that in the transition from the universal quantification to the square brackets, all that has been lost is the irrelevant name of the dummy.

Above, we have introduced the square brackets as an abbreviation, as a "mere" notational device. Having done so, however, we have achieved more: the dummy s being no longer visible, we don't need to remember any more that once it was there! We don't need to remember that $X,Y,$ Z,M,N started as functions: we can treat them as variables of new types. The only thing we need to remember is that the type of $X,Y,Z$ has boolean connotations - in the sense that true and false are possible values and the logical operators are defined on them - and that the type of M,N has integer connotations - in the sense that 0,1, and, say, 7 are possi- sible values and that the arithmetic operations are defined on them.

For lack of a better name, we called them boolean and integer "structures" respectively. (Had I have to name them now, I might have chosen "profiles".) More important than their names is that we can postulate the algebraic properties of the operators introduced for them.

In this exercise, the boolean structures and the square brackets play a fundamental role. The square brackets now denote an operator - called "the everywhere operator" of the type

$$ b o o l e a n s t r u c t u r e s \rightarrow {\mathrm {t r u e}, f a l s e } $$

or, calling true and false the two "boolean scalars," of the type

$$ b o o l e a n s t r u c t u r e s \rightarrow b o o l e a n s c a l a r s $$

The fundamental properties of the every where

(i) true and false are the 2 solutions of the equation

$$ X: \quad [ X ] = X $$

(ii) $\left\lbrack {\left( {\underline{A}X\vdots X}\right) }\right\rbrack \equiv \left( {\underline{A}X\vdots \left\lbrack X\right\rbrack }\right)$

from (i) we deduce

• $\left\lbrack {\left\lbrack X\right\rbrack \equiv }\right\rbrack \left\lbrack X\right\rbrack$ ,i.e. the every where operator is idempotent; because false is disjunctio's unit element and true its zero element

$$ [ Y \vee [ X ] ] \equiv [ Y ] \vee [ X ] \quad , $$

and similarity

$$ [ [ X ] \Rightarrow Y ] \equiv [ X ] \Rightarrow [ Y ] $$

With trading and the above we derive from (ii)

$\left\lbrack {\left( {\underline{A}X}\right) : \left\lbrack {r,X}\right\rbrack : X}\right\rbrack = \left( {\underline{A}X;\left\lbrack {r,X}\right\rbrack ;\left\lbrack X\right\rbrack }\right)$ ,

where we have written [r. x] with a pair of square brackets to express explicitly that the range of $P$ is given by an expression of type boolean scalar. A special instance is

$\left\lbrack {X \land Y}\right\rbrack \equiv \left\lbrack X\right\rbrack \land \left\lbrack Y\right\rbrack$

An immediate consequence is the monotonicity of the everywhere operator, i.e.

$$ [ X \Rightarrow Y ] \Rightarrow ([ X ] \Rightarrow [ Y ]) $$

A major advantage of the above algebraic introduction of boolean structures is that it creates a universe of discourse more abstract than set theory. The comparison with set theory is sug- gested because, in the functional view with which we started, X and Y can be viewed as the characteristic functions of subsets -to function X corresponds the set ${s\mid X.s} -$ ; function XY is then the characteristic function of their intersection,etc.. Since sets are defined as composed of elements, it is hard to talk about sets without mentioning the elements as well. With the transition from the boolean functions to the boolean structures the dummy s disappeared from our formulae, but not only

that: we have got rid of the underlying space with its individual points!

We can introduce the points of the space into the world of the boolean structures by postulating the existence of special boolean structures called "point predicates". (As derivations of characteristic functions they would be derived from the characteristic functions of the singleton sets.) With $x$ ranging over the point predicates, the notion of point predicates can now be captured by postulating

(iii) $\left\lbrack {\left( {E \times : x}\right) }\right\rbrack$ $\left\lbrack {x \Rightarrow {7x}}\right\rbrack \equiv \neg \left\lbrack {x \Rightarrow X}\right\rbrack$ for all $x,x$

(Set-theoretically,(iii) states that the union of all singleton sets is the universe, and (iv) that, given a set and a singleton set, the latter is a subset of either the former or the former's complement.)

The great thing about (iii) and (iv) is that we can abstain from postulating them, thereby creating a formal system that is intrinsically simpler to work with. (For a discussion of the same simplification in connection with the relational calculus, see [0].)

The usual name for boolean structures is

"predicates"; this the name that will be used in the sequel.

Leibniz's Principle states that a function applied to equal arguments yields equal values, formally usually expressed as

$$ p = q \Rightarrow f. p = f. q $$

or,equivalently,

$$ p = q \land f _ {\cdot} p = k \equiv p = q \land f _ {\cdot} q = k $$

Because the arguments $p$ and $q$ could be structures - in which case $p = q$ would be a predicate and not necessarily a boolean scalar- and because $f$ could be structure-valued, we reformulate Leibniz's Principle as

$$ (v) \qquad [ p = q ] \Rightarrow [ f, p = f, q ] $$

or, equivalently,

$$ [ p = q \land f. p = k ] \equiv [ p = q \land f. q = k ]. $$

Formula (v) holds for all p,q,p of the ap. appropriate types. There are functions, known as punctual functions, for which the stronger (vi) holds:

$$ (v i) \quad [ p = q \Rightarrow f. p = f. q ] $$

or,equivalently,

$$ [ p = q \land f. p = k \equiv p = q \land f. q = k ] \quad . $$

The logical connectives -i.e. $\equiv \land v \Rightarrow \Leftarrow \neg$ - are all punctual in all their arguments, e.g.

$$ [ (p \equiv q) \Rightarrow (p \wedge r \equiv q \wedge r) ] \quad , $$

this in contrast to the relational operators:

for composition we have only general Leibniz(v)

$$ [ p \equiv q ] \Rightarrow [ p; r \equiv q; r ] \quad . $$

Remark Matrix calculus provides an environment in which punctuation can be identified. Negation is punctual $- {\left( -A\right) }{ij} = - \left( {A}{ij}\right)$ ,the transpose $- {\left( {A}^{T}\right) }{ij} = {A}{ji}$ - is not. The matrix sum is punctual, the product is not. This is not too surprising, since the relational calculus can be modelled as a boolean matrix calculus with for (addition,multiplication,matrix multiplication) the triple (disjunction, conjunction, composition). (End of Remark.)

There is a wide-spread inclination to render the application of the everywhere operator by special infix operators , e.g.

$$ X = Y \qquad \mathrm {f o r} \qquad [ X \equiv Y ] $$

$$ X \leq Y \quad \mathrm {f o r} \quad [ X \Rightarrow Y ] \quad , $$

but this way of eliminating square brackets leads to notational conflicts. Performing the elimination on the Golden Rule

$$ [ X \wedge Y \equiv X \equiv Y \equiv X \vee Y ] $$

destroys the associativity and leads - see [1] - to 5 different "theorems" of set theory. A 6th form would be

$$ X \wedge Y \equiv X \equiv Y \equiv X \vee Y = = t r u e, $$

a device that can be used to render for instance

$$ [ X \vee \neg X ] b y X \vee \neg X = t r u e, $$

but the device is not recommended. It would lead to rendering (ii) by

$$ ((A X:: X) = = \mathrm {t r u e}) \equiv (A X:: X = = \mathrm {t r u e}), $$

but this has now become a very special property

$$ ((A X:: X) = = Y) \mathrm {a n d} (A X:: X = = Y) $$

are unrelated.

Besides generating the need for more and more symbols, the convention of special infix operators generates the need for more theorems. In the case of the $\leq$ introduced above we would need

$$ \begin{array}{l} (E X: X) \leq Y \equiv (A X: X \leq Y) \ X \leq (\underline {{A}} Y: Y) \equiv (\underline {{A}} Y: X \leq Y) \ \end{array} $$

The great notational advantage of the square brackets is that, once they have been accepted,

they free us from the dilemma whether to introduce a special operator like $= \text{or} \leq$ . Giving us all the combinatorial freedom we need, the square brackets solve these problems once and for all. [0] Alfred Tarski, On the Calculus of Relations, Journal of Symbolic Logic, 6 (3); pp. 73-89; 1941 [1] Edsger W. Dgksra & Carel S. Scholten, Predicate Calculus and Program Semantics, Springer-Verlag, p. 60; 1990

Austin, 26 November 1990

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