key: cord-0060383-th5caumq
authors: Bonchi, Filippo; Santamaria, Alessio
title: Combining Semilattices and Semimodules
date: 2021-03-23
journal: Foundations of Software Science and Computation Structures
DOI: 10.1007/978-3-030-71995-1_6
sha: 74874d994ccc15fce9f7383c6d9056e37ada4c01
doc_id: 60383
cord_uid: th5caumq

We describe the canonical weak distributive law [Formula: see text] of the powerset monad [Formula: see text] over the S-left-semimodule monad [Formula: see text] , for a class of semirings S. We show that the composition of [Formula: see text] with [Formula: see text] by means of such [Formula: see text] yields almost the monad of convex subsets previously introduced by Jacobs: the only difference consists in the absence in Jacobs’s monad of the empty convex set. We provide a handy characterisation of the canonical weak lifting of [Formula: see text] to [Formula: see text] as well as an algebraic theory for the resulting composed monad. Finally, we restrict the composed monad to finitely generated convex subsets and we show that it is presented by an algebraic theory combining semimodules and semilattices with bottom, which are the algebras for the finite powerset monad [Formula: see text] .

Monads play a fundamental role in different areas of computer science since they embody notions of computations [32] , like nondeterminism, side effects and exceptions. Consider for instance automata theory: deterministic automata can be conveniently regarded as certain kind of coalgebras on Set [33] , nondeterministic automata as the same kind of coalgebras but on EM(P f ) [35] , and weighted automata on EM(S) [4] . Here, P f is the finite powerset monad, modelling nondeterministic computations, while S is the monad of semimodules over a semiring S, modelling various sorts of quantitative aspects when varying the underlying semiring S. It is worth mentioning two facts: first, rather than taking coalgebras over EM(T ), the category of algebras for the monad T , one can also consider coalgebras over Kl(T ), the Kleisli category induced by T [20] ; second, these two approaches based on monads have lead not only to a deeper understanding of the subject, but also to effective proof techniques [6, 7, 14] , algorithms [1, 8, 22, 36, 39] and logics [19, 21, 27] .

Since compositionality is often the key to master complex structures, computer scientists devoted quite some efforts to compose monads [40] or the equivalent notion of algebraic theories [24] . Indeed, the standard approach of composing monads by means of distributive laws [3] turned out to be somehow unsatisfactory. On the one hand, distributive laws do not exist in many relevant cases: see [28, 41] for some no-go theorems; on the other hand, proving their existence is error-prone: see [28] for a list of results that were mistakenly assuming the existence of a distributive law of the powerset monad over itself.

Nevertheless, some sort of weakening of the notion of distributive law-e.g., distributive laws of functors over monads [26] -proved to be ubiquitous in computer science: they are GSOS specifications [38] , they are sound coinductive up-to techniques [7] and complete abstract domains [5] . In this paper we will exploit weak distributive laws in the sense of [15] that have been recently shown successful in composing the monads for nondeterminism and probability [17] .

The goal of this paper is to somehow combine the monads P f and S mentioned above. Our interest in S relies on the wide expressiveness provided by the possibility of varying S: for instance by taking S to be the Boolean semiring, one obtains the monad P f ; by fixing S to be the field of reals, coalgebras over EM(S) turn out be linear dynamical systems [34] .

We proceed as follows. Rather than composing P f , we found it convenient to compose the full, not necessarily finite, powerset monad P with S. In this way we can reuse several results in [12] that provide necessary and sufficient conditions on the semiring S for the existence of a canonical weak [15] distributive law δ : SP → PS. Our first contribution (Theorem 21) consists in showing that such δ has a convenient alternative characterisation, whenever the underlying semiring is a positive semifield, a condition that is met, e.g., by the semirings of Booleans and non-negative reals.

Such characterisation allows us to give a handy definition of the canonical weak lifting of P over EM(S) (Theorem 24) and to observe that such lifting is almost the same as the monad C : EM(S) → EM(S) defined by Jacobs in [25] (Remark 25): the only difference is the absence in C of the empty subset. Such difference becomes crucial when considering the composed monads, named CM : Set → Set in [25] and P c S : Set → Set in this paper: the latter maps a set X into the set of convex subsets of SX, while the former additionally requires the subsets to be non-empty. It turns out that while Kl(CM) is not CPPO-enriched, a necessary condition for the coalgebraic framework in [20] , Kl(P c S) indeed is (Theorem 30).

Composing monads by means of weak distributive laws is rewarding in many respects: here we exploit the fact that algebras for the composed monad P c S coincide with δ-algebras, namely algebras for both P and S satisfying a certain pentagonal law. One can extract from this law some distributivity axioms that, together with the axioms for semimodules (algebras for the monad S) and those for complete semilattices (algebras for the monad P), provide an algebraic theory presenting the monad P c S (Theorem 32).

We conclude by coming back to the finite powerset monad P f . By replacing, in the above theory, complete semilattices with semilattices with bottom (algebras for the monad P f ) one obtains a theory presenting the monad P f c S of finitely generated convex subsets (Theorem 35), which is formally defined as a restriction of the canonical P c S. The theory, displayed in Table 1 , consists of the 

theory presenting the monad P f and the theory presenting the monad S with four distributivity axioms. To save space we had to omit most of the proofs of the results in this article: the interested reader can find them in [9] .

Notation. We assume the reader to be familiar with monads and their maps. Given a monad (M, η M , µ M ) on C, EM(M ) and Kl(M ) denote, respectively, the Eilenberg-Moore category and the Kleisli category of M . The latter is defined as the category whose objects are the same as C and a morphism f :

Given n a natural number, we denote by n the set {1, . . . , n}.

Given two monads S and T on a category C, is there a way to compose them to form a new monad ST on C? This question was answered by Beck [3] and his theory of distributive laws, which are natural transformations δ : T S → ST satisfying four axioms and that provide a canonical way to endow the composite functor ST with a monad structure. We begin by recalling the classic definition. In the following, let (T, η T , µ T ) and (S, η S , µ S ) be two monads on a category C.

A distributive law of the monad S over the monad T is a natural transformation δ : T S → ST such that the following diagrams commute.

One important result of Beck's theory is the bijective correspondence between distributive laws, liftings to Eilenberg-Moore algebras and extensions to Kleisli categories, in the following sense.

An extension of the monad T to Kl(S) is a monad (T , ηT , µT ) such that

Böhm [11] and Street [37] have studied various weaker notions of distributive law; here we shall use the one that consists in dropping the axiom involving η T in Definition 1, following the approach of Garner [15] .

A weak distributive law of S over T is a natural transformation δ : T S → ST such that the diagrams in (1) regarding µ S , µ T and η S commute.

There are suitable weaker notions of liftings and extensions which also bijectively correspond to weak distributive laws as proved in [11, 15] . such that πι = id U TS and such that the following diagrams commute:

A weak extension of T to Kl(S) is a functorT : Kl(S) → Kl(S) together with a natural transformation µT :TT →T such that F S T =T F S and µT F S = F S µ T .

Theorem 5 ( [3, 11, 15] ). There is a bijective correspondence between (weak) distributive laws T S → ST , (weak) liftings of S to EM(T ) and (weak) extensions of T to Kl(S).

The Monad P. Let us now consider, as S, the powerset monad (P, η P , µ P ), where η P X (x) = {x} and µ P X (U ) = U ∈U U . Its algebras are precisely the complete semilattices and we have that Kl(P) is isomorphic to the category Rel of sets and relations. Hence, giving a distributive law T P → PT is the same as giving an extension of T to Rel: for this to happen the notion of weak cartesian functor and natural transformation is crucial.

Definition 6. A functor T : Set → Set is said to be weakly cartesian if and only if it preserves weak pullbacks. A natural transformation ϕ : F → G is said to be weakly cartesian if and only if its naturality squares are weak pullbacks.

Kurz and Velebil [29] proved, using an original argument of Barr [2] , that an endofunctor T on Set has at most one extension to Rel and this happens precisely when it is weakly cartesian; similarly a natural transformation ϕ : F → G, with F and G weakly cartesian, has at most one extensionφ :F →G, precisely when it is weakly cartesian. The following result is therefore immediate. The Monad S. Recall that a semiring is a tuple (S, +, ·, 0, 1) such that (S, +, 0) is a commutative monoid, (S, ·, 1) is a monoid, · distributes over + and 0 is an annihilating element for ·. In other words, a semiring is a ring where not every element has an additive inverse. Natural numbers N with the usual operations of addition and multiplication form a semiring. Similarly, integers, rationals and reals form semirings. Also the Booleans Bool = {0, 1} with ∨ and ∧ acting as + and ·, respectively, form a semiring. Every semiring S generates a semimodule monad S on Set as follows. Given a set X,

This makes S a functor. The unit η S X : X → S(X) is given by η S 

An algebra for S is precisely a left-S-semimodule, namely a set X equipped with a binary operation +, an element 0 and a unary operation λ· for each λ ∈ S, satisfying the equations in Table 1 . Indeed, if X carries a semimodule structure then one can define a map a : SX → X as, for ϕ ∈ SX,

where the above sum is finite because so is supp ϕ. Vice versa, if (X, a) is an S-algebra, then the corresponding left-semimodule structure on X is obtained by defining for all λ ∈ S and x, y ∈ X

Above and in the remainder of the paper, we write the list (x 1 → s 1 , . . . , x n → s n ) for the only function ϕ : X → S with support {x 1 , . . . , x n } mapping x i to s i and we write the empty list ε for the function constant to 0. For instance, for a = µ S X : SSX → SX, the left-semimodule structure is defined for all ϕ 1 , ϕ 2 ∈ SX and x ∈ X as

Proposition 7 tells us exactly when a (weak) distributive law of the form T P → PT exists for an arbitrary monad T on Set. Take then T = S: when are the functor S and the natural transformations η S and µ S weakly cartesian? The answer has been given in [12] (see also [18] ), where a complete characterisation in purely algebraic properties for S is provided. In Table 2 we recall such properties. Table 2. 3. If S is weakly cartesian, then µ S is weakly cartesian if and only if S enjoys (B) and (E) in Table 2 .

Remark 9. In [12, Proposition 9.1] it is proved that if S enjoys (C) and (D), then S is refinable; if S is a positive semifield, then it enjoys (B) and (E). In the next Proposition we prove that if S is a positive semifield then it is also refinable, hence S and µ S are weakly cartesian.

Proposition 10. If S is a positive semifield, then it is refinable.

.

Example 11. It is known that, for S = N, a distributive law δ : SP → PS exists. Indeed one can check that all conditions of Theorem 8 are satisfied, therefore we can apply Proposition 7.1. In this case, the monad SX is naturally isomorphic to the commutative monoid monad, which given a set X returns the collection of all multisets of elements of X. The law δ is well known (see e.g. [15, 23] ): given a multiset A 1 , . . . , A n of subsets of X in SPX, where the A i 's need not be distinct, it returns the set of multisets { a 1 , . . . , a n | a i ∈ A i }.

Convex Subsets of Left-semimodules. Theorem 8 together with Proposition 7.1 tell us that whenever the element 1 of S can be decomposed as a non-trivial sum there is no distributive law δ : SP → PS. Semirings with this property abound, for example Q, R, R + with the usual operations of sum an multiplication, as well as Bool (since 1 ∨ 1 = 1). Such semirings are precisely those for which the notion of convex subset of their left-semimodules is nontrivial. For the existence of a weak distributive law, however, this condition on 1 S is not required: convexity will indeed play a crucial role in the definition of the weak distributive law.

Definition 12. Let S be a semiring, X an S-left-semimodule and A ⊆ X. The convex closure of A is the set

The set A is said to be convex if and only if A = A.

Recalling that the category of S-left-semimodules is isomorphic to EM(S), we can use (4) to translate Definition 12 of convex subset of a semimodule into the following notion of convex subset of a S-algebra a : SX → X.

A is said to be convex in (X, a) if and only if A = A a . We denote by P a c X the set of convex subsets of X with respect to a.

Observe that ∅ is convex, because ∅ a = ∅, since there is no ϕ ∈ SX with empty support such that x∈X ϕ(x) = 1.

Example 15. Suppose S is such that η S is weakly cartesian (equivalently (A) holds: x + y = 1 =⇒ x = 0 or y = 0), for example S = N, and let (X, a) ∈ EM(S). A ϕ ∈ SX such that x∈X ϕ(x) = 1 and supp ϕ ⊆ A is a function that assigns 1 to exactly one element of A and 0 to all the other elements of X. These functions are precisely all the ∆ x for those elements x ∈ A. Since a : SX → X is a structure map for an S-algebra, it maps the function ∆ x into x. Therefore

Example 16. When S = Bool, we have that S is naturally isomorphic to P f , the finite powerset monad, whose algebras are idempotent commutative monoids or equivalently semilattices with a bottom element. So, for (X, a) ∈ EM(S), a ϕ ∈ SX such that x∈X ϕ(x) = 1 and supp ϕ ⊆ A is any finitely supported function from X to Bool that assigns 1 to at least one element of A. Intuitively, such a ϕ selects a non-empty finite subset of A, then a(ϕ) takes the join of all the selected elements. Table 2 . Then there exists a unique weak distributive law δ : SP → PS defined for all sets X and Φ ∈ SPX as:

The above δ, which is obtained by following the standard recipe of Proposition 7, is illustrated by the following example. and Φ(A) = 0 for all other sets A ⊆ X, so supp Φ = {A 1 , A 2 , A 3 }. In order to find an element ϕ ∈ δ X (Φ), we can first take a ψ ∈ S( X ) satisfying condition (a) in (6) and then compute the ϕ ∈ SX using condition (b). Among the ψ ∈ S( X ), consider for instance the following:

, we have that ψ satisfies condition (a) in (6) . Condition (b) forces ϕ to be the following:

. Table 2 , then the transformation δ given in (6) is actually a distributive law, and for S = N we recover the well-known δ of Example 11. Example 18 can be repeated with S = N: then Φ is the multiset where the set A 1 occurs five times, A 2 nine times and A 3 thirteen times. The elements of δ X (Φ) are all those multisets containing one element per copy of A 1 , A 2 and A 3 in supp Φ. The ϕ provided indeed contains five elements of A 1 (two copies of x and three of y), nine elements of A 2 (four copies of y and five of z), thirteen elements of A 3 (six copies of a and seven of b).

As Example 18 shows, each element ϕ of δ X (Φ) is determined by a function ψ choosing for each set A ∈ supp Φ a finite number of elements such that x A j = x B k (like y in Example 18), then x A j is mapped to s A j + s B k . Among those ψ's, there are some special, minimal ones as it were, that choose for each A in supp Φ exactly one element of A, and assign to it Φ(A). The induced ϕ in δ X (Φ) can be described as A∈u −1 {x} Φ(A) (equivalently S(u)(Φ) 1 ) where u : supp Φ → X is a function selecting an element of A for each A ∈ supp Φ (that is u(A) ∈ A). We denote the set of such ϕ's by c(Φ).

Example 20. Take X, A 1 and A 2 as in Example 18, but a different, smaller,

There are only four functions u : supp Φ → X such that u(A) ∈ A and thus only four functions ϕ in c(Φ):

Observe that the function ϕ = (x → 1, y → 1, z → 1) belongs to δ X (Φ) but not to c(Φ). Nevertheless ϕ can be retrieved as the convex combination 1 2 ·ϕ 1 + 1 2 ·ϕ 2 .

Our key result states that every ϕ ∈ δ X (Φ) can be written as a convex combination (performed in the S-algebra (SX, µ S X )) of functions in c(Φ), at least when S is a positive semifield, which by Remark 9 and Proposition 10 satisfies all the conditions that make (6) a weak distributive law. The proof is laborious and omitted here: we only remark that divisions in S play a crucial role in it.

Theorem 21. Let S be a positive semifield. Then for all sets X and Φ ∈ SPX

Remark 22. If we drop the hypothesis of semifield and only have the minimal assumptions of Theorem 17, then (8) does not hold any more: S = N is a counterexample. Indeed, in this case every subset of SX is convex with respect to µ S X (see Example 15), therefore we would have δ X (Φ) = c(Φ), which is false: the function ϕ of Example 18 is an example of an element in δ X (Φ) \ c(Φ).

Remark 23. When S = Bool (which is a positive semifield), the monad S coincides with the monad P f . The function c(·) in (7) can then be described as

for all A ∈ P f PX. It is worth remarking that this is the transformation χ appearing in Example 9 of [27] (which is in turn equivalent to the one in Example 2.4.7 of [31] ). This transformation was erroneously supposed to be a distributive law, as it fails to be natural (see [28] ). However, by taking its convex closure, as displayed in (8), one can turn it into a weak distributive law.

By exploiting the characterisation of the weak distributive law δ (Theorem 21), we can now describe the weak lifting of P to EM(S) generated by δ.

Recall from Definition 13 that P a c X is the set of convex subsets of X with respect to the S-algebra a : SX → X. The functions ι (X,a) : P a c X → PX and π (X,a) : PX → P a c X are defined for all A ∈ P a c X and B ∈ PX as

that is ι (X,a) is just the obvious set inclusion and π (X,a) performs the convex closure in a. The function α a : SP a c X → P a c X is defined for all Φ ∈ SP a c X as

To be completely formal, above we should have written c(S(ι)(Φ)) in place of c(Φ), but it is immediate to see that the two sets coincide. Proving that α a : SP a c X → P a c X is well defined (namely, α a (Φ) is a convex set) and forms an S-algebra requires some ingenuity and will be shown later in Section 5.1. The assignment (X, a) → (P a c X, α a ) gives rise to a functorP : EM(S) → EM(S) defined on morphisms f : (X, a) → (X , a ) as

for all A ∈ P a c X. For all (X, a) in EM(S), ηP (X,a) : (X, a) →P(X, a) and µP (X,a) :PP(X, a) →P(X, a) are defined for x ∈ X and A ∈ P αa c (P a c X) as

Theorem 24. Let S be a positive semifield. Then the canonical weak lifting of the powerset monad P to EM(S), determined by (8), consists of the monad (P, ηP , µP ) on EM(S) defined as in (10), (11) , (12) and the natural transformations ι : U SP → PU S and π : PU S → U SP defined as in (9).

It is worth spelling out the left-semimodule structure on P a c X corresponding to the S-algebra α a : SP a c X → P a c X. Let us start with λ· αa A for some A ∈ P a c X.

Following the definition of c(Φ) given in (7), one has to consider functions u : supp Φ → X such that u(B) ∈ B for all B ∈ supp Φ: if λ = 0, then supp Φ = {A} and thus, for each x ∈ A, there is exactly one function u x : supp Φ → X mapping A into x. It is immediate to see that S(u x )(Φ) is exactly the function (x → λ) and thus a(S(u x )(Φ)) is, by (5), λ· a x. Now if λ = 0, then supp Φ = ∅, so there is exactly one function u : supp Φ → X and S(u)(Φ) is the function mapping all x ∈ X into 0 and thus, by (5), a(S(u)(Φ)) = 0 a . Summarising,

Following similar lines of thoughts, one can check that

Remark 25. By comparing (14) and (13) with (4) and (5) in [25] , it is immediate to see that our monadP coincides with a slight variation of Jacobs's convex powerset monad C, the only difference being that we do allow for ∅ to be in P a c X. Jacobs insisted on the necessity of C(X) to be the set of non-empty convex subsets of X, because otherwise he was not able to define a semimodule structure on C(X) such that 0 · ∅ = {0 a }. However, we do manage to do so, since by (13) , 0 · A = 0 a for all A and in particular for A = ∅. At first sight, this may look like an ad-hoc solution, but this is not the case: it is intrinsic in the definition of the unique weak lifting of P to EM(S), as stated by Theorem 24 and shown next.

By Theorem 5, the weak distributive law (6) corresponds to a weak liftingP of P to EM(S), which we are going to show coincides with the data of (9)- (12) . The image alongP of a S-algebra (X, a) will be a set Y together with a structure map α a that makes it a S-algebra in turn. Garner [15, Proposition 13] gives us the recipe to build Y and α a appropriately. Y is obtained by splitting the following idempotent in Set:

as a composite e (X,a) = ι (X,a) • π (X,a) , where π (X,a) is the corestriction of e (X,a) to its image and ι (X,a) is the set-inclusion of the image of e (X,a) into PX. In other words, Y is the set of fixed points of e (X,a) . α a is obtained as the composite

Let us, then, fix an S-algebra (X, a). Given A ∈ PX, we have η S PX (A) = ∆ A : PX → S, the Dirac-function centred in A. The set δ X (η S PX (A)) has a simple description, shown in the next Lemma.

The image along A of the idempotent e is therefore

Hence the idempotent e computes the convex closure of elements of PX and its fixed points are precisely the convex subsets of X with respect to the structure map a. Therefore, the carrier set ofP(X, a) is precisely P a c X, the natural transformations π and ι are, respectively, the convex closure operator and the set-inclusion of P a c X into PX as in (9) . P a c X is then equipped with a structure map α a : SP a c X → P a c X given by

Let us try to calculate α a : given Φ : P a c X → S with finite support, we have that S(ι (X,a) )(Φ) is just the extension of Φ to PX which assigns 0 to each non-convex subset of X. If we write ι instead of ι (X,a) for short, we have

Next, we can use the following technical result.

Proposition 27. Let (X, a) be a S-algebra. If A is a convex subset of (SX, µ S X ), then Pa(A) is convex in (X, a).

Since δ X (Φ ) is the convex closure of c(Φ ) in (SX, µ S X ) for every Φ ∈ SPX, by Proposition 27 we can avoid to perform the a-convex closure in (16) . Therefore

In the next Proposition we show that also the µ S X -convex closure is superfluous, due to the fact that Φ ∈ SP a c X (and not simply SPX), thus obtaining (10). Proposition 28. Let S be a positive semifield, (X, a) a S-algebra, Φ ∈ SP a c X. Then Pa(δ X (S(ι)(Φ))) = Pa(c(S(ι)(Φ))).

Proof. In this proof we shall simply write Φ instead of the more verbose S(ι)(Φ). We want to prove that

where we have, by Theorem 21, that

First of all, ∅ is not a S-algebra, because there is no map S(∅) → ∅ given that S(∅) = {∅ : ∅ → S}, hence X = ∅. Next, if Φ = ε : PX → S, namely the function constant to 0, then c(Φ) = {ε : X → S} therefore one can easily see that the left-hand side of (17) is equal to {a(ε : X → S)}. For the same reason, the righthand side is also equal to {a(ε : X → S)}. Moreover, if Φ(∅) = 0, then there is no u : supp Φ → X such that u(∅) ∈ ∅, so c(Φ) = ∅ and so is the left-hand side of (17); for the same reason, also the right-hand side is empty. Suppose then, for the rest of the proof, that Φ = 0 and that Φ(∅) = 0. For the right-to-left inclusion in (17): given ψ ∈ c(Φ), consider Ψ = η S SX (ψ) = ∆ ψ ∈ S 2 X. Then Ψ clearly satisfies all the required properties and µ S X (Ψ ) = ψ. The left-to-right inclusion is more laborious. Let Ψ ∈ S 2 X be such that χ∈SX Ψ (χ) = 1 and such that supp Ψ ⊆ c(Φ), that is, for all ϕ ∈ supp Ψ there is u ϕ : supp Φ → X such that u ϕ (A) ∈ A for all A ∈ supp Φ and ϕ = S(u ϕ )(Φ). We have to show that a(µ(Ψ )) = a(ψ) for some ψ ∈ SX of the form A∈supp Φ Φ(A) · u(A) for some choice function u : supp Φ → X. Notice that the given Ψ is a convex linear combination of functions ϕ's in SX like the one we have to produce: the trick will be to exploit the fact that each A ∈ supp Φ is convex. Here we shall only give a sketch of the proof. Suppose supp Φ = {A 1 , . . . , A n } and supp Ψ = {ϕ 1 , . . . , ϕ m }. Call u j the choice function that generates ϕ j . Then Ψ is of this form:

Define the following element of S 2 X:

Observe that u 1 (A i ), . . . , u m (A i ) ∈ A i by definition, and A i is convex by assumption: since m j=1 Ψ (ϕ j ) = 1, we have that a(χ i ) ∈ A i . Set then u(A i ) = a(χ i ) and define ψ = S(a)(Ψ ): we have ψ ∈ c(Φ) with u as the generating choice function. It is not difficult to see that µ S X (Ψ ) = µ S X (Ψ ), therefore we have

as desired.

The rest of the proof of Theorem 24, concerning the action ofP on morphisms and the unit and multiplication of the monadP, consists in following the recipe provided by Garner [15] .

We can now compose the two monads P and S by considering the monad arising from the composition of the following two adjunctions:

Direct calculations show that the resulting endofunctor on Set, which we call P c S, maps a set X and a function f : X → Y into, respectively,

for all A ∈ P c SX. For all sets X, η PcS X : X → P c SX and µ PcS X : P c SP c SX → P c SX are defined as

for all x ∈ X and A ∈ P c SP c SX.

Theorem 29. Let S be a positive semifield. Then the canonical weak distributive law δ : SP → PS given in Theorem 21 induces a monad P c S on Set with endofunctor, unit and multiplication defined as in (18) and (19) .

Recall from Remark 25 that the monad C : EM(S) → EM(S) from [25] coincides with our liftingP modulo the absence of the empty set. The same happens for the composite monad, which is named CM in [25] . The absence of ∅ in CM turns out to be rather problematic for Jacobs. Indeed, in order to use the standard framework of coalgebraic trace semantics [20] , one would need the Kleisli category Kl(CM) to be enriched over CPPO, the category of ω-complete partial orders with bottom and continuous functions. Kl(CM) is not CPPO-enriched since there is no bottom element in CM(X). Instead, in P c SX the bottom is exactly the empty set; moreover, Kl(P c S) enjoys the properties required by [20] .

Theorem 30. The category Kl(P c S) is enriched over CPPO and satisfies the left-strictness condition: for all f : X → P c SY and Z set,

It is immediate that every homset in Kl(P c S) carries a complete partial order. Showing that composition of arrows in Kl(P c S) preserves joins (of ω-chains) requires more work: the proof, omitted here, crucially relies on the algebraic theory presenting the monad P c S, illustrated next.

An Algebraic Presentation. Recall that an algebraic theory is a pair T = (Σ, E) where Σ is a signature, whose elements are called operations, to each of which is assigned a cardinal number called its arity, while E is a class of formal equations between Σ-terms. An algebra for the theory T is a set where Σ SLSM = {+, 0} ∪ {λ · | λ ∈ S} and E LSM is the set of axioms in Table 1 . As already mentioned in Section 3, left S-semimodules are exactly Salgebras and morphisms of S-semimodules coincide with those of S-algebras. Thus, the theory LSM presents the monad S.

Similarly, semilattices are algebras for the theory SL = (Σ SL , E SL ) where Σ SL = { , ⊥} and E SL is the set of axioms in Table 1 . It is well known that semilattices are algebras for the finite powerset monad. Actually, this monad is presented by SL. In order to present the full powerset monad P we need to take joins of arbitrary arity. A complete semilattice is a set X equipped with joins x∈A x for all-not necessarily finite-A ⊆ X. Formally the (infinitary) theory of complete semilattices is given as CSL = (Σ CSL , E CSL ) where Σ CSL = { I | I set} and E CSL is the set of axioms displayed in Table 3 (for a detailed treatment of infinitary algebraic theories see, for example, [30] ).

We can now illustrate the theory (Σ, E) presenting the composed monad P c S: the operations in Σ are exactly those of complete semilattices and S- Table 3 . The sets of axioms ECSL for complete semilattices: the second axiom generalises the usual idempotency and commutativity properties of finitary , while the third one generalises associativity and neutrality of ∅ = ⊥. i∈{0} xi = x0 j∈J xj = i∈I x f (i) for all f : I → J surjective i∈I xi = j∈J i∈f −1 {j} xi for all f : I → J semimodules, while the axioms are those of complete semilattices and S-semimodules together with the set E D of distributivity axioms illustrated below.

In short,

Theorem 32. The monad P c S is presented by the algebraic theory (Σ, E).

The presentation crucially relies on the fact that P c S is obtained by composing P and S via δ. Indeed, we know from general results in [11, 15] that P c Salgebras are in one to one correspondence with δ-algebras [3] , namely triples (X, a, b) such that a : SX → X is a S-algebra, b : PX → X is a P-algebra and the following diagram commutes.

SX PX

The S-algebra a corresponds to a S-semimodule (X, +, 0, λ·), the P-algebra b to a complete lattice (X, I ) and the commutativity of diagram (21) expresses exactly the distributivity axioms in (20) .

: P c SP c S1 → P c S1 induces a δ-algebra where the structure of complete lattice is given as 2

The R + -semimodule is as expected, e.g.,

Finite Joins and Finitely Generated Convex Sets. We now consider the algebraic theory (Σ , E ) obtained by restricting (Σ, E) to finitary joins. More precisely, we fix

is the algebraic theory for semilatices, (Σ LSM , E LSM ) is the one for S-semimodules, and E D is the set of distributivity axioms illustrated in Table 1 . Thanks to the characterisation provided by Theorem 32, we easily obtain a function translating Σ -terms into convex subsets.

Proposition 34. Let T Σ ,E (X) be the set of Σ -terms with variables in X quotiented by E . Let [[·]] X : T Σ ,E (X) → P c S(X) be the function defined as 

We say that a set A ∈ P c S(X) is finitely generated if there exists a finite set B ⊆ S(X) such that B = A. We write P f c S(X) for the set of all A ∈ P c S(X) that are finitely generated. The assignment X → P f c S(X) gives rise to a monad P f c S : Set → Set where the action on functions, the unit and the multiplication are defined as for P c S.

Theorem 35. The monads T Σ ,E and P f c S are isomorphic. Therefore (Σ , E ) is a presentation for the monad P f c S.

Example 36. Recall P c S(1) for S = R + from Example 33. By restricting to the finitely generated convex sets, one obtains P f c S(1) = {∅} ∪ {[a, b] | a, b ∈ R + }, that is the sets of the form [a, ∞) are not finitely generated. Table 4 illustrates the isomorphism [[·]] : T Σ ,E (1) → P c S(1). It is worth observing that every closed interval [a, b] is denoted by a term in T Σ ,E (1)

is the set containing all convex polygons: for instance the term (r 1 · x + s 1 · y) (r 2 · x + s 2 · y) (r 3 · x + s 3 · y) denote a triangle with vertexes (r i , s i ). For n = {x 0 , . . . x n−1 }, it is easy to see that P f c S(n) contains all convex n-polytopes.

Our work was inspired by [17] where Goy and Petrisan compose the monads of powerset and probability distributions by means of a weak distributive law in the sense of Garner [15] . Our results also heavily rely on the work of Clementino [12] that illustrates necessary and sufficient conditions on a semiring S for the existence of a weak distributive law δ : SP → PS. However, to the best of our knowledge, the alternative characterisation of δ provided by Theorem 21 was never shown.

Such characterisation is essential for giving a handy description of the lifting P : EM(S) → EM(S) (Theorem 24) as well as to observe the strong relationships with the work of Jacobs (Remark 25) and the one of Klin and Rot (Remark 23). The weak distributive law δ also plays a key role in providing the algebraic theories presenting the composed monad P c S (Theorem 24) and its finitary restriction P f c S (Theorem 35). These two theories resemble those appearing in, respectively, [17] and [10] where the monad of probability distributions plays the role of the monad S in our work.

Theorem 30 allows to reuse the framework of coalgebraic trace semantics [20] for modelling over Kl(P c S) systems with both nondeterminism and quantitative features. The alternative framework based on coalgebras over EM(P c S) directly leads to nondeterministic weighted automata. A proper comparison with those in [13] is left as future work. Thanks to the abstract results in [7] , language equivalence for such coalgebras could be checked by means of coinductive upto techniques. It is worth remarking that, since δ is a weak distributive law, then thanks to the work in [16] , up-to techniques are also sound for "convexbisimilarity" (in coalgebraic terms, behavioural equivalence for the lifted functor P : EM(S) → EM(S)).

We conclude by recalling that we have two main examples of positive semifields: Bool and R + . Booleans could lead to a coalgebraic modal logic and trace semantics for alternating automata in the style of [27] . For R + , we hope that exploiting the ideas in [34] our monad could shed some lights on the behaviour of linear dynamical systems featuring some sort of nondeterminism.

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Coalgebra learning via duality

Relational algebras

Distributive laws

A coalgebraic perspective on linear weighted automata

Sound up-to techniques and complete abstract domains

Up-to techniques for behavioural metrics via fibrations

Coinduction up-to in a fibrational setting

Hacking nondeterminism with induction and coinduction

Combining Semilattices and Semimodules

The theory of traces for systems with nondeterminism and probability

The weak theory of monads

The monads of classical algebra are seldom weakly cartesian

Handbook of weighted automata

Up-to techniques for branching bisimilarity

The Vietoris Monad and Weak Distributive Laws

Combining weak distributive laws: Application to up-to techniques

Combining probabilistic and non-deterministic choice via weak distributive laws

Monoid-labeled transition systems

Generic weakest precondition semantics from monads enriched with order

Generic trace semantics via coinduction

Lattice-theoretic progress measures and coalgebraic model checking

Learning weighted automata over principal ideal domains

A category theoretic formulation for engeler-style models of the untyped lambda

Combining effects: Sum and tensor

Coalgebraic Trace Semantics for Combined Possibilitistic and Probabilistic Systems

Bialgebras for structural operational semantics: An introduction

Coalgebraic trace semantics via forgetful logics

Iterated covariant powerset is not a monad

Algebraic Theories

Monad compositions I: General constructions and recursive distributive laws. Theory and Applications of Categories [electronic only

Notions of computation and monads

Automata and coinduction (an exercise in coalgebra)

A tutorial on coinductive stream calculus and signal flow graphs

Generalizing determinization from automata to coalgebras

Guarded kleene algebra with tests: verification of uninterpreted programs in nearly linear time

Weak Distributive Laws

Towards a mathematical operational semantics

Distributing probability over nondeterminism

No-Go Theorems for Distributive Laws