Let us deepen our understanding of the Hoare powerspace construction. We shall see that it defines a so-called monad. I’ll define everything needed to understand the latter as we go along.
Monads
I have briefly mentioned monads in Filters IV. There is an equivalent way of presenting monads (on a category C), as the following data (I don’t expect you to understand those equations for now, we shall illustrate them shortly):
- for each object X of C, an object TX in C
- for each object X of C, a morphism ηX: X → TX called the unit of the monad
- an extension operation †, transforming every morphism f: X → TY into a morphism f†: TX → TY, so that the following equations are satisfied (we explain them shortly):
- ηX† = idTX
- for every morphism f: X → TY, f† o ηX = f
- for all morphisms f: X → TY and g: Y → TZ, (g† o f)† = g† o f†.
We then say that (T, η, †) is a monad, or, by abuse of language, that T itself is a monad. Let’s illustrate that on a concrete example.
Consider the category Set of sets for the category C. The morphisms from X to Y are just the functions from X to Y. Let TX be the powerset P(X) of X, that is, the set of all subsets of X. Define ηX as mapping x in X to {x}, and for every set E, let f†(E) be defined as the union of all the sets f(x), x in E. We check the monad equations as follows:
- ηX† maps E to the union of the sets {x}, x in E, namely E, so ηX† = idTX;
- f† o ηX maps every element x to f†({x}) = f(x), hence is equal to f;
- for every subset E, (g† o f)† (E) is the union over all x in E of g†(f (x)), namely the union over all x in E of the union over all y in f(x) of g(y). On the other hand, (g† o f†) (E) is the union over all y in f† (E) of g(y), and that is just the same thing.
The Kleisli category of a monad
There is a very rich theory of monads. I would like to explain why the equations 1—3 above are what they are. The reason is the construction of the so-called Kleisli category CT of the monad T on C.
This is built as follows. The objects of the CT are the same as those of C; the only thing that changes are the morphisms: the morphisms from X to Y in CT are exactly those from X to TY in the old category C. The map ηX: X → TX serves as the identity morphism at X in CT, and composition of f: X → TY with g: Y → TZ is given by g† o f: X → TZ. The equations 1—3 are exactly what you need to show that this indeed forms a category: composition is associative, and the identity is neutral for composition both on the left and on the right. In fact, you can check that the Kleisli “category” is really a category if and only if the equations 1—3 are satisfied.
In the case of the powerset monad on Set, the Kleisli category can be thought as a category of sets and binary relations as morphisms. Any binary relation R on X x Y defines a Kleisli morphism f: X → P(Y), which maps every x in X to the set {y in Y | (x, y) in R}. Conversely, every Kleisli morphism f: X → P(Y) defines a binary relation R by (x, y) in R if and only if y is in f(x). You can check that the Kleisli identity (the unit of the monad) is the equality relation {(x, x) | x in X}, and that Kleisli composition is the ordinary composition of relations: S o R = {(x, z) | (x, y) in R and (y, z) in S for some y}.
One can also think of the set X as a set of states for some computer system. A Kleisli morphism f from X to TY tells you, given that you are in some state x in X, what the set f (x) of successor states is. In other words, f is a so-called transition relation. The fact that f(x) may contain more than one element means that you can choose y non-deterministically.
Oh, before we examine the more complicated Hoare monad, recall that I had given another definition of monads in Filters IV. We obtain that presentation from a monad as defined above, as follows:
- a functor T from C to C; we already have its object parts, and on morphisms f: X → Y, we define Tf: TX → TY as (ηY o f)† (check, using 1—3, that this is indeed a functor!)
- a natural transformation η from the identity functor to T; this is given as ηX on each object X (check, using 1—3, that this is indeed natural in X);
- a natural transformation μ from T2 to T, defined on each object X by μX = idTX†: T2X → TX (check, again, that this is natural);
- all of these are also required to satisfied the three laws: (left unit) μX o ηTX = idTX, (right unit) μX o TηX = idTX, and (associativity) μX o TμX = μX o μTX. Again, I’ll let you check that those follow from 1—3.
Conversely, any monad as given by a functor, a unit natural transformation, and a multiplication natural transformation satisfying the left unit, right unit, and associativity laws yields back a monad (T, η, †) by defining f† as μX o Tf. The fancy names “left unit”, “right unit”, and “associativity” really come from the fact that monads on C are exactly the monoid objects in the monoidal category of endofunctors of C, with composition as tensor product. (Ignore that if this is your first time with monads, and think of it as some Zen koan: it is impenetrable, but it holds the truth.)
The H monad
We can now proceed with the more complicated case of the H powerspace construction. That this defines a monad is again due to Andrea Schalk [1]. We take C=Top, and let TX=H(X) with the upper (=lower Vietoris) topology.
We already have a continuous map ηX: X → H(X), which sends x in X to the closure ↓x of x. This will be our unit.
Given any continuous map f: X → H(Y), we define f†: H(X) → H(Y) by letting f† (F) be the closure of the union of all the closed subsets f(x), x in F. We need to take the closure because a union of closed subsets may fail to be closed. What we have done here is taking a supremum in H(Y), ordered by inclusion: suprema are closures of unions. In summary, f† (F) = sup {f (x) | x in F}.
Let us check that this indeed defines a monad. This is somehow more complicated than for the powerset monad.
- To show that f† is continuous, we only have to show that the inverse image of ◊V, for V open in Y, is open in H(X). Since the closure of a set intersects an open V if and only if the set itself intersects V (Corollary 4.1.28), that inverse image is ◊f-1 (◊V), and we are done.
We now turn to the monad equations.
- First, ηX† = idH(X). Indeed, the left hand side maps each closed set F to the closure of the union of all the sets ↓x, x in F. That union is just F, and since F is closed, its closure is itself.
- Second, for every continuous map f: X → H(Y), f† o ηX = f. The left hand side maps every x in X to the closure of the union of all the sets f(x’), where x’ ranges over ↓x. Since f is continuous hence monotonic, every such set f(x’) is included in f(x), so (f† o ηX) (x) is included in f(x); the converse inclusion is because x itself is in ↓x.
- Third, for all continuous maps f: X → H(Y) and g: Y → H(Z), we have two maps from H(X) to H(Z), namely (g† o f)† and g† o f†. We claim that they are equal: (g† o f)† = g† o f†… but if you try to prove this directly, you’ll suffer as hell. Instead, recall that for continuous h for which h† makes sense, for every open subset W, (h†)-1 (◊W) = ◊f-1 (◊W): this is how we proved that h† was continuous. Using that, we check that, for every open subset W of Z, the inverse image of ◊W by (g† o f)† and by g† o f† is the same, namely ◊f-1 (◊g-1 (◊W)). This is enough to conclude that (g† o f)† = g† o f† are identical, by Stone duality, and because H(X) is sober. We can also see that directly: for every closed subset F of X, for every open subset W of Z, F is in the inverse image of ◊W by (g† o f)† if and only if it is in in the inverse image of ◊W by g† o f†, that is, for every open subset W of Z, (g† o f)† (F) intersects W if and only if (g† o f†) (F) intersects W; hence they are equal closed sets.
Just like the powerset monad on Set, the Hoare monad H on Top can be thought as some kind of powerset, with extra topological information. As for the powerset monad, the Kleisli morphisms encode some form of non-deterministic choice, called angelic non-determinism. Let me postpone the explanation of that denomination, as I would prefer to explain a few things about theories of monads, and monad algebras… next time. We shall see that, in a precise sense, the theory of the H monad is given by the following axioms:
- (unit) a ∨ 0 = a
- (associativity) (a ∨ b) ∨ c = a ∨ (b ∨ c)
- (commutativity) a ∨ b = b ∨ a
- (idempotence) a ∨ a = a
- (inflationary) a ≤ a ∨ b
Note that, if you interpret ∨ as binary union of closed sets, 0 as the empty set, and ≤ as inclusion, then those (in)equalities are trivially satisfied. A topological space with a continuous map ∨ satisfying the above (in)equalities is called an inflationary semi-lattice. What we shall see is that, for each space X, H(X) is the free sober inflationary semi-lattice above X, as proved by Schalk [1]… and I’ll try to explain what this means.
— Jean Goubault-Larrecq (May 17th, 2015)
[1] Andrea Schalk. Algebras for Generalized Power Constructions. PhD Thesis, TU Darmstadt, 1993.