Coalgebraic representations of distributive lattices with operators

M.M. Bonsangue ^{∗}

LIACS, Leiden University The Netherlands

        marcello@liacs.nl

A. Kurz ^{†}

University of Leicester United Kingdom

                                  kurz@mcs.le.ac.uk

I.M. Rewitzky

University of Stellenbosch South Africa

                                                           rewitzky@sun.ac.za

Abstract

We present a framework for extending Stone’s representation theorem for distributive lattices to representation theorems for distributive lattices with operators. We proceed by introducing the definition of algebraic theory of operators over distributive lattices. Each such theory induces a functor on the category of distributive lattices such that its algebras are exactly the distributive lattices with operators in the original theory. We characterize the topological counterpart of these algebras in terms of suitable coalgebras on spectral spaces. We work out some of these coalgebraic representations, including a new representation theorem for distributive lattices with monotone operators.

1 Introduction

Boolean algebras with operators were first introduced and investigated in 1951 by Jónsson and Tarski [18, 19] as a common framework for the study of several algebras and logics, including relation algebras, cylindric algebras and modal logics. Using Stone’s topological representation of Boolean algebras [37], they showed that every Boolean algebra with operators can be represented as a relational structure. Their result played an important role in the study of many extensions of classical logics, such as normal modal logics [11] and monotone modal logics [14].

Although Jónsson and Tarski considered only Boolean algebras with operators, their result suggested that similar methods can be applied to more general algebraic structures for which a representation theorem is known. For example, an extensive theory of representation of distributive lattices with operators has been developed in the past years [7, 36, 8, 9], either using Stone’s representation of distributive lattices in terms of spectral spaces [38], or Priestley’s duality [30], an alternative to Stone’s original duality.

Building on the original Stone representation theorem, in this paper we present a framework aiming at a general representation theory of distributive lattices with operators in terms of relational structures. Following Rutten [34], we see a relational structure as a coalgebra, allowing the treatment of a large variety of different relational structures in a uniform way.

∗The research of Dr. Bonsangue has been made possible by a fellowship of the Royal Netherlands Academy of Arts and Sciences

†Partially support by the Nuffield Foundation Grant NUF-NAL04.

Stone duality between distributive lattices and spectral spaces can be lifted to a duality between suitable coalgebras over spectral spaces and algebras over distributive lattices induced by algebraic theories of operators over distributive lattices.

Informally speaking, coalgebras encode operational meaning of systems in terms of the possible next-steps relation a system may engage in; whereas algebras over distributive lattices describes how to construct, up to logical equivalence, formulae for this next-step relations from an intuitionistic (i.e. negation free) logic. The usefulness of our framework stems from the fact that a lifting of Stone duality to a duality between coalgebras and algebras automatically gives rise to non-classical logics that are sound, complete, and expressive with respect to a suitable relational semantics [4].

Our approach greatly differs from most of the work on distributive lattices with operators we are aware of (e.g. [7, 36, 8, 22, 27, 9]), all based on canonical extensions of distributive lattices. Canonical extensions are a very useful technique for enriching topological spaces with relations, obtaining structures departing from classical constructors as studied in topology. Our framework can be casted in terms of classical works on topology, universal algebra and locale theory. For example we consider coalgebras arising from classical hyperspace constructors [24, 26], and theories of operators on distributive lattices inducing functors on distributive lattices that have been greatly studied in the context of domain theory and locales. This goes back to Johnstone [17] where a dual of the Vietoris hyperspace, called Vietoris locale, is described. Winskel [41] used additive and multiplicative operators to describe the Plotkin powerdomain [29], and Robinson [32] established the connection between the work in domain theory and that of Johnstone. Abramsky [1] extended these ideas to give logical descriptions of domains for a large number of other functors. Bonsangue [3] and Brink and Rewitzky [31] applied these ideas to the semantics of programming languages.

We argue that the category of topological spaces in general, and spectral spaces in particular, forms an interesting base category for coalgebras. In fact, most of the work with the aim of giving semantics to coalgebraic logics (as e.g.[33, 15, 25]) can be casted in terms of so-called predicate liftings, as in Pattinson [28].^{1} In [21] it was shown that any modal logic given by predicate liftings in the sense of [28] can be described by a functor on Boolean algebras, or, equivalently, by a category of Boolean algebras with operators. In [5] this was generalised to other algebraic categories including distributive lattices.

We proceed as follows. In Section 2 we recall Stone’s representation theorem for distributive lattices, and, in Section 3, some basic notions from universal algebra and coalgebra. In Section 4 we introduce a definition of algebraic theory of operators over distributive lattices in a such way that it induces a canonical functor on distributive lattices. As in [5], algebras over the induced functors are exactly algebras of the original theories of distributive lattices with operators. Using Stone duality, we relate these algebras with coalgebras generated by a suitable functor over spectral spaces. This abstract framework is then applied to theories of additive and multiplicative operators. In Section 5 we extend the approach of [5] from sets to posets, that is, we move to ordered algebras to consider theories of monotone operators over distributive lattices, and give a new representation of distributive lattices with monotone operators in terms of the double hyperspace, obtained by composing (in either order [20]) the upper and lower hyperspace constructions, as extensively studied in [40].

1Given T:Set → Set, a predicate lifting is a natural transformation λ_{X}:2^{X} → 2^{T X}, which lifts predicates over X to predicates over T X (2 is here the contravariant powerset functor). The import of predicate liftings λ stems from the fact that they give semantics to modal operators □_{λ} in a canonical way: Given a T -coalgebra (X, ξ) and a predicate A ⊆ X, □_{λ}A is defined as □_{λ}A = ξ^{−1}(λ_{X}(A)).

Acknowledgments We would like to thank the anonymous referee and Hans-Peter Kunzi for the useful comments and remarks.

2 Stone duality for distributive lattices

A distributive lattice D is a partial order that has join and meets for arbitrary finite subsets, and it satisfies the distributive law

a ∧ (b ∨ c) = (a ∧ b) ∨ (a ∧ c)

We denote by ⊤ the empty meet, and by ⊥ the empty join. For example, the two-element partial order 2 with ⊥ ≤ ⊤ is a distributive lattice. Distributive lattices with functions preserving both finite joins and finite meets form a category called DLat.

In what follows we will often refer to Stone’s representation theorem for distributive lattice [38]. We mention below the main ingredients of Stone’s result. The points of a distributive lattice D are defined by the set S(D) of morphisms f:D → 2 in DLat. This set of points can be equipped with a topology with basic opens defined, for every x ∈ D, by

△(x) = {f:D → 2 | f(x) = ⊤}

In particular, the distributive lattice 2 has one single point, the identity morphism id_{2}:2 → 2, and two basic opens, namely △(⊥) = ∅ and △(⊤) = {id_{2}}.

Definition 2.1 A topological space X is spectral if it is sober and its compact opens form a basis for X and are closed under finite intersections. If, moreover, the compact opens are closed under complement, then X is said to be a Stone space.

For every distributive lattice D, the topological space S(D) is spectral. Spectral spaces can be organized into a category Spec by taking as morphisms all continuous maps with inverse preserving compact opens. Examples of spectral spaces are Scott domains taken with the Scott topology [29].

Our interest in spectral spaces is justified by the following observation. Since finite unions of compact opens are again compact, it follows that if X is a spectral space then the set K(X) of its compact opens is a distributive lattice. Moreover, if f:X → Y is a morphism between the spectral spaces X and Y then

K(f) = f^{−1}: K(Y) → K(X)

is well-defined and preserves finite meets and finite joins of the distributive lattice K(Y). Thus we have a functor K: Spec → DLat^{op}.

Lemma 2.2 The assignment D ↦ S(D) for each distributive lattice D can be extended to a functor from DLat^{op} to Spec which is the right adjoint of K.

For a spectral space X, the unit η_{X}:X → S(K(X)) of the above adjunction, given by the assignments

x ↦ p_{x}:K(X) → 2 where p_{x}(o) = ⊤ ⟺ x ∈ o for o ∈ K(X),

is an isomorphism. The same holds also for the co-unit △(−):D → K(S(D)). This result, originally due to M. Stone [38], can be viewed as a generalization of his famous representation theorem for Boolean algebras [37].

Theorem 2.3 The functors S and K establish a dual equivalence between the categories DLat and Spec:

Spec ^{K} DLat_{S}  (1)

In other words, every distributive lattice D is isomorphic in DLat to K(S(D)) via △, and every spectral space X is isomorphic in Spec to S(K(X)) via η_{X}. By definition of △(D) we have the following corollary.

Corollary 2.4 For each distributive lattice D and d_{1}, d_{2} ∈ D, if d_{1} ≰ d_{2} then there exists a morphism f:D → 2 such f(d_{1}) = ⊤ but f(d_{2}) = ⊥.

3 Algebras and coalgebras

An algebraic theory 𝕋 = (Σ, E) consists of a set Σ of function symbols σ, each with an associated arity n_{σ}, and a set E of equations consisting of pairs (e_{l}, e_{r}), where e_{l} and e_{r} are expressions formed from a set of variables V by applying the given function symbols.

A 𝕋-algebra is a set A together with a corresponding function σ_{A}:A^{n_{σ}} → A for each function symbol σ ∈ Σ, such that, independently of the way we substitute elements of A for the variables, each equation in E holds in A as an identity. A homomorphism between two 𝕋-algebras A and B is a function f:A → B such that σ_{B} ∘ f^{n_{σ}} = f ∘ σ_{A} for each function symbol σ ∈ Σ. The category of 𝕋-algebras is denoted by Alg(𝕋).

Given a functor F on a category A, an F -algebra (denoted by (A, α) or simply α) is a morphism α:F A → A in A. A morphism f:α → α′ between two F -algebras is a morphism f:A → A′ in A such that f ∘ α = α′ ∘ F f. The category of F -algebras is denoted by Alg(F). Dually, given a functor T on a category X, a T -coalgebra (denoted by (X, ξ) or just ξ) is a morphism ξ:X → T X in X. A morphism f:ξ → ξ′ between two T -coalgebras is a morphism f:X → X′ in X such that T f ∘ξ = ξ′∘f. The category of T -coalgebras is denoted by Coalg(T).

A category A, or more precisely, a functor U:A → Set is monadic if A is (isomorphic to) a category Alg(𝕋) of 𝕋-algebras over an algebraic theory 𝕋 = (Σ, E) and, moreover, U has left adjoint. The latter condition implies that a monadic category has free algebras. For example, the category of distributive lattices DLat is monadic [16]. Indeed DLat ≅ Alg(𝔻), where 𝔻 = (Σ_{𝔻}, E_{𝔻}) is the algebraic theory of distributive lattices with a signature Σ_{𝔻} consisting of two function symbols of arity 0 (namely ⊤ and ⊥) and two binary function symbols (namely ∧ and ∨). The set of equations E_{𝔻} is as expected. Because the forgetful functor U:DLat → Set is monadic, it has a left adjoint denoted by F throughout. Hence F X is the free distributive lattice over X and UF X is the set of equivalence classes of Σ_{𝔻}-terms over X modulo the equations E_{𝔻}.

We conclude by recalling a useful technique to describe objects of monadic categories (for more see [39]). Let U:A → Set, be a monadic functor with left adjoint F. A presentation A⟨G | R⟩ of an object of A consists of a set of generators G and a set of relations R ⊆ UF G × UF G. A morphism f:F G → A in A satisfies the relations R if (t, s) ∈ R implies Uf(t) = Uf(s). An object A is presented by A⟨G | R⟩ if

F G_{ı_{A}}  _{f} A _{f^{+}} A′

• A comes with an insertion of generators ı_{A}:F G → A satisfying the relations R,

• for all A′ ∈ A and all f:F G → A′ satisfying the relations R there is a unique f^{+}:A → A′ with f^{+} ∘ ı_{A} = f.

For example, each distributive lattice D can be presented in DLat by taking as generators the set {d̂ | d ∈ D} and as relations the set containing the pairs (ˆ⊤, ⊤), (ˆ⊥, ⊥), and

(({ \atop d_{1} ∧ d_{2}}), d̂_{1} ∧ d̂_{2}), ({ \atop d_{1} ∨ d_{2}}, d̂_{1} ∨ d̂_{2}) for all d_{1}, d_{2} ∈ D.

The next proposition shows that also the converse holds.

Proposition 3.1 Every presentation A⟨G | R⟩ presents an object in A.

Proof: The proof relies on the fact that A, as a category monadic over Set, has coequalizers [23]. The object presented by A⟨G | R⟩ is given by the coequalizer

F R _{π_{2}^{♯}}^{π_{1}^{♯}} F G ^{ı_{A}} A.

where π_{1}^{♯}, π_{2}^{♯} come from the projections π_{1}, π_{2}:R → UF G. ⊓ ⊔

4 Distributive lattices with operators

The algebraic theory 𝔻 = (Σ_{𝔻}, E_{𝔻}) of distributive lattices can be extended with signature Ω_{𝕆} for operators over distributive lattices and a set of identities I_{𝕆} relating the new operators ω ∈ Ω_{𝕆} with the function symbols of the theory of distributive lattices. The corresponding algebras are called distributive lattice with operators. In what follows we formally define an algebraic theory for operators over distributive lattices, and introduce a framework relating the category of algebras over the extended theory with a category of coalgebras over spectral spaces.

Definition 4.1 ([5]) Let U be the forgetful functor from DLat to Set with left adjoint F. A theory 𝕆 of operators over distributive lattices consists of

1. a signature Ω of operations ω ∈ Ω with arities n_{ω} which gives rise to a functor G_{Ω}:Set → Set, X ↦ ∐_{ω∈Ω} X^{n_{ω}},

2. a set I of identities containing pairs of elements in UF G_{Ω}UF V, for some set V of variables.

Note that I ⊆ UF G_{Ω}UF V × UF G_{Ω}UF V means that the terms appearing in identities may freely use the finite joins and finite meets of distributive lattices but do not contain nested occurrences of operations from Ω. We will discuss this restriction in the conclusions.

For each algebraic theory 𝕆 = (Ω_{𝕆}, I_{𝕆}) of operators over distributive lattices, let 𝕋 = (Σ, E) be the algebraic theory where Σ = Σ_{𝔻} + Ω_{𝕆} is the disjoint union of the signatures, and E = E_{𝔻} + I_{𝕆} is the disjoint union of the equations. The equations in E_{𝔻} and I_{𝕆} are understood as equations over Σ_{𝔻} + Ω_{𝕆}. ^{2} We define the category DLat(𝕆) of distributive lattices with operators in the algebraic theory 𝕆 as the category of algebras Alg(𝕋).

Next we set-up a framework for relating categories of distributive lattices with operators to suitable categories of coalgebras over spectral spaces.

Definition 4.2 Given a theory of operators 𝕆 = (Ω, I) and a functor L:DLat → DLat, we say that a natural transformation f:F G_{Ω}U → L satisfies the identities I if for all distributive lattices D and all morphisms v:F V → D (mapping variables to closed terms) it holds

(t, s) ∈ I ⇒ (f_{D} ∘ F G_{Ω}Uv)(t) = (f_{D} ∘ F G_{Ω}Uv)(s) .

Each theory of operators 𝕆 = (Ω, I) defines a canonical functor L_{𝕆}:DLat → DLat that comes equipped with a natural transformation ı satisfying the identities I. We define the functor L_{𝕆} on a distributive lattice D as

F I ^{π_{1}^{♯}}_{π_{2}^{♯}} F G_{Ω}UF V ^{F G_{Ω}Uv}F G_{Ω}UD ^{ı_{D}} L_{𝕆}D

where the π_{1}^{♯}, π_{2}^{♯} come from the projections π_{1}, π_{2}:I → UF G_{Ω}UF V, and ı_{D} is the joint coequalizer with respect to all pairs (F G_{Ω}Uv∘π_{1}^{♯}, F G_{Ω}Uv∘π_{2}^{♯}), for v:F V → D. The universal property of L_{𝕆}D gives the action of L_{𝕆} on morphisms and the requested naturality of ı.

The distributive lattice L_{𝕆}D can be presented in DLat by taking as generators the set G_{Ω}UD of all Ω terms over D, and as relations the set of all pairs

(UF G_{Ω}Uv ∘ Uπ_{1}^{♯}(l), UF G_{Ω}Uv ∘ Uπ_{2}^{♯}(r))

for all v:F V → D, and (l, r) ∈ UF I. More intuitively, we take as relations the set of all instantiations of the identities I obtained by substituting the variables with elements of D.

Theorem 4.3 ([5]) Let 𝕆 = (Ω_{𝕆}, I_{𝕆}) be a theory of operators for distributive lattices and L_{𝕆}:DLat → DLat its associated canonical functor. Then the category of distributive lattices with operators DLat(𝕆) is isomorphic to the category Alg(L_{𝕆}).

Proof: Let Σ be Σ_{𝔻} + Ω_{𝕆}, and E be E_{𝔻} + I_{𝕆}. Consider an L_{𝕆} algebra α:L_{𝕆}D → D. The corresponding Σ-algebra A has carrier UD and the interpretation ω^{A} of the operations ω ∈ Ω_{𝕆} is given by (UD)^{n_{ω}} → UF G_{Ω_{𝕆}}UD →^{Uı_{D}} ULD →^{Uα} UD, where the leftmost arrow is stemming from the composition of counit of the adjunction between DLat and Set with a suitable projection associated with the functor G_{Ω_{𝕆}}. The algebra A satisfies the equations E_{𝔻} because D does, and it satisfies the identities I_{𝕆} because ı_{D} does.

2Strictly speaking, I_{𝕆} was defined on equivalence classes of Σ_{𝔻}-terms. Formally, one obtains the new I_{𝕆}, denoted I′_{𝕆}, as follows. Let T_{Σ_{𝔻}}V be the set of Σ_{𝔻}-terms with variables in V. Consider a left-inverse m of the quotient T_{Σ_{𝔻}}G_{Ω_{𝕆}}T_{Σ_{𝔻}}V → UF G_{Ω_{𝕆}}UF V (m chooses a representative for each equivalence class). Then I′_{𝕆} = {(m(t), m(s)) | (t, s) ∈ I_{𝕆}}.

Conversely, every (Σ, E)-algebra A is also a distributive lattice. We then obtain, from the operations in Ω_{𝕆}, a function G_{Ω_{𝕆}}UA → UA, i.e. a morphism f:F G_{Ω_{𝕆}}UA → A. Since A satisfies the equations I_{𝕆} we obtain the required L_{𝕆} algebra f^{+}:L_{𝕆}A → A. ⊓ ⊔

To summarize the situation, for each theory 𝕆 = (Ω_{𝕆}, I_{𝕆}) of operators for distributive lattices, we have the following diagram:

Alg(L_{𝕆})  ≅  DLat(𝕆) Spec _{K} DLat_{S}  _{L_{𝕆}}_{U} Set_{F}  (2)

The ultimate goal of this paper is to give coalgebraic representations of distributive lattices with operators. The idea is to extend the duality generated by the functors K and S using a functor on Spec dual to L_{𝕆}, where a functor T on Spec is called the dual of L_{𝕆} if there is a natural isomorphism δ:L_{𝕆}K → KT.

The natural isomorphism δ gives us the link between the algebraic structure of distributive lattices with operators and the relational structure of coalgebras. Indeed it allows us to extend the equivalence in Diagram (1) to an equivalence of algebras and coalgebras by lifting the functors K and S. Explicitly, on objects, the lifted K̃:Coalg(T) → Alg(L) and S̃:Alg(L_{𝕆}) → Coalg(T) are given as

\begin{aligned}K̃(X, ξ) & = & LK(X) ⟶^{δ_{X}} K(T X) ⟶^{K(ξ)} K(X) \\ S̃(D, α) & = & S(D) ⟶^{S(α)} S(LD) ≅ S(LK(S(D))) ⟶^{(SδS)_{D}} S(K(T S(D))) ≅ T S(D) \end{aligned}

We can thus fill, for each theory 𝕆 = (Ω_{𝕆}, I_{𝕆}) of operators for distributive lattices, the upper left corner of Diagram (2) as follows:

Coalg(T) ^{K̃} Alg(L_{𝕆})_{S̃}  ≅  DLat(𝕆) Spec_{T}  _{K} DLat_{S}  _{L_{𝕆}}_{U} Set_{F}

If T is a dual functor of L_{𝕆} then we say that category Coalg(T) is a representation of the category of distributive lattices with operators in the theory 𝕆.

In the remainder of this section we give a few examples of functors T such that T - coalgebras represent distributive lattices with operators. Our discussion follows a common pattern. For each theory of operators 𝕆 and each distributive lattice D, we give a presentation of the distributive lattice L_{𝕆}D by generators and relations. Our method for establishing a representation theorem for DLat(𝕆) goes via the definition of an isomorphism δ_{X}:L_{𝕆}K(X) → KT (X) in DLat, where T is an assignment between spectral spaces. The assignment T can be lifted to a functor using the isomorphism δ_{X}, the functor L_{𝕆} and the unit η of the duality between Spec and DLat. More explicitly, we define the action of T on a morphism f:X → Y as follows

T (f) = T X ⟶^{η_{T X}} SKT X ⟶^{Sδ_{X}} SL_{𝕆}KX ⟶^{SL_{𝕆}Kf} SL_{𝕆}KY ⟶^{Sδ_{X}^{−1}} SKT Y ⟶^{Sη_{T Y}^{−1}} T Y .

This way δ is a natural isomorphism between the functors L_{𝕆}K(X) → KT (X). By the discussion above we finally obtain the category Coalg(T) as representation of the category DLat(𝕆).

4.1 Additive operators

Let us consider the theory of an additive operator 𝔸 = (Ω, I), where Ω contains a unary operation ♢. Further, taking V = {v_{0}, v_{1}} as set of variables, and, writing ”· = ·” instead of ”(·, ·)”, the set of identities I is given by

♢⊥ = ⊥ and ♢(v_{0} ∨ v_{1}) = ♢v_{0} ∨ ♢v_{1} .

The theory 𝔸 induces a functor L_{𝔸}:DLat → DLat, mapping each distributive lattice D to the distributive lattice

L_{𝔸}D = DLat⟨♢d:d ∈ D | ♢ preserves finite joins⟩.

By Theorem 4.3, the category DLat(𝔸) of distributive lattice with an additive unary operator is isomorphic to the category of algebras Alg(L_{𝔸}). We want to find a functor on Spec dual to L_{𝔸}. First we note that points of the distributive lattice L_{𝔸}D are related to sets of closed subsets of points of D: The lemma below will allow us to associate f:L_{𝔸}D → 2 with the set SD \ ⋃{Δ(d′) | d′ ∈ D and f(♢d′) = ⊥}.

Lemma 4.4 Let D be a distributive lattice and d ∈ D. For every morphism f:L_{𝔸}D → 2 we have

f(♢d) = ⊥ if and only if Δ(d) ⊆ ⋃{Δ(d′) | d′ ∈ D and f(♢d′) = ⊥}

Proof: The direction from left to right is obvious. For the converse we first notice that the right-hand side is a directed union of compact opens. Since Δ(d) is compact there exists d′ ∈ D with f(♢d′) = ⊥ and Δ(d) ⊆ Δ(d′). Because Δ(−) is isomorphic as co-unit of the adjunction, d ≤ d′, from which it follows f(♢d) ≤ f(♢d′) = ⊥ because both f and ♢ preserve joins. ⊓ ⊔

Next we recall the definition of the topology of the lower hyperspace [24, 26].

Definition 4.5 For a spectral space X, we define the lower hyperspace L(X) to be the set of all closed subsets of X taken with the topology generated by the sub-basic sets

L_{o} = {c ∈ L(X) | c ∩ o ≠ ∅}

for each o ∈ K(X).

Spectral spaces are closed under the lower hyperspace construction, that is, if X is a spectral space then so is L(X) [35].

We can now state and prove the essential ingredient for a coalgebraic representation of distributive lattices with additive operators.

Theorem 4.6 For each spectral space X, L_{𝔸}K(X) is isomorphic in DLat to KL(X).

Proof: Let X be a spectral space and o be a compact open of X. The assignment ♢o ↦ L_{o} extends to a morphism γ:F G_{K(X)} → KL(X), where G_{K(X)} is the set of generators of L_{𝔸}K(X). Since L_{∅} = ∅ and L_{o_{1}∪o_{2}} = L_{o_{1}} ∪ L_{o_{2}}, the morphism γ satisfies the relations of L_{𝔸}K(X). Hence we obtain a canonical morphism γ^{+}:L_{𝔸}K(X) → KL(X) in DLat, that is, by definition, surjective as a function.

Next we prove that γ^{+} is an isomorphism. Because ♢ preserves joins, an element in L_{𝔸}K(X) is the finite meet of elements in G_{K(X)}. Suppose ⋀_{I} ♢o_{i} ≰ ⋀_{J} ♢o_{j}, for some finite index sets I and J, with all o_{i}’s and o_{j}’s in K(X). By Corollary 2.4, there is a morphism f:L_{𝔸}K(X) → 2 in DLat such that f(⋀_{I} ♢o_{i}) = ⊤ but f(⋀_{J} ♢o_{j}) = ⊥, that is, f(♢o_{i}) = ⊤ for all i ∈ I and there is a k ∈ J such that f(♢o_{k}) = ⊥. Consider now the set

S = ⋃{u ∈ K(X) | f(♢u) = ⊥} .

Its complement is closed, and hence in LK(X). Furthermore, by Lemma 4.4, o_{k} ⊆ S whereas o_{i} ⊈ S for all i ∈ I. Hence X \ S ∈ ⋂_{I} L_{o_{i}} but X \ S ∉ L_{o_{k}}. Therefore ⋂_{I} L_{o_{i}} ⊈ ⋂_{J} L_{o_{j}}. ⊓ ⊔

We thus have a duality between the category DLat(𝔸) of distributive lattices with a unary additive operator and the category Coalg(L) of L-coalgebras over spectral spaces.

Recall that a join-hemimorphism is an n-ary operator on a distributive lattice additive on each of its arguments [11, 12]. We leave it to the reader to verify that the functor induced by the theory of a join-hemimorphism on distributive lattices is dual to the functor L ∏_{n}. More generally, the following result holds.

Corollary 4.7 For a theory 𝕆 with a signature Ω of operators additive in each of their arguments, the functor L_{𝕆} is dual to the functor L ∐_{ω∈Ω} ∏_{n_{ω}}.

4.2 Multiplicative operators

Next we consider the theory of a unary multiplicative operator 𝕄 = (Ω, I), where Ω contains a unary operation □, and the set of identities I over the set of variables V = {v_{0}, v_{1}} is given by

□⊤ = ⊤ and □(v_{0} ∧ v_{1}) = □v_{0} ∧ □v_{1} .

The theory 𝕄 induces the functor L_{𝕄}:DLat → DLat, mapping each distributive lattice D to the distributive lattice

L_{𝕄}D = DLat⟨□d:d ∈ D | □ preserves finite meets⟩ .

By Theorem 4.3 we have that the category DLat(𝕄) of distributive lattices with unary multiplicative operators is isomorphic to the category of algebras Alg(L_{𝕄}).

As for additive operators, we have the following lemma, relating points of the distributive lattice L_{𝕄}D with saturated subsets of the representation of D: The lemma below will allow us to associate f:L_{𝕄}D → 2 with ⋂{Δ(d′) | d′ ∈ D and f(□d′) = ⊤}. (Recall that a subset q of a spectral space is saturated if q is the intersection of some compact opens.)

Lemma 4.8 Let D be a distributive lattice and d ∈ D. For every morphism f:L_{𝕄}D → 2 we have

f(□d) = ⊤ if and only if ⋂{Δ(d′) | d′ ∈ D and f(□d′) = ⊤} ⊆ Δ(d)

Proof: The direction from left to right is obvious. For the converse we first notice that right hand side intersection is a filtered intersection of compact open subsets of S(D). Hence we can apply the Hoffman-Mislove theorem [13, 39] to show that there exists d′ ∈ D with f(□d′) = ⊤ and Δ(d′) ⊆ Δ(d). Since Δ(−) is injective, d′ ≤ d, from which it follows ⊤ = f(□d′) ≤ f(□d) because both f and □ preserve finite meets ⊓ ⊔

Compact saturated subsets are used in the definition of the upper hyperspace [24, 26].

Definition 4.9 For a spectral space X we define the upper hyperspace U(X) to be the set of all compact saturated subset of X taken with the topology generated by the basic sets

U_{o} = {q ∈ U(X) | q ⊆ o}

for each o ∈ K(X).

If X is a spectral space then U(X) is a Scott domain (taken with the Scott topology), and hence spectral [39].

The proof of the theorem below follows the same line of reasoning as that of Theorem 4.6. However the similarity is only apparent, as in one the additivity of the operators is translated into closed sets whereas in the next theorem, the multiplicativity of the operators is translated into (compact) upward-closed sets, and not into (compact) opens as one would expect. Moreover this similarity breaks down even more if one considers spaces that are not sober [3].

Theorem 4.10 For each spectral space X, L_{𝕄}K(X) is isomorphic in DLat to KU(X).

Proof: Let X be a spectral space and o be a compact open of X. The assignment □o ↦ U_{o} extends to a morphism δ:F G_{K(X)} → KU(X), where G_{K(X)} is the set of generators of L_{𝕄}K(X). Since U_{X} = U(X) and U_{o_{1}∩o_{2}} = U_{o_{1}} ∩ U_{o_{2}}, the morphism δ satisfies the relations of L_{𝕄}K(X). Hence we obtain a canonical morphism δ^{+}:L_{𝕄}K(X) → KU(X) that, by definition, surjective as a function.

Next we prove that δ^{+} is an isomorphism in DLat. Because □ preserves meets, an element in L_{𝕄}K(X) is the finite join of elements in G_{K(X)}. Suppose ⋁_{I} □o_{i} ≰ ⋁_{J} □o_{j}, for some finite index sets I and J, and with all o_{i}’s and o_{j}’s in K(X). By Corollary 2.4, there is a a morphism f:L_{𝕄}K(X) → 2 in DLat such that f(⋁_{I} □o_{i}) = ⊤ but f(⋁_{J} □o_{j}) = ⊥. Hence there is k ∈ I such that f(□o_{i}) = ⊤, and f(□o_{j}) = ⊥ for all j ∈ J. Consider now the set S = ⋂{u ∈ K(X) | f(□u) = ⊤}. It is a compact saturated and hence in U(K(X)). Furthermore, by Lemma 4.8, S ⊆ o_{k} whereas S ⊈ o_{j}, for all j ∈ J. In other words, S ∈ U_{o_{k}} but S ∉ ⋃_{J} U_{o_{j}}. Therefore ⋃_{I} U_{o_{i}} ⊈ ⋃_{J} U_{o_{j}}. ⊓ ⊔

We thus have a duality between the category DLat(𝕄) of distributive lattices with a unary multiplicative operator and the category Coalg(U) of U-coalgebras over spectral spaces.

Corollary 4.11 For a theory 𝕆 with a signature Ω of operators multiplicative on each of their arguments, the functor L_{𝕆} is dual to the functor U ∐_{ω∈Ω} ∏_{n_{ω}}.

4.3 Additive and multiplicative operators, together

The above theories 𝔸 of a unary additive operator and 𝕄 of a unary multiplicative operator can be combined in a single complex theory that relates the two operators. We define it by 𝕍 = (Ω, I), where the set Ω contains two unary operations ♢ and □, and the set of identities I over the variables v_{0}, v_{1} is given by

\begin{matrix}♢⊥ = ⊥ & □⊤ = ⊤ \\ ♢(v_{0} ∨ v_{1}) = ♢v_{0} ∨ ♢v_{1} & □(v_{0} ∧ v_{1}) = □v_{0} ∧ □v_{1} \\ □(v_{0} ∨ v_{1}) = □v_{0} ∨ (□(v_{0} ∨ v_{1}) ∧ ♢v_{1}) & □v_{0} ∧ ♢v_{1} = □v_{0} ∧ ♢(v_{0} ∧ v_{1}) . \end{matrix}

The theory 𝕍 induces the functor L_{𝕍}:DLat → DLat, mapping each distributive lattice D to the Vietoris locale of D [17]:

L_{𝕍}D = DLat⟨□d, ♢d:d ∈ D | □ preserves finite meets

♢ preserves finite joins

□(d ∨ d′) = □d ∨ (□(d ∨ d′) ∧ ♢d′) □d ∧ ♢d′ = □d ∧ ♢(d ∧ d′) ⟩ .

By Theorem 4.3 we have that the category DLat(𝕍) is isomorphic to the category of algebras Alg(L_{𝕍}).

Recall that a subset S of a topological space X is convex closed if S = ↑S ∩ \overline{S}, where ↑S is the upper closure of S with respect to the order defined by its topology, and \overline{S} is the topological closure of S [24].

Definition 4.12 For a spectral space X we define the Vietoris hyperspace V(X) to be the set of all compact convex subsets of X taken with the topology generated by the sub-basic sets U_{o} and L_{o} for each o ∈ K(X).

If X is a spectral space then V(X) is also spectral [17, 39].

Theorem 4.13 For each spectral space X, L_{𝕍}K(X) is isomorphic in DLat to KV(X).

Proof: Let X be a spectral space and o be a compact open of X. The assignments □o ↦ U_{o} and ♢o ↦ L_{o} extends to a morphism ρ:F G_{K(X)} → KV(X), where G_{K(X)} is the set of generators of L_{𝕍}K(X). It is not hard to see that ρ satisfies the relations of L_{𝕍}K(X). Hence we obtain a canonical morphism ρ^{+}:L_{𝕍}K(X) → KV(X) that is clearly surjective as a function.

Next we prove that ρ^{+} is an isomorphism in DLat. First of all we note that elements in F G_{K(X)} are finite joins of finite meets of generators in G_{K(X)}. Using the laws of distributive lattices, because □ preserves finite meets, ♢ preserves finite joins, and K(X) is closed under finite unions and finite intersections, we have that every element in F G_{K(X)} is identified to an element of the form ⋁_{I}(□o_{i} ∧ ⋀_{J_{i}} ♢o_{j}) for finite sets I and J_{i}’s, (i ∈ I), and compact opens o_{i}’s and o_{j}’s. Assume

d = ⋁_{I}(□o_{i} ∧ ⋀_{J_{i}} ♢o_{j}) ≰ ⋁_{N}(□o_{n} ∧ ⋀_{M_{n}} ♢o_{m}) = d′

By Corollary 2.4, there is a function f:L_{𝕍}K(X) → 2 such that f(d) = ⊤ but f(d′) = ⊥. Because f is a morphism in DLat, the above means that

1. there exists i_{0} ∈ I such that f(□o_{i_{0}}) = ⊤ and f(♢o_{j}) = ⊤ for all j ∈ J_{i_{0}}; 2. for all n ∈ N, f(□o_{n}) = ⊥ or there exists m_{0} ∈ M_{n} such that f(♢o_{m_{0}}) = ⊥.

Consider now the sets Q = ⋂{u ∈ K(X) | f(□u) = ⊤}, O = ⋃{u ∈ K(X) | f(♢u) = ⊥} and C = Q ∩ (X \ O). The set Q is compact saturated (and hence upper closed), O is open and C is compact because it is the intersection of a compact set with a closed one. Since X \ O is closed, \overline{C} ⊆ X \ O. Similarly, because Q is upper closed, ↑C ⊆ Q. Hence ↑C ∩ \overline{C} ⊆ C. Since the other inclusion trivially holds, we have that C is a convex closed set. Therefore C ∈ V(K(X)).

By Lemma 4.8 C ⊆ Q ⊆ o_{i_{0}}, that is C ∈ U_{o_{i_{0}}} . Further, for each u ∈ K(X) such that f(□u) = ⊤ and for each j ∈ J_{i_{0}} we have

⊤ = f(□u) ∧ f(♢o_{j}) = f(□u ∧ ♢o_{j}) ≤ f(♢(u ∩ o_{j})) ,

where the last inequality follows from the relations in L_{𝕍}K(X) and because f is monotone. Hence, by Lemma 4.4, u ∩ o_{j} ⊈ O for all u ∈ K(X) such that f(□u) = ⊤ and for all j ∈ J_{i_{0}}. By definition, we thus have Q ∩ o_{j} ⊈ O, (or, equivalently, Q ∩ (X \ O) ∩ o_{j} ≠ ∅) for all j ∈ J_{i_{0}}. Therefore C ∈ ⋂_{J_{i_{0}}} L_{o_{j}}, from which we finally obtain that C ∈ ⋃_{I}(U_{o_{i}} ∩ ⋂_{J_{i}} L_{o_{j}}).

Similarly, by Lemma 4.4, if f(♢o_{m_{0}}) = ⊥ for some m_{o} ∈ M then o_{m_{0}} ⊆ O, from which it follows that Q ∩ (X \ O) ∩ o_{m_{0}} = ∅, or, equivalently, C ∉ L_{o_{m_{0}}} . On the other hand, for each u ∈ K(X) such that f(♢u) = ⊥ and for each n ∈ N with f(□o_{n}) = ⊥ we have

f(□(o_{n} ∪ u)) ≤ f(□o_{n} ∨ ♢u) = f(□o_{n}) ∨ f(♢u) = ⊥ ,

where the first inequality follows from the relations in L_{𝕍}K(X) and because f is monotone. Hence, by Lemma 4.8, Q ⊈ o_{n} ∪ u for all u ∈ K(X) such that f(♢u) = ⊥ and for all n ∈ N with f(□o_{n}) = ⊥. By definition, this is equivalent to say Q ⊈ o_{n} ∪ O (or, equivalently, Q ∩ (X \ O) ⊈ o_{n}) for all n ∈ N with f(□o_{n}) = ⊥. Therefore C ∉ U_{o_{n}} for each n ∈ N with f(□o_{n}) = ⊥, showing that C ∉ ⋃_{M}(U_{o_{m}} ∩ ⋂_{N_{m}} L_{o_{n}}).

Summarizing, we have thus seen that

ρ^{+}(d) = ⋃_{I}(U_{o_{i}} ∩ ⋂_{J_{i}} L_{o_{j}}) ⊈ ⋃_{M}(U_{o_{m}} ∩ ⋂_{N_{m}} L_{o_{n}}) = ρ^{+}(d′) ,

proving that ρ^{+} is order preserving and hence an isomorphism in DLat. ⊓ ⊔

As a corollary we obtain a duality between the category DLat(𝕍) of distributive lattices with two unary operators and the category Coalg(V) of V-coalgebras over spectral spaces.

5 Ordered algebras and monotone operators

An ordered algebra (posalg in short) is an algebra with a partially ordered carrier set and monotone operators [10]. More specifically, for an algebraic theory 𝕋 = (Σ, E), a 𝕋-posalg is a poset A together with a corresponding monotone function σ_{A}:A^{n_{σ}} → A for each function symbol σ ∈ Σ, such that, independently of the way we substitute elements of A for the variables, each equation in E holds in A as an identity. A homomorphism between two 𝕋posalg A and B is a monotone function f:A → B such that σ_{B} ∘f^{n_{σ}} = f ∘σ_{A} for each function symbol σ ∈ Σ. The category of 𝕋-posalg is denoted by PosAlg(𝕋).

Clearly every 𝕋-algebra is a 𝕋-posalg. The converse holds, for example, for the theory 𝔻 of distributive lattices, because every partial order on a distributive lattice that makes its operations monotone coincides with the partial order of the distributive lattice itself. It follows that DLat ≅ PosAlg(𝔻). Let PoSet be the category of posets with monotone functions as morphisms. The forgetful functor U:DLat → PoSet has a left adjoint denoted by F, mapping a poset P to the distributive lattice F P presented by taking as generators the underlying set of P and as relations the pairs p ∧ p′ = p for all p ≤ p′ in P. Further, products and coproducts in PoSet are computed as in Set.

Definition 5.1 Let U be the forgetful functor from DLat to PoSet with left adjoint F. A theory 𝕆 of monotone operators over distributive lattices consists of

1. a signature Ω of operations ω ∈ Ω with arities n_{ω} which gives rise to a functor G_{Ω}:PoSet → PoSet, X ↦ ∐_{ω∈Ω} X^{n_{ω}},

2. a set I of identities containing pairs of elements of the underlying set of UF G_{Ω}UF V, for some poset V of variables.

For each algebraic theory 𝕆 = (Ω_{𝕆}, I_{𝕆}) of monotone operators over distributive lattices we define the category DLat(𝕆) of distributive lattices with monotone operators as the category of PosAlg(𝕋). Here 𝕋 = (Σ_{𝔻}+Ω_{𝕆}, E_{𝔻}+I_{𝕆}), where the equations in E_{𝔻} and I_{𝕆} are understood as equations over Σ_{𝔻} + Ω_{𝕆}.

Definition 5.2 Given a theory of monotone operators 𝕆 = (Ω, I) and a functor L:DLat → DLat, we say that a natural transformation f:F G_{Ω}U → L satisfies the identities I if for all distributive lattices D and all morphism v:F V → D (mapping variables to closed terms) it holds

(t, s) ∈ I ⇒ (f_{D} ∘ F G_{Ω}Uv)(t) = (f_{D} ∘ F G_{Ω}Uv)(s) .

In a similar way as we have already seen in the previous section, a theory of monotone operators 𝕆 = (Ω, I) defines a canonical functor L_{𝕆}:DLat → DLat that comes equipped with a natural transformation ı satisfying the identities I. We define the functor L_{𝕆} on a distributive lattice D as

F I ^{π_{1}^{♯}}_{π_{2}^{♯}} F G_{Ω}UF V ^{F G_{Ω}Uv}F G_{Ω}UD ^{ı_{D}} L_{𝕆}D

where the π_{1}^{♯}, π_{2}^{♯} come from the projections π_{1}, π_{2}:I → UF G_{Ω}UF V, and ı_{D} is the joint coequalizer with respect to to all pairs (F G_{Ω}Uv ∘ π_{1}^{♯}, F G_{Ω}Uv ∘ π_{2}^{♯}), for v:F V → D. The universal property of L_{𝕆}D gives the action of L_{𝕆} on morphisms and the naturality of ı. With a proof similar to that of Theorem 4.3, we have that the category of distributive lattices with monotone operators DLat(𝕆) is isomorphic to the category Alg(L_{𝕆}). Therefore we can give a coalgebraic representation of a category of distributive lattices with monotone operators DLat(𝕆) by finding a dual functor T:Spec → Spec.

5.1 Monotone operators

Let us consider the theory of monotone operators ℙ = (Ω, I), where Ω contains a single unary monotone operation ◯ and there are no identities, that is, I = ∅. Then G_{Ω}P = P and, for each distributive lattice D, L_{ℙ}D can be presented by

DLat⟨◯a:a ∈ D | ◯ preserves order⟩ The representation of the distributive lattice L_{ℙ}D is obtained by consecutively applying the lower and upper hyperspace construction.

Theorem 5.3 For every spectral space X, LU(X) ≅ SL_{ℙ}K(X).

Proof: For S ∈ LU(X) define γ(S):K(X) → 2 by

γ(S)(o) = ⊤ iff o ∈ S .

Note that if o_{1} ⊆ o_{2} and o_{1} ∈ S for some lower closed subset of U(X), then also o_{2} ∈ S. Hence γ(S) is monotone, i.e. it satisfies the relations of L_{ℙ}K(X). We can therefore extend γ(S) to a distributive lattice morphism γ^{+}(S) ∈ L_{ℙ}K(X) → 2, that is γ^{+}:LU(X) → SL_{ℙ}K(X). To prove that γ^{+} is continuous we see that, for each o ∈ K(X),

γ^{+^{−1}}(Δ(o)) = {S ∈ LU(X) | γ(S) ∈ Δ(o)}
= {S ∈ LU(X) | γ(S)(o) = ⊤}
= {S ∈ LU(X) | o ∈ S} .

But o ∈ S ∈ LU(X) if and only if S ∩ U_{o} ≠ ∅. Indeed, o ∈ U_{o} by definition, hence if o ∈ S then S ∩ U_{o} ≠ ∅. Conversely, if q ∈ U_{o} then q ⊆ o. Thus, by lower closure of S, if q ∈ S, then also o ∈ S. It follows that γ^{+^{−1}}(Δ(o)) = L_{U_{o}}.

Next define, for f ∈ SL_{ℙ}K(X),

η(f) = {q ∈ U(X) | ⋀_{q⊆o} f(o) = ⊤} .

For q_{1}, q_{2} ∈ U(X), if q_{1} ⊇ q_{2} and ⋀_{q_{2}⊆o} f(o) = ⊤, then also ⋀_{q_{1}⊆o} f(o). Hence η(f) is lower closed, that is, η:SL_{ℙ}K(X) → LU(X). To show that η is a continuous function, we have, for each o ∈ K(X),

η^{−1}(L_{U_{o}}) = {f ∈ SL_{ℙ}K(X) | η(f) ∩ U_{o} ≠ ∅}
= {f ∈ SL_{ℙ}K(X) | o ∈ η(f)}
= {f:L_{ℙ}K(X) → 2 | f(o) = ⊤}
= Δ(o) ,

where the second equality holds because o ∈ S ∈ LU(X) if and only if S ∩ U_{o} ≠ ∅, as we have already seen above.

The function η is inverse of γ. Indeed, for f ∈ SL_{ℙ}K(X) and o ∈ K(X) we have

γ(η(f))(o) = ⊤ ⟺ o ∈ η(f)
⟺ ⋀_{o⊆o′} f(o′) = ⊤
⟺ f(o) = ⊤ [f is monotone]

and also, for S ∈ LU(X) and q ∈ U(X),

q ∈ η(γ(S)) ⟺ ⋀_{q⊆o} γ(S)(o) = ⊤
⟺ ∀q ⊆ o.o ∈ S
⟺ q ∈ S

where the last implication from right to left holds because S is lower closed, whereas the implication from left to right holds because U(X) is a Scott domain, thus S is Scott closed. Since the set {o | q ⊆ o} is directed in U(X), it follows that its least upper bound q must be in S. ⊓ ⊔

Since the continuous image of compact opens is compact, as a corollary we obtain an isomorphism in DLat between KLU(X) and L_{ℙ}K(X). Thus it follows that the category of distributive lattices with a unary monotone operator is isomorphic to the category of LU-coalgebras.

6 Conclusion and future directions

In this paper we presented a framework for a coalgebraic representation of distributive lattices with operators. We have applied our method to several theories of operators, including additive, multiplicative and monotone operators.

An immediate investigation is to apply our framework to similar operators but contravariant in their arguments, as studied, for example, in [36]. One intriguing way to define suitable coalgebraic representations could be to re-consider the definitions of the sub-basic opens of the lower, upper and Vietoris hyperspaces by indexing them with closed sets rather than with opens.

Although we have considered here only operators on distributive lattices, our framework could be applied to any category of algebras over Set (with minor changes for infinitary algebras to take into account equations involving infinitary operations) for which a dual category is known [5]. For example, to consider additional properties such as completeness of the lattice operations and of the operators, we can take the category of algebraic completely distributive lattices (the canonical extensions of distributive lattices [7, 8, 9]) as starting point of our investigations. Its dual is well-known: the category of PoSet.

Let us point out that our approach allows us to treat theories with arbitrary nesting of operators in their identities, although, according to Definitions 4.1 and 5.1, terms appearing in equations may not contain nested occurrences of operations from the theory 𝕆 of operators. Intuitively, this restriction arises from our interest in a representation via coalgebras for a functor T dual to L_{𝕆}. In contrast to coalgebras for a comonad, a T -coalgebra encodes the operational view of what a system can perform in one single step [34]. From this point of view, our format of the equation is not a restriction, but formalizes that we do not need nested modalities to describe a single step (nested modalities describe sequences of steps), see [5]. In other words, identities with nested operators are not identities on distributive lattices, but rather on the algebras for the induced functor from the simple identities. Additional identities with nested operators can be dealt with without problems. They specify particular equationally/modally definable full subcategories of algebras/coalgebras for dual functors.

For example, it is routine to see that the addition of the nested identity □v_{0} ∨ v_{0} = v_{0} (i.e. □v_{0} ≤ v_{0}) on the theory 𝕄 of a unary multiplicative operator characterizes those L_{𝕄} algebras that are represented by reflexive U-coalgebras on spectral spaces, that is, coalgebras α:X → U(X) such that x ∈ α(x) for all x ∈ X. More interestingly, the theory of distributive lattices with a monadic universal quantifier, obtained by adding the nested equations

□v_{0} ∨ v_{0} = □v_{0} and □(v_{0} ∨ □v_{1}) = □v_{0} ∨ □v_{1}

to the theory of 𝕄 of a unary multiplicative operator, characterizes those L_{𝕄} algebras that are represented by U-coalgebras α:X → U(X) with α an equivalence relation on X such that α(o) ∈ K(X) for each o ∈ K(X) (i.e. α is an open equivalence relation on X) and the quotient of X with respect to α is a T_{0} space [2].

References

[1] S. Abramsky. Domain theory in logical form. Annals of Pure and Applied Logic, 51:1– 77, 1991.

[2] N. Bezhanishvili. Distributive lattices with quantifiers: topological representation. In Proc. of the ESSLLI student session 1999, Chapter 8, 1999.

[3] M.M. Bonsangue Topological Dualities in Semantics. Volume 8 of Electronic Notes in Computer Science, Elsevier, 1997.

[4] M.M. Bonsangue and A. Kurz. Duality for Logics of Transition Systems. In Proc. of FOSSACS 2005, volume 3441 of Lecture Notes in Computer science, pages 455-469, Springer, 2005.

[5] M.M. Bonsangue and A. Kurz. Presenting Functors by Operations and Equations. Submitted for publication.

[6] B.A. Davey and H.A. Priestley. Introduction to Lattices and Order. Cambridge University Press, 1990.

[7] M. Gehrke and B. Jónsson. Bounded distributive lattices with operators. Mathematica Japonica, 40:207–215, 1994.

[8] M. Gehrke and B. Jónsson. Monotone bounded distributive lattice expansions Mathematica Japonica, 52(2):197–213, 2000.

[9] M. Gehrke and B. Jónsson. Canonical extensions of bounded distributive lattice expansions. Mathematica Scandinavica, 94(1):13-45, 2004.

[10] J.A. Goguen, J.W. Thatcher, E.G. Wagner, and J.B. Wright. Initial algebra semantics and continuous algebras. Journal of the ACM, 24:68–95, 1977.

[11] R. Goldblatt. Varieties of complex algebras. Annals of Pure and Applied Logic, 44:173– 242, 1989.

[12] P. Halmos. Algebraic logic I: monadic boolean algebras. Compositio Mathematicae 12:217–249, 1955.

[13] K.H. Hofmann and M.W. Mislove. Local compactness and continuous lattices. In Continuous Lattices - Proceedings Bremen 1979, volume 871 of Lecture Notes in Mathematics, pages 209–248. Springer-Verlag, 1981.

[14] H.H. Hansen and C. Kupke A Coalgebraic Perspective on Monotone Modal Logic. In Proc. the 7th Workshop on Coalgebraic Methods in Computer Science (CMCS 2004), volume 106 of Electronic Notes in Theoretical Computer Science, pages 121-143, Elsevier, 2004.

[15] B. Jacobs. Many-sorted coalgebraic modal logic: a model-theoretic study. Theoretical Informatics and Applications, 35(1):31–59, 2001.

[16] P.T. Johnstone. Stone Spaces. Cambridge University Press, 1982.

[17] P.T. Johnstone. The Vietoris monad on the category of locales. In Continuous lattices and related topics, volume 27, pages 162–179. Mathematik-Arbeitspapiere, University of Bremen, 1982.

[18] B. Jónsson and A. Tarski. Boolean algebras with operators, part I. American Journal of Mathematics, 73:891–939, 1951.

[19] B. Jónsson and A. Tarski. Boolean algebras with operators, part II. American Journal of Mathematics, 74:127–167, 1952.

[20] P.T. Johnstone and S.J. Vickers. Preframe presentations present. In Proc. Category Theory 1990, volume 1488 of Lecture Notes in Computer Science, pages 193–212. Springer-Verlag, 1991.

[21] C. Kupke, A. Kurz, and D. Pattinson. Algebraic semantics for coalgebraic logics. In Proc. of Coalgebraic Methods in Computer Science (CMCS’04), volume 106 of Electronic Notes in Theoretical Computer Science, Elsevier, 2004.

[22] C. Kupke, A. Kurz, and Y. Venema. Stone coalgebras. Theoretical Computer Science 327:109–134, 2004.

[23] E.G. Manes. Algebraic Theories, volume 26 of Graduate Texts in Mathematics. Springer-Verlag, 1976.

[24] E. Michael. Topologies on spaces of subsets. Transactions of the American Mathematical Society, 71:152–182, 1951.

[25] L. Moss and L. Viglizzo. Harsanyi type space and final coalgebras constructed from satisfied theories. In Proc. of Coalgebraic Methods in Computer Science (CMCS’04), volume. 106 of Electronic Notes in Theoretical Computer Science, Elsevier, 2004.

[26] S.B. Nadler. Hyperspaces of Sets. Pure and Applied Mathematics. Marcel Dekker, 1978.

[27] A. Palmigiano. Coalgebraic Semantics for Positive Modal Logic. Theoretical Computer Science 327:175–195, 2004.

[28] D. Pattinson. Coalgebraic modal logic: Soundness, completeness and decidability of local consequence. Theoretical Computer Science 309, 2003.

[29] G.D. Plotkin. Post-graduate Lecture Notes in Advanced Domain Theory (incorporating the ‘Pisa notes’). Department of Computer Science, University of Edinburgh, 1981.

[30] H.A. Priestley. Representation of distributive lattices by means of ordered Stone spaces. Bulletin of London Mathematical Society, 2:186–190, 1970.

[31] C. Brink and I.M. Rewitzky. A Paradigm for Program Semantics. CSLI Publications, Stanford, 2001

[32] E. Robinson. Logical aspects of denotational semantics. In Summer conference on Category Theory and Computer Science, volume 83 of Lecture Notes in Computer Science, pages 238–253. Springer-Verlag, 1988.

[33] M. Rößiger. From modal logic to terminal coalgebras. Theoretical Computer Science 260:209–228, 2001.

[34] J.J.M.M. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science, 249:3–80, 2000.

[35] A. Schalk. Algebras for generalized power constructions. PhD thesis, Technische Hochschule Darmstadt, Germany, 1993.

[36] V. Sofronie-Stokkermans. Duality and canonical extensions of bounded distributive lattices with operators, and applications to the semantics of non-classical logics I. Studia Logica 64:93–132, 1999.

[37] M.H. Stone. The theory of representation for Boolean algebras. Transactions of the American Mathematical Society, 40:37–111, 1936.

[38] M.H. Stone. Topological representation of distributive lattices and Brouwerian logics. Casopis Pro Potování Mathematiky, 67:1–25, 1937.

[39] S.J. Vickers. Topology via Logic. Volume 5 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.

[40] S.J. Vickers and C.F. Townsend. A Universal Characterization of the Double Powerlocale. Theoretical Computer Science 316:297-321, 2004.

[41] G. Winskel. Powerdomains and modality. In Proc. of Foundations of Computation Theory, volume 158 of Lecture Notes in Computer Science, pages 505–514, Springer-Verlag 1983.