Powerdomains and hyperspaces III: the theory of H

The last post was late.  Let me compensate by being early this time.

I had promised you that we would see why the theory of the Hoare powerspace monad was given by a small family of axioms, those of unital inflationary semilattices.  I will substantiate this claim in two ways.  Following Andrea Schalk, we shall see that H(X) is the free such (sober) thing over X, and we shall see that those (sober) things are exactly the algebras of the H monad—a nice way to introduce the notion of algebra of a monad.  Read the full post.

 

Powerdomains and hyperspaces II: monads

Let us deepen our understanding of the Hoare powerspace construction. We shall see that it defines a so-called monad.  There would be many, many things to say about monads!  I will only give a very superficial introduction here, trying to convince you that the Hoare powerspace construction indeed produces a monad.  In part III, I’ll tell you about the inequational theories of monads, and monad algebras.  Read the full post.