Idempotence and reflexivity; associativity and transitivity; distribution and monotonicity

Idempotence and reflexivity; associativity and

We consider an infix operator $\bullet$ and a relational operator $\Leftrightarrow$ , connected by

(0) $\underset{\sim }{A}x.y\therefore x \cdot y = x \equiv x < y$ )

(Here the order of decreasing binding power is $\left. {\cdot , < \text{and} = ,\land \text{and}v, \equiv \cdot }\right)$

Lemma 0 " $\bullet$ is idempotent" $\equiv$ " $\Leftarrow$ is reflexive"

Proof. $\left( {A \times : x \cdot x = x}\right) \equiv \left( {A \times : x < x}\right)$

(End of Proof.)

$$ \begin{array}{l} \Leftarrow {\mathrm {p r e d i c a t e c a l c u l u s} } \ (A ^ {\prime} x: \quad x \cdot x = x \equiv x < x) \ = { \begin{array}{l} {(0) \mathrm {w i t h} y := x} \ {\mathrm {t r u e}} \end{array} } \ \end{array} $$

Lemma 1 "is associative" $\Rightarrow$ "is transitive".

Proof We observe for any $x,y$ ,and $z$

$$ \begin{array}{l} x < y \land y < z \ = {(0); (0) \mathrm {w i t h} x, y := y, z } \ x \cdot y = x \wedge y \cdot z = y \ \Rightarrow {\mathrm {L e i b n i z} } \ x \cdot y = x \wedge x \cdot (y \cdot z) = x \ = {\cdot \mathrm {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 {\mathrm {L e i b o n i z} } \ x \cdot z = x \ = {(0) \mathrm {w i t h} y := z } \ x < z \ \end{array} $$

(End of Proof.)

We now introduce a unary prefix operator $\infty$ , which is given the highest binding power.

Lemma 2 " $\infty$ distributes over $\cdot \Rightarrow$ " $\infty$ is monotonic with respect to $<$ "

Proof We observe for any $x$ and $y$

$$ \begin{array}{l} \cos x < \cos y \ = {(0) \mathrm {w i t h} x, y := \cos x, \cos y } \ \cos x \cdot \cos y = \cos x \ = {\infty d i s t r i b u t e s o v e r \cdot } \ \cos (x \cdot y) = \cos x \ \Leftarrow {\mathrm {L e i b n i z} } \ x \cdot y = x \ = {(0) } \ x < y \ \end{array} $$

(End of Proof.)

Lemma 3 " $\bullet$ is idempotent,associative,and symmetric" $\Rightarrow$ " $\bullet$ is monotonic with respect to $\leq$ ".

Proof We observe for any $u,x$ ,and $y$

$$ \begin{array}{l} u \cdot (x \cdot y) \ = {\cdot i s a s s o c i a t i v e } \ (u \cdot x) \cdot y \ = {\cdot i s i d e m p o t e n t } \ ((u \cdot u) \cdot x) \cdot y \ = {\cdot i s a s s o c i a t i v e } \ (u \cdot (u \cdot x)) \cdot y \ = {\cdot i s s y m m e t r i c } \ ((u \cdot x) \cdot u) \cdot y \ = {\cdot \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 Lemma 2 it follows that $\cdot$ yields an

EWD954-2

expression that is monotonic in its right-hand operand; symmetry extends monotonicity to its left-hand operand.

(End of Proof.)

Lemma 4 "i is a right-hand unit element of $P \cdot \forall$ " $\equiv$ " i is a right-hand extreme of $P <$ " $\downarrow$

Proof. $\left( {A \times : x \cdot 1 = x}\right) \equiv \left( {A \times : x < 1}\right)$

$$ \begin{array}{l} \Leftarrow {p r e d i c a t e c a l c u l u s } \ (A \times :: x \cdot 1 = x \equiv x < 1) \ = {(0) \mathrm {w i t h} y := 1 } \ t r u e \ \end{array} $$

(End of Proof)

Lemma 5 "0 is a left-hand zero element of $\rho$ ." $\Rightarrow$ "0 is a left-hand extreme of $\phi <$ "

Proof. $\left( {\underline{A}y\because 0 \cdot y = 0}\right) \equiv \left( {\underline{A}y\because 0 < y}\right)$

$$ \begin{array}{l} \Leftrightarrow {\mathrm {p r e d i c a t e c a l c u l u s} } \ (\frac {A}{B} y: 0. 5 y = 0 \equiv 0 < y) \ = {(0) \mathrm {w i t h} x := 0 } \ \mathbf {f r u e} \ \end{array} $$

(End of Proof.)

One might wonder why a grown-up scientist should waste his time by writing down such trivialities. Well, consider them "for the record". The sad truth is that I was not aware of all these lemmata in their full generality. (I had not realized before that the notion of monotonicity is also meaningful with respect to a relation that is not transitive. Did I know that the connective in lemmata 4 and 5 was an equivalence, rather than an implication? I don't think so.)

This is the umpteenth occasion for my being rather dissatised with my mathematical education. I consider these little lemmata very beautiful and think every mathematician should know them. Why weren't they included? Because their proofs are too simple? But that only adds to their charm!

Here is another one I just thought of:

[\text{Lem}6 \quad \left( {x < y \land y < x \Rightarrow x = y}\right) \Leftarrow ]

Proof We observe for any $x$ and $y$

$$ x < y \land y < x $$

$$ = {(0); (0) \mathrm {w i t h} x, y := y, x } $$

$$ x \cdot y = x \wedge y \cdot x = y $$

$$ = {\cdot i s s y m m e t r i c } $$

$$ x \cdot y = x, \wedge x \cdot y = y $$

$$ \Rightarrow {\mathrm {l e i b n i z} } $$

$$ x = y $$

(End of Proof)

(The property of $\leq$ proved in the above theorem is,curiously enough,known as "antisymmetry".)

Austin, 9 February 1986

prof. dr. Edsger W. Dgkstra

Department of Computer Sciences

The University of Texas at Austin

Austin, TX 78712 - 1188

United States of America