How closures could have been invented

How closures could have been invented

Let us consider some type and a func tion $f$ from that type to that type, a so-called endofunction. Argument and function value being of the same type means that we can now consider the equation

(0) $x: p \cdot x = x$ ,

solutions of which are called fixpoints

Without any further knowledge of the type, there is little more we can say about the solutions of (0) than that each value of the type solves (0) if $f$ is the identity function (and vice versa).

In order to be able to say somewhat more we impose some structure on the type by introducing a relation $\equiv$ (pro- nounced "under") on it, which we postulate to be a partial order, i.e. to be

(1) reflexive , i.e. $x \leq x$

(2) antisymmetric, i.e. $x \equiv y \land y \equiv x \Rightarrow x = y$ (3) transitive, i.e. $x \in y \land y \in z \Rightarrow x \in z$ , the above three formal explanations holding for all $x,y,z$ of the type in question.

Aside From a logical point of view, the existence of a partial order on the type is a very mild requirement, since = (read "equals") is a partial order; we leave to the reader to verify that = is indeed reflexive, antisymmetric, and transitive. Equality is a very spe- cial relation in that it is also symmetric i.e. $x = y \equiv y = x$ ,a constraint that does not hold for the general partial order $\varepsilon$ : xEy may differ from y£x. (End of Aside.)

We can use our partial order to strengthen equation (0) and express that we are only interested in fixpoints of $f$ that are "above" some lower bound $h$ ; in formula, we consider the solutions of

(4) $x : f\left( x\right) = x \land h \in x$

Did the solutions of (0) depend only on $f$ , those of (4) depend in general on

h as well.

Equation (4) can still have many so- lutions, but very often the relation E provides the means for singling out a special one, which - if it exists- is known a the lowest solution of (4). It is singled out by stating that we are interested in that solution $x$ of (4) that in addition satisfies

(5) $f \cdot y = y \land h \equiv y \Rightarrow x \equiv y\;$ for any $y$ .

In words: the lowest solution (of (4)) is required to lie under any solution $y\left( {o,f}\right)$ ).

Aside For any equation, there is at most 1 lowest solution, as is shown by the following argument. Let $p$ and $q$ both be a lowest solution of the equation $x$ : $B.x$ ,i.e. we have

(6) B. p (7) $B.y \Rightarrow p \leq y\;$ for all $y$ (8) B. 9 (9) $B \cdot y \Rightarrow q = y\;$ for all $y$ .

We now deduce the equality of $p$ and $q$ by observing

$$ \begin{array}{l} \Leftarrow \quad p = q \quad (2), i.e. \subseteq \mathrm {i s a n t i s y m m e t r i c} \ \Leftarrow \quad \begin{array}{l} {p \equiv q \wedge q \equiv p} \ {\left{(7) \mathrm {w i t h} y := q; (9) \mathrm {w i t h} y := p \right}} \end{array} \ \equiv \begin{array}{l} B. q \wedge B. p \ {(8); (6) } \end{array} \ t r u e \ \end{array} $$

If a lowest solution exists, it is unique. (End of Aside.)

The lowest solution of (4) depends in general on $f$ and $h$ . The simp- plect expression that does so is $f\& h$ and that raises the question: what properties are required of $f$ such that (for any $h$ ), $f\& h$ is the lowest solution of (4)? Formally: which properties of $f$ enable us to establish

$$ \begin{array}{l} (1 0) \quad f. (f, h) = f, h \quad \wedge \quad h \subseteq f, h \ (1 1) \quad f. y = y \land h \equiv y \Rightarrow f. h \equiv y \qquad ? \ \end{array} $$

Relation (10) follows if $f$ is

(12) raising, i.e. $x \leq f \cdot x\;$ ,and (13) idempotent , i.e. $f\left( {f \cdot x}\right) = f \cdot x$

(the formal explanations holding for all $x$ )

In order to establish (11) we observe, starting with the consequent

$\Leftrightarrow \begin{array}{l} {f}_{.}h \leq y \ \left{ {\text{ substituting equals for equals}}\right} \end{array}$ $\Leftarrow \left{ {\begin{array}{l} f \end{array}\text{ is monotonic,see (14)}}\right}$ $P \cdot y = y \land h \equiv y$

i.e. for the demonstration of (11) we need that $f$ is

(14) monotonic, i.e. $x \leq y \Rightarrow f \cdot x \leq f \cdot y$ . (Another name for "monotonic (with respect to $E$ " is "E-preserving".)

A function that is raising, idem- potent and monotonic is called a closure, and we have established the Theorem If $\rho$ is a closure, $\phi$ is the lowest solution of

$$ x: f _ {x} = x \wedge h _ {5} x $$

And that concludes my story of how closures could have been discovered.

Austin, 1 September 1998

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