On binary operators and their derived relations

Copyright Notice

The manuscript

EWD 954A: On binary operators and their derived relations was published as

BIT 28 (1988): 378-382.

It is reproduced here by permission.

On binary operators and their derived relations

This note contains about half a dozen charming little theorems, none of which I expect to be new. It has been written because, though their proofs are very simple, the theorems are not half as well-known as I feel they deserve to be. I hope the reader will be as pleasantly surprised by the independence of the links between pairs of well-known concepts as I was when I composed this collection.

A few notational remarks first.

(i) I shall use $(\infty \bullet \Delta = \land v \Rightarrow \equiv , \therefore)$ , here listed in the order of decreasing binding power. (ii) In the proofs, the hint "Leibniz" refers to the fact that we may "substitute equals for equals", i.e.

$$ x = y \Rightarrow f (x) = f (y) $$

or,equivalently,

$$ x = y \land b (x) \Rightarrow b (y) $$

(iii) In hints, the symbol $\vDash$ is used to denote the instantiating substitution.

In terms of some infix operator $\bullet$ we define the relation $\triangleleft$ by

$\left( *\right) \;\left( {\forall x,y : x \neq y \equiv x \cdot y = x}\right)$

(Example: if we choose "greatest common divisor" for $\bullet$ , $A$ becomes "divides".) The remainder

properties of $\bullet$ and possible properties of $\Delta$

Theorem 0 (O is a left-hand zero element of $\rho$ ) $\equiv$

Proof (O is a left-hand zero element of $\bullet$ )

$$ \begin{array}{l} \equiv {\mathrm {d e f i n i t i o n o f z e r o e l e m e n t} } \ (\forall y: 0 \cdot y = 0) \ \equiv {(x) \mathrm {w i t h} x := 0 } \ (\forall y: 0 \leq y) \ \equiv {\mathrm {d e f i n i t i o n o f e x t r e m e} } \ (0 \mathrm {i s a l e f t - h a n d e x t r e m e o f} \Delta) \ \end{array} $$

(End of Proof)

Theorem 1 (I is a right-hand unit element of $\rho$ ) $=$ (I is a right-hand extreme of $\rho \Delta$ )

Proof (I is a right-hand unit element of $P$ )

(End of Proof)

$$ \begin{array}{l} \equiv \left{ \begin{array}{l} \mathrm {d e f i n i t i o n o f u n i t e l e m e n t} \end{array} \right} (\forall x: x \cdot I = x) \ \equiv {(\ast) w i t h y := I } \ (\forall x: \quad x \triangleleft I) \ \equiv {\mathrm {d e f i n i t i o n o f e x t r e m e} } \ (I \mathrm {i s} ^ {\prime} a \mathrm {r i g h t - h a n d e x t r e m e o f} A) \ \end{array} $$

Theorem 2 ( $\bullet$ is idempotent) $\equiv$ ( $\triangleleft$ is reflexive)

Proof ( $\bullet$ is idempotent)

$$ \equiv {\mathrm {d e f i n i t i o n o f i d e m p o t e n c e} } $$

$$ (\forall x: \quad x \cdot x = x) $$

$$ \equiv {(x) w i t h y := x } $$

$$ (\forall x: \quad x \triangleleft x) $$

$$ \equiv {\mathrm {d e f i n i t i o n o f r e p l e x i v i l y} } $$

(4 is reflexive)

(End of Proof)

EWD954a - 2

Theorem 3. ( $\bullet$ is associative) $\Rightarrow$ ( $\Delta$ is transitive)

Proof By definition of associativity

$$ (\bullet \mathrm {i s a s s o c i a t i v e}) \equiv (\forall x, y, z: x \bullet (y \bullet z) = (x \bullet y) \bullet z); $$

by definition of transitivity

$$ (\Delta \mathrm {i s t r a n s i t i v e}) \equiv (\forall x, y, z: x \Delta y \land y \Delta z \Rightarrow x \Delta z). $$

We shall establish the consequent, using the antecedent. To this end, we observe for any $x,y,z$

$$ \begin{array}{l} \equiv {(\ast); (\ast) \mathrm {w i t h} x, y := y, z } \ x \cdot y = x, \wedge y \cdot z = y \ \Rightarrow \quad {\mathrm {L e i b n i z} } \ x \cdot y = x \wedge x \cdot (y \cdot z) = x \ \equiv {\bullet \text {i s a s s o c i a t i v e} } \ x \cdot y = x \wedge (x \cdot y) \cdot z = x \ \Rightarrow {\text {L e i b n i z} } \ x \cdot z = x \ \equiv {(*) \mathrm {w i t h} y := 2 } \ x \Delta z \ \end{array} $$

(End of Proof)

Theorem 4 (is symmetric) $\Rightarrow$ (4 is antisymmetric).

Proof By definition of symmetry

$$ (\bullet \mathrm {i s s y m m e t r i c}) \equiv (\forall x, y: x \cdot y = y \cdot x) ; $$

by definition of antisymmetry

$$ (\Delta \mathrm {i s a n t i s y m m e t r i c}) \equiv (\forall x, y: x \Delta y \land y \Delta x \Rightarrow x = y). $$

We shall establish the consequent, using the antecedent. To this end, we observe for any $x,y$

$$ \begin{array}{l} = {(\ast); (\ast) \mathrm {w i t h} x, y := y, x } \ = \left{ \begin{array}{l l} x \cdot y = x & \wedge y \cdot x = y \ \bullet \mathrm {i s s y m m e t r i c} \end{array} \right} \ x \cdot y = x \wedge x \cdot y = y \ \Rightarrow {\mathrm {L e i b n i z} } \ \end{array} $$

$$ x = y $$

$$ (E n d o f P r o o p) $$

For a unary prefix operator $\infty$ we have

Theorem 5 ( $\infty$ distributes over $\bullet$ ) $\Rightarrow$ ( $\infty$ is monotonic with respect to $\Delta$ ).

Proof By definition of distributivity

$$ (\infty \mathrm {d i s t i b u t e s o v e r} \bullet) \equiv (\forall x, y: \infty (x \cdot y) = \infty x \cdot \infty y); $$

by definition of monotonicity

$$ \begin{array}{l} (\infty \mathrm {i s m o n o t o n i c w i t h r e s p e c t t o} \Delta) \equiv \ (\forall x, y: \quad x \triangle y \Rightarrow \infty \times \triangle \infty y) \ \end{array} $$

We shall establish the consequent, using the antecedent. To this end we observe for any $x,y$

$$ \begin{array}{l} = \left{(\ast) \mathrm {w i t h} x, y := \infty , \infty \right} \ \infty x \cdot \infty y = \infty x \ = {\infty d i s t r i b u t e s o v e r \cdot } \ \infty (x \cdot y) = \infty x \ \Leftrightarrow {L e i b n i z } \ = \begin{array}{l} x \cdot y = x \ {\star) } \end{array} \ x \triangle y \ \end{array} $$

(End of Proof.)

Theorem 6 (is idempotent, associative, and symmetric) $\Rightarrow$ (is monotonic with respect to $A$ )

Proof By definition of monotonicity

( $\bullet$ is monotonic with respect to $a$ ) $\equiv$

$$ (\forall x, y, z: x \Delta y \Rightarrow x \cdot 2 \Delta y \cdot 2 \wedge 2 \cdot x \Delta 2 \cdot y) $$

Using the antecedent, we observe to begin with

$$ \begin{array}{l} u \cdot (x \cdot y) \ = {\bullet \mathrm {i s a s s o c i a t i v e} } \ (u \cdot x) \cdot y \ = {\bullet \mathrm {i s} ^ {\mathrm {j d e m p o t e n t}} } \ ((u \cdot u) \cdot x) \cdot y \ = {\bullet \mathrm {i s a s s o c i a t i v e} } \ (u \cdot (u \cdot x)) \cdot y \ = {\bullet \mathrm {i s} \mathrm {s y m m e t r i c} } \ ((u \cdot x) \cdot u) \cdot y \ = {\bullet \mathrm {i s a s s o c i a t i v e} } \ (u \cdot x) \cdot (u \cdot y) \ \end{array} $$

i.e. the prefix operator u● distributes over ●, and from Theorem 5 it now follows that ● yields an expression that is monotonic with respect to $\Delta$ in its right-hand operand; symmetry extends monotonicity to its left-hand operand.

(End of Proof.)

I composed this collection of little theorems when I noticed myself appealing to some of them with increasing frequency and therefore felt that the time had come to explore this area more explicitly. The experience profoundly mixed my feelings. On

the one hand I was, for instance, tickled by the observation that the notion of monotonicity with respect to a relation is totally independent of the question of whether that relation is transitive or not. On the other hand it made me annoyed with the mathematical culture in which I had grown up, but in which the teaching of (admittedly beautiful) but also) elaborate theories had totally suppressed the teaching of simple relationships between basic concepts as collected in the above. May the above collection spare the next generation a similar disappointment.

Austin, 26 April 1987

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