Lifting, orders, and the Galois connection

Lifting, orders, and the Galois connection

Let $\leq$ be the infix symbol for a relation on some domain $D$ .

Let $f, g$ be functions of type $D \leftarrow E$ . i.e., "to $D$ from $E$ " for some domain $E$ .

Denoting, as usual, function application by left associative infix dot, we can define in terms of $\leq$ a relation $\xi$ on domain $D \leftarrow E$ by defining for all $f,g$

$f \leq g \equiv \langle \forall e : f.e \leq g.e\rangle$

Note that with $=$ for both $\leq$ and $\leq$ , (0) boils down to the standard definition for equality of functions.

In the jargon, is obtained "by lifting $\leq$ "; hence the first word in the title of this note. lifting is a notational device for reducing the number of explicit quantifi-cations to be written down.

"Relation $\leq$ is reflexive" means that for all $x,y$ $x = y \Rightarrow x \leq y \land y \leq x\;$

we have the theorem

$$ (\leq i s r e f l e x i v e) \equiv (\leq i s r e f l e x i v e) $$

"Relation $\leq$ is antisymmetric " means that for all $x,y$

$$ x \leq y \land y \leq x \Rightarrow x = y $$

We have the theorem

$$ (\leq i s a n t i s y m m e t r i c) \equiv (\stackrel {\circ} {=} i s a n h i s y m m e t r i c). $$

"Relation $\leq$ is transitive" means that for all

$$ x \leq y \land y \leq z \Rightarrow x \leq z $$

We have the theorem

$$ (\leq i s t r a n s i t i v e) \equiv (\leq i s t r a n s i t i v e) $$

The proofs of these three little theorems are left to the reader. A relation that is reflexive, antisymmetric, and transitive is called a partial order; hence $\leq$ and $\leq$ are both or neither partial orders.

"Relation $\leq$ is total" means that for all

$$ x \leq y \vee y \leq x $$

A partial order that is total is called a total order. Note that $\lesseqqgtr$ being total in general does not imply that $\lesseqqgtr$ is total as well, an observation that probably explains why total orders are less popular than the more general orders.

In the rest of this note we omit the no-tational distinction between $\leq$ and $\lesseqqgtr$ ; also the latter will be denoted by $\leq$ . This notational change does not introduce any ambiguity: $\leq$ 's original domain $D \times D$ is extended with the distinct $(D \leftarrow E) \times (D \leftarrow E)$ .

We shall also take the liberty of not mentioning ranges and domains of functions, this in the understanding that in the case of functional composition the types always match

As pointed out, a special case of (0) is

(1) $p = g \equiv \left\langle {\forall e : f.e = g.e}\right\rangle$

which should be compared with Leibniz's Principle

$x = y \equiv \left\langle {\forall f : f \cdot x = f \cdot y}\right\rangle$

The symmetry between (1) and (2) is seductive, but misleading because there is such a thing as the identity function. -used to prove $x = y \Leftrightarrow \left\langle {Yf\therefore f{x}^{\prime } = {f}_{y}}\right\rangle -$ and no such thing as an identity argument.

The symmetry can, however, be restored by confining ourselves to functions and

replacing functional application with func- tiona composition, which we denote by an infix o. This yields, analogous to

(1) and (2) respectively, $f = g \equiv \left\langle {\forall e : {f}{0}e = {g}{0}e}\right\rangle$ $x = y \equiv \left\langle {\forall f : {f}^{0}x = {f}^{0}y}\right\rangle$

Note that the identity function is both left- and right-identity element of $\theta$ .

Analogous to (0) we have

$f \leq g \equiv \left\langle {\forall e : {f}{0}e \leq {g}{0}e}\right\rangle$

and for reasons of symmetry we would of course love to have as well $x \leq y \equiv \left\langle {\forall f : {f}{0}x \leq {f}{0}y}\right\rangle$ ,

but this only holds provided the last universal quantificatlon is restricted to monotonic f. So we save the situation by brute, but also elegant force: in the rest of this note all functions are monotonic. Note

• a constant function is monotonic
• the identity function is monotonic
• the composition of monotonic functions is monotonic.

Note that as a consequence of (5) & (6):

$f \leq g \land x \leq y \Rightarrow {f}^{ \circ }x \leq {g}^{ \circ }y$

that is: the restriction to monotonic functions turns composition into a monotonic operator. (Who would prefer to write (7)'s antecedent as ${\left( {f}^{\prime },x\right) }_{s} \leq \left( {g,y}\right)$ ,is free to do so .)

For monotonic functions $f$ and $g$ ,(8), (9), and (10) are equivalent; they are three different ways of saying that the pair $\left( {{f}_{2}g}\right)$ forms what is known as a Galois connection".

(8a) ${f}_{0}g \leq {id}$

and

(8 b) ${id} \leq g{of}^{2}$

(9) ${f}_{0}x \leq y \equiv x \leq {g}^{ \circ }y\;$ for all $x,y$ $\left( {10}\right) y \leq x \circ f \equiv {y}^{ \circ }g \leq x\;f\left( 0\right) =$

We prove their equivalence by mutual implications. Implications (9) $\Rightarrow$ (8a) and (9) $\Rightarrow$ (8b) are proved by the instantiations $x,y \mathrel{\text{:=}} g,{id}$ and $x,y \mathrel{\text{:=}} {id},f$ ; the proofs use that is reflexive

For the proof of (8) $\Rightarrow$ (9) we present a ping-pong argument. For ping

we observe for any $x,y$

$$ \begin{array}{l} = \begin{array}{l} f _ {0} x \leq y \ {(8) } \end{array} \ \Rightarrow \quad \begin{array}{l} i d \leq g _ {0} f \wedge f _ {0} x \leq y \ {\circ m o n o t o n i c, t w i c e } \end{array} \ \Rightarrow \quad x \leq g _ {\mathrm {o}} f _ {\mathrm {o}} x \wedge g _ {\mathrm {o}} f _ {\mathrm {o}} x ^ {\prime} \leq g _ {\mathrm {o}} y. \ x \leq g \circ y \ \end{array} $$

and thus we have established that

(11) ${f}_{0}x \leq y \Rightarrow x \leq g \circ y$

follows from (8) . Consider now the following transformations

$\alpha : x \leftrightarrow y\;$ ,i.e. an interchange of $x$

, i.e. an interchange of the arguments of $\leq$ ; note that the transpose of a partial order is again a partial order (in particular transitive).

$\gamma : f \leftrightarrow g\;$ ,i.e. an interchange of $f$ and $g$

1. i.e. an interchange of the arguments of $0$ ; note that the "transpose" of a functional composition is again a functional composition (in par

ticular monotonic)

Note that the transformations $\alpha ,\beta ,\gamma ,\delta$ commute and that each is its own inverse.

Because $\left( 8\right) \Rightarrow \left( {11}\right)$ and the combination $\left( {\alpha ,\beta ,\gamma }\right)$ leaves (8) unchanged,(8) implies(11)transformed by $\left( {\alpha ,\beta ,\gamma }\right)$ :

$$ x \leq g \circ y \Rightarrow f \circ x \leq y $$

but that is pong! Hence we have established (8) $\Rightarrow$ (9).

Because (8) $\Rightarrow$ (9) and the combination $\left( {\beta ,\delta }\right)$ leaves (8) unchanged,(8) implies (9) transformed by $\left( {\beta ,\delta }\right)$ :

$$ y \leq x \circ f \equiv y \circ g \leq x $$

but that is (10)! Hence we have established $\left( 8\right) \Rightarrow \left( {10}\right)$ .

Note We have not used that $\leq$ is antisymmetric,so for this part of the theory it suffices that $\leq$ be a "pre-order", i.e. a reflexive and transitive relation. (End of Note.)

• • Admittedly the above argument is longer than four times the proof of (8) $\Rightarrow$ (11),

the length proving (8) $\Rightarrow \left( 9\right) \land \left( {10}\right)$ would have required traditionally. But that traditional proof would have been repetitive, and the transformations $\alpha ,\beta ,\gamma ,\delta$ have their charm.

The above has been triggered by a meeting of the ETAC, and in particu cular Wim Fegen's insistence on "the symbol dynamics" that would enable him to remember how to derive (10) from (9). Furthermore the influence of Roland Backhouse et al. is gratefully acknowledged.

When - what perhaps we should not do- we consider transformations $\alpha ,\beta ,\gamma ,s$ "semantically meaningless", it could be argued that we have pushed the notion of calculation to a next level of abstraction.

Austin, 8 September 1994

Prof. Dr. Edsger W. Dyrkstra Department of Computer Sciences The University of Texas at Austin, Austin, TX 78712-1188 USA