Cancellative Convex Semilattices

Sokolova, Ana; Woracek, Harald

doi:10.4230/LIPIcs.CALCO.2025.12

Cancellative Convex Semilattices

Ana Sokolova

University of Salzburg, Austria Harald Woracek

TU Wien, Austria

Abstract

Convex semilattices are algebras that are at the same time a convex algebra and a semilattice, together with a distributivity axiom. These algebras have attracted some attention in the last years as suitable algebras for probability and nondeterminism, in particular by being the Eilenberg-Moore algebras of the nonempty finitely-generated convex subsets of the distributions monad.

A convex semilattice is cancellative if the underlying convex algebra is cancellative. Cancellative convex algebras have been characterized by M. H. Stone and by H. Kneser: A convex algebra is cancellative if and only if it is isomorphic to a convex subset of a vector space (with canonical convex algebra operations).

We prove an analogous theorem for convex semilattices: A convex semilattice is cancellative if and only if it is isomorphic to a convex subset of a Riesz space, i.e., a lattice-ordered vector space (with canonical convex semilattice operations).

Keywords and phrases:

convex semilattice, cancellativity, Riesz space

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Randomness, geometry and discrete structures ; Theory of computation

\rightarrow

Logic and verification ; Theory of computation

\rightarrow

Probabilistic computation

DOI:

10.4230/LIPIcs.CALCO.2025.12

Event:

11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Editors:

Corina Cîrstea and Alexander Knapp

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Models of computation exhibiting both nondeterministic and probabilistic behaviour have been studied for decades and are prominent in verification [33, 14, 2, 15, 24, 8, 43, 13, 34], AI [6, 21, 32], as well as in semantics [17, 37, 16]. Probabilities quantitatively model uncertainty and belief, whereas nondeterminism represents incomplete information, unknown environment, implementation freedom, or concurrency.

Algebras play an important role in the analysis of software and systems. In terms of categorical algebra, the combination of probability and nondeterminism has been problematic, in the sense that there is no distributive law of probability over nondeterminism [42, 22, 26, 19, 41, 29, 11, 40, 30]. However, the relevant algebraic structures have been identified already some time ago in the above mentioned works and have attracted additional attention recently [3, 4, 5, 12, 31]. Convex semilattices, as coined in [3], are such relevant algebraic structures. They are closely connected to the finitely-generated-convex-sets-of-probability-distributions monad [29, 11, 40, 41, 42, 19, 12, 28]: they are its Eilenberg-Moore algebras as shown in [3, 4, 5]. Convex semilattices also play a role in extending probability and nondeterminism to metric spaces and quantitative equational theories [28, 27], in semantics for higher-order languages that combine probabilistic and nondeterministic choice [1], as well as in recent work on deductive verification [44]. In the pure mathematical context of universal algebra, convex semilattices have appeared as certain semilattices with operators e.g. in [18], or as certain modals e.g. in [35].

A convex semilattice is an algebra that is a convex algebra and a semilattice at the same time, including a suitable distributivity axiom of probabilistic choice (the convex algebra operations) over nondeterminism (the semilattice operation). A convex algebra is cancellative, if each of the convex operations, that can be understood as biased coins, is cancellative. We call a convex semilattice cancellative if the underlying convex algebra is cancellative.

Cancellative convex algebras have been characterized by M. H. Stone in 1949 [38] and a few years later in 1952 [23] independently by H. Kneser: A convex algebra is cancellative if and only if it is isomorphic to a convex subset of a vector space (with canonical convex algebra operations).

In this paper, we prove an analogous theorem for convex semilattices: A convex semilattice is cancellative if and only if it is isomorphic to a convex subset of a Riesz space, which is a lattice-ordered vector space (with canonical convex semilattice operations). Interestingly, no assumption involving the semilattice operation is needed to ensure embeddability.

The paper has a simple structure: In Section 2, we present the necessary background and the main result. In Section 3 we prove our result in a sequence of steps, discussing the main ideas and tools as well as all details. The development is elementary, with extensive use of an important geometric intuition of perspective shift that we have already prominently employed in [36]. We wrap up with a short discussion in Section 4.

2 Background and main result

Our main result is that cancellative convex semilattices (cf. Definition 4) can always be embedded homomorphically into a Riesz space (cf. Example 5). This result is formulated in Theorem 6 below, and is an analogue in the variety of convex semilattices of a classical theorem about convex algebras. To set the scene, we discuss the classical theorem first.

Revisiting convex algebras

Abstractly, convex algebras (also known as convex sets, barycentric algebras, convex spaces, see e.g. [36] for details on related work) are the Eilenberg-Moore algebras of the finitely-supported probability distribution monad [39, 9, 10, 20]. Concretely, they have been studied for decades in various contexts within algebra and convex geometry. They are algebras with a family of “biased-coin” binary operations, used for modeling probabilistic choice. We start with recalling their definition.

Definition 1.

A convex algebra $\mathbb{X}$ is a set $X$ together with a family of binary operations $+_{p}$ , $p\in(0,1)$ , which satisfy

$\blacksquare$

idempotence: ${\displaystyle{\forall x\in X,p\in(0,1){\mathop{:}\kern 5.0pt}x+_{p}x=x}}$ ,
$\blacksquare$

parametric commutativity: ${\displaystyle{\forall x,y\in X,p\in(0,1){\mathop{:}\kern 5.0pt}x+_{p}y=y+_{1-% p}x}}$ ,
$\blacksquare$

parametric associativity:

$\forall x,y,z\in X,p,q\in(0,1){\mathop{:}\kern 5.0pt}(x+_{p}y)+_{q}z=x+_{pq}% \big{(}y+_{\frac{(1-p)q}{1-pq}}z\big{)}.$

A convex algebra is called cancellative, if it satisfies

$\blacksquare$

${\displaystyle{\forall x,y,z\in X,p\in(0,1){\mathop{:}\kern 5.0pt}\big{(}x+_{p% }z=y+_{p}z\Rightarrow x=y\big{)}}}$ .

If it is necessary to make the operations of a convex algebra notationally explicit, we write $\mathbb{X}=\langle X,+_{p}\rangle$ .

It is often practical to extend the set of operations on a convex algebra $\mathbb{X}=\langle X,+_{p}\rangle$ by defining

x+_{1}y\mathrel{\mathop{:}}=x,\quad x+_{0}y\mathrel{\mathop{:}}=y\qquad\text{% for }x,y\in X.

Then the laws of idempotence, parametric commutativity, and parametric associativity hold even for $p,q\in[0,1]$ .

Examples of cancellative convex algebras are obtained from linear algebra.

Example 2.

Let $V$ be a vector space over the scalar field $\mathbb{R}$ . A subset $Y$ of $V$ is called convex, if

$\blacksquare$

${\displaystyle{\forall x,y\in Y,p\in(0,1){\mathop{:}\kern 5.0pt}p\cdot x+(1-p)% \cdot y\in Y}}$ .

Let $Y$ be a convex subset of $V$ , and define binary operations $+_{p}$ on $Y$ as

x+_{p}y\mathrel{\mathop{:}}=p\cdot x+(1-p)\cdot y\qquad\text{for }x,y\in Y,p% \in(0,1).

(1)

Then $\mathbb{Y}\mathrel{\mathop{:}}=\langle Y,+_{p}\rangle$ is a cancellative convex algebra.

M. H. Stone [38] and H. Kneser [23] proved that every cancellative convex algebra (in Stone’s terminology “barycentric algebra” and in Kneser’s terminology “konvexer Raum”) is of that form. We remark that both authors work with arbitrary ordered skew fields in place of $\mathbb{R}$ .

Theorem 3 (Stone-Kneser).

Let $\mathbb{X}$ be a cancellative convex algebra. Then there exists a vector space $V$ over $\mathbb{R}$ and a convex subset $Y$ of $V$ , such that $\mathbb{X}$ is isomorphic to $\mathbb{Y}$ (meaning the set $Y$ made into a convex algebra as in Example 2).

Cancellative convex semilattices

In our presentation we interchangeably work with the “algebraic” and the “order theoretic” viewpoint on semilattices. That is:

1.

Algebraically, a semilattice is a set $X$ together with a binary operation $\oplus$ that is idempotent, commutative, and associative, i.e., the axioms

$x\oplus x=x,\qquad x\oplus y=y\oplus x,\qquad x\oplus(y\oplus z)=(x\oplus y)\oplus z$

hold for all $x,y\in X$ .
2.

Order-theoretically, a semilattice is a set $X$ together with a partial order in which each two elements have a supremum.

The connection between these viewpoints (going both ways) is given by

x\leq y\mathrel{\mathop{:}}\Leftrightarrow x\oplus y=y,\qquad x\oplus y% \mathrel{\mathop{:}}=\sup\{x,y\}.

(2)

Definition 4.

A convex semilattice $\mathbb{X}$ is a set $X$ together with a family of binary operations $+_{p}$ , $p\in(0,1)$ , and another binary operation $\oplus$ , such that

$\blacksquare$

$\langle X,+_{p}\rangle$ is a convex algebra,
$\blacksquare$

$\langle X,\oplus\rangle$ is a semilattice,
$\blacksquare$

the following distributivity law holds:

$\forall x,y,z\in X,p\in(0,1){\mathop{:}\kern 5.0pt}(x\oplus y)+_{p}z=(x+_{p}z)% \oplus(y+_{p}z).$

We call a convex semilattice cancellative, if the convex algebra $\langle X,+_{p}\rangle$ is cancellative.

If it is necessary to make the operations of a convex semilattice notationally explicit, we write $\mathbb{X}=\langle X,+_{p},\oplus\rangle$ .

Again examples of cancellative convex semilattices stem from linear algebra.

Example 5.

An ordered vector space is a vector space $V$ over $\mathbb{R}$ together with a partial order $\leq$ , such that

$\blacksquare$

${\displaystyle{\forall x,y,z\in V{\mathop{:}\kern 5.0pt}\big{(}x\leq y% \Rightarrow x+z\leq y+z\big{)}}}$ ,
$\blacksquare$

${\displaystyle{\forall x\in V,q>0{\mathop{:}\kern 5.0pt}\big{(}0\leq x% \Rightarrow 0\leq q\cdot x\big{)}}}$ .

An ordered vector space is called a Riesz space, if its order is a lattice order, i.e., each two elements have a supremum and an infimum.

Let $V$ be a Riesz space, and let $Y$ be a convex subset of $V$ that is closed under binary suprema. Define binary operations $+_{p}$ and $\oplus$ on $Y$ as

x+_{p}y\mathrel{\mathop{:}}=p\cdot x+(1-p)\cdot y\qquad\text{for }x,y\in V,p% \in(0,1),

x\oplus y\mathrel{\mathop{:}}=\sup\{x,y\}\qquad\text{for }x,y\in V.

Then $\mathbb{Y}\mathrel{\mathop{:}}=\langle Y,+_{p},\oplus\rangle$ is a cancellative convex semilattice, and we refer to $\mathbb{Y}$ as the convex semilattice induced by $V$ on $Y$ .

Riesz spaces go back to the work of F. Riesz, L. V. Kantorovich, G. Birkhoff and others. There is a vast literature, we refer to [7, 25].

We are going to prove the following theorem.

Theorem 6.

Let $\mathbb{X}$ be a cancellative convex semilattice. Then there exists a Riesz space $V$ and a convex subset $Y$ of $V$ that is closed under binary suprema, such that $\mathbb{X}$ is isomorphic to the convex semilattice induced by $V$ on $Y$ .

$\blacktriangleright$ Remark 7.

It may seem unnatural that we start in Example 5 from a vector space ordered with a lattice order instead of requiring only existence of suprema as for convex semilattices. However, this is just a matter of taste, as:

1.

In every Riesz space $V$ the following law holds:

$\forall x,y\in V{\mathop{:}\kern 5.0pt}\inf\{x,y\}=-\sup\{-x,-y\}.$ (3)
2.

If $V$ is a convex semilattice whose underlying convex algebra is a vector space, we can use Equation 3 as a definition and in this way obtain a Riesz space (for the sake of completeness a proof of this statement is given in Lemma 15 below).

We decided to start with a Riesz space in our presentation, since it is a classical concept and a large amount of theory on Riesz spaces is available.

$\blacktriangleright$ Remark 8.

Among other algebraic structures, in [22] also ordered barycentric algebras are studied (see Definition 2.6 in that paper). These are convex algebras that are additionally endowed with an order relation such that the convex operations are monotone (they do not form an equational class of algebras). As usual, examples are obtained from linear algebra: every convex subset of an ordered vector space is an ordered barycentric algebra. Note that every convex semilattices in the sense of Definition 4 is in particular also an ordered barycentric algebra.

In [22, Remarks 2.9] it is stated (without explicit proof) that an ordered barycentric algebra can be embedded into an ordered vector space, if and only if the following order cancellation axiom holds:

\forall x,y,z\in X,p\in(0,1){\mathop{:}\kern 5.0pt}\big{(}x+_{p}z\leq y+_{p}z% \Rightarrow x\leq y\big{)}.

(4)

Apparently, Equation 4 implies that the underlying convex algebra is cancellative.

Theorem 6 above now shows that, if suprema exist, no assumption on the order is needed to guarantee embeddability into an ordered vector space (even a Riesz space).

3 Ideas, tools, construction, proof

In this section we prove Theorem 6. The argument involves one geometric notion (Subsection 3.1) and one rather general construction (Subsection 3.2) that together lead to the theorem.

Note already in the start, that the case when $X=\emptyset$ is trivial. Hence, from now on we assume that $X\neq\emptyset$ . We can assume without loss of generality that $X$ is a convex subset of some vector space $V$ and that the operations $+_{p}$ of $X$ are inherited from $V$ as in Equation 1. This holds since we can embed $\langle X,+_{p}\rangle$ into some vector space by the Stone-Kneser theorem. Moreover, we may assume that $0\in X$ . This holds since we can make a translation to force that $X$ contains $0$ . Note here that translations in a vector space are isomorphisms with respect to the convex algebra structure.

Our plan is to extend the semilattice operation from $X$ to some linear subspace $W$ of $V$ in such a way that $W$ becomes a convex semilattice, and then use Remark 7.2. to view this as a Riesz space.

3.1 Perspective shift

We start with the notion of perspective shift, that we will extensively use throughout the proof.

Definition 9.

Let $V$ be a vector space over $\mathbb{R}$ . Then we denote

P\colon\left\{\begin{array}[]{rcl}V\times\mathbb{R}\times V&\to&V\\ (c,p,x)&\mapsto&px+(1-p)c\end{array}\right.

We think of $P$ as a perspective shift with center at $c$ and ratio $p$ :

This function played an essential role in [36], where it was considered on $\mathbb{R}^{n}$ (and was denoted as $\Phi_{z}(s,x)\mathrel{\mathop{:}}=P(z,1-s,x)$ ).

Clearly, when $V$ is considered as a convex algebra in the canonical way, $P(c,p,x)=x+_{p}c$ . The next several lemmas gather some properties of perspective shifts that we will need in the sequel.

Lemma 10.

Let $V$ be a vector space over $\mathbb{R}$ . Then the following properties hold:

1.

${\displaystyle{\forall c,x\in V{\mathop{:}\kern 5.0pt}P(c,0,x)=c\text{ and }P(% c,1,x)=x}}$ ,
2.

${\displaystyle{\forall c\in V,p,q\in\mathbb{R}{\mathop{:}\kern 5.0pt}P(c,p,% \text{\_\kern 1.0pt})\circ P(c,q,\text{\_\kern 1.0pt})=P(c,pq,\text{\_\kern 1.% 0pt})}}$ ,
3.

Let $c,d\in V$ and $p,q\in\mathbb{R}$ with $(1-p)(1-q)\neq 1$ , and set

$s\mathrel{\mathop{:}}=\frac{p}{p+q-pq},\quad r\mathrel{\mathop{:}}=\frac{q}{p+% q-pq}.$ (5)

Then

$P(d,r,\text{\_\kern 1.0pt})\circ P(c,p,\text{\_\kern 1.0pt})=P(c,s,\text{\_% \kern 1.0pt})\circ P(d,q,\text{\_\kern 1.0pt}).$ (6)

Proof.

The proof is carried out by simple computation.

1.

$P(c,0,x)=0x+1c=c$ , $P(c,1,x)=1x+0c=x$ .
2.

We have

$\displaystyle P\big{(}c,p,P(c,q,x)\big{)}=$ $\displaystyle\,p\big{[}qx+(1-q)c\big{]}+(1-p)c$

$\displaystyle=$ $\displaystyle\,pq\cdot x+\big{(}\underbrace{p(1-q)+(1-p)}_{1-pq}\big{)}\cdot c% =P(c,pq,x).$

3.

The assumption that $(1-p)(1-q)\neq 1$ just says that the denominator in the definition of $r, s$ is nonzero. We compute

	$\displaystyle P\big{(}d,r,P(c,p,x)\big{)}=$	$\displaystyle\,r\big{[}px+(1-p)c\big{]}+(1-r)d=$
	$\displaystyle=$	$\displaystyle\,rp\cdot x+r(1-p)\cdot c+(1-r)\cdot d,$
	$\displaystyle P\big{(}c,s,P(d,q,x)\big{)}=$	$\displaystyle\,s\big{[}qx+(1-q)d\big{]}+(1-s)c=$
	$\displaystyle=$	$\displaystyle\,sq\cdot x+(1-s)\cdot c+s(1-q)\cdot d.$

Plugging the definitions of $s, r$ yields

	$\displaystyle rp=\frac{qp}{p+q-pq}=sq,$
	$\displaystyle r(1-p)=\frac{q-pq}{p+q-pq}=1-\frac{p}{p+q-pq}=1-s,$
	$\displaystyle 1-r=1-\frac{q}{p+q-pq}=\frac{p-pq}{p+q-pq}=s(1-q).\$

$\hfill\blacktriangleleft$

As a consequence from Lemma 10, we immediately see that $P(c,p,\text{\_\kern 1.0pt})$ is bijective with $P(c,p,\text{\_\kern 1.0pt})^{-1}=P(c,\frac{1}{p},\text{\_\kern 1.0pt})$ for all $c\in V$ and $p\in\mathbb{R},p\neq 0$ .

We need one more property, a kind of associativity of perspectives.

Lemma 11.

Let $V$ be a vector space over $\mathbb{R}$ . Let $p,q,r,s\in\mathbb{R}$ be a solution of the system of equations

		$\displaystyle qp=s$		(7)
		$\displaystyle q(1-p)=(1-s)(1-r)$		(8)
		$\displaystyle 1-q=(1-s)r$		(9)

Then

\forall c,d,x\in V{\mathop{:}\kern 5.0pt}P\big{(}d,q,P(c,p,x)\big{)}=P\big{(}P% (c,r,d),s,x\big{)}

Proof.

We compute

	$\displaystyle P\big{(}d,q,P(c,p,x)\big{)}=$	$\displaystyle\,q\big{[}px+(1-p)c\big{]}+(1-q)d$
	$\displaystyle=$	$\displaystyle\,qp\cdot x+q(1-p)\cdot c+(1-q)\cdot d,$
	$\displaystyle P\big{(}P(c,r,d),s,x\big{)}=$	$\displaystyle\,sx+(1-s)\big{[}rd+(1-r)c\big{]}$
	$\displaystyle=$	$\displaystyle\,s\cdot x+(1-s)(1-r)\cdot c+(1-s)r\cdot d.\$

$\hfill\blacktriangleleft$

$\blacktriangleright$ Remark 12.

1.

Any two of the three equations Equation 7–Equation 9 implies the third.
2.
The system Equation 7–Equation 9 can be solved for different variables. We use:
- $\blacksquare$
  
  Given $p,q\in\mathbb{R}$ with $pq\neq 1$ , set
  
  $s\mathrel{\mathop{:}}=qp,\quad r\mathrel{\mathop{:}}=\frac{1-q}{1-qp}.$
  
  Then $p, q, r, s$ satisfy Equation 7–Equation 9.
- $\blacksquare$
  
  Given $p,r\in\mathbb{R}$ with $pr\neq 1$ , set
  
  $q\mathrel{\mathop{:}}=\frac{1-r}{1-pr},\quad s\mathrel{\mathop{:}}=p\frac{1-r}% {1-pr}.$
  
  Then $p, q, r, s$ satisfy Equation 7–Equation 9.
3.

If in the previous item $p,q\in(0,1)$ (or $p,r\in(0,1)$ ), then also $r,s\in(0,1)$ (or $q,s\in(0,1)$ , respectively).

We end this tools-section with one more observation about perspective shift.

Lemma 13.

Let $X$ be a convex semilattice that is a convex subset of a vector space $V$ . Let $c\in X$ and $p\in[0,1]$ . Then the perspective shift $P(c,p,\text{\_\kern 1.0pt})|_{X}$ is a convex semilattice homomorphism.

Proof.

Let $x,y\in X$ . Then

$\displaystyle P(c,p,x)+_{q}P(c,p,y)$	$\displaystyle=$	$\displaystyle(x+_{p}c)+_{q}(y+_{p}c)$
	$\displaystyle=$	$\displaystyle q(px+(1-p)c)+(1-q)(py+(1-p)c)$
	$\displaystyle=$	$\displaystyle p(qx+(1-q)y)+(1-p)c$
	$\displaystyle=$	$\displaystyle(x+_{q}y)+_{p}c$
	$\displaystyle=$	$\displaystyle P(c,p,x+_{q}y)$

for any $q\in[0,1]$ and, using distributivity,

$\displaystyle P(c,p,x)\oplus P(c,p,y)$	$\displaystyle=$	$\displaystyle(x+_{p}c)\oplus(y+_{p}c)$
	$\displaystyle=$	$\displaystyle(x\oplus y)+_{p}c$
	$\displaystyle=$	$\displaystyle P(c,p,x\oplus y).$

$\hfill\blacktriangleleft$

Of course, for arbitrary $c\in V$ and $p\in\mathbb{R}$ , the perspective shift $P(c,p,\text{\_\kern 1.0pt})$ is a linear map on $V$ , and therefore a convex algebra homomorphism on $V$ . We will also use this fact later.

3.2 Constructing the needed space

We establish the following assertion, whose proof gives a construction of the space that we are looking for.

Proposition 14.

Let $V$ be a vector space over $\mathbb{R}$ and let $X$ be a convex subset of $V$ with $0\in X$ . Assume that we have a binary operation $\oplus$ on $X$ , such that $\langle X,+_{p},\oplus\rangle$ is a convex semilattice (as usual $+_{p}$ is inherited from $V$ as in Equation 1). Then there exists a linear subspace $W$ of $V$ with $X\subseteq W$ , and a binary operation $\boxplus$ on $W$ , such that $\langle W,+_{p},\boxplus\rangle$ (again $+_{p}$ as in Equation 1) is a convex semilattice and $\boxplus|_{X\times X}=\oplus$ .

Proof.

Our candidate for the subspace $W$ is

W\mathrel{\mathop{:}}=\big{\{}x\in V\mid\mkern 3.0mu\exists c\in X,p\in(0,1]{% \mathop{:}\kern 5.0pt}P(c,p,x)\in X\big{\}}.

The main idea is that we can define convex semilatttice operations on $W$ as shown in the following picture

The fact that $X\subseteq W$ is clear: given $x\in X$ just use $c=x$ and $p=1$ .

We structure the proof of the required properties in five steps. Steps ➀ and ➁ are preparatory, in Step ➂ we show that $W$ is a linear subspace, in Step ➃ we define $\boxplus$ , and in Step ➄ we prove that $W$ becomes a convex semilattice.

Step ➀.

Let $x\in W$ and let $c\in X,p\in(0,1]$ be such that $P(c,p,x)\in X$ . Set

p(x)\mathrel{\mathop{:}}=\sup\big{\{}p\in(0,1]\mid\mkern 3.0muP(c,p,x)\in X% \big{\}}.

We show that $P(c,q,x)\in X$ for all $q\in(0,p(x))$ . To see this, assume $q\in(0,p(x))$ , and choose $p\in[q,p(x)]$ with $P(c,p,x)\in X$ . Then $\frac{q}{p}\in[0,1]$ , and hence, by Lemma 10.2.,

P(c,q,x)=P\Big{(}c,\frac{q}{p},P(c,p,x)\Big{)}\in X.

Step ➁.

Let $x_{1},\ldots,x_{n}\in W$ . We show that there exists $c\in X,p\in(0,1]$ , such that $P(c,p,x_{i})\in X$ for all $i\in\{1,\ldots,n\}$ .

To start with, consider $x\in W$ , let $c\in X,p\in(0,1]$ with $P(c,p,x)\in X$ , and let $d\in X,r\in(0,1)$ . Then, by Lemma 11 and Remark 12.2., we have

P\Big{(}P(c,r,d),\underbrace{p\frac{1-r}{1-pr}}_{\in(0,1]},x\Big{)}=P\Big{(}d,% \underbrace{\frac{1-r}{1-pr}}_{\in(0,1]}P(c,p,x)\Big{)}\in X.

(10)

Now consider $x_{1},\ldots,x_{n}\in W$ . Choose $c_{i}\in X,p_{i}\in(0,1]$ with $P(c_{i},p_{i},x_{i})\in X$ . Set

c\mathrel{\mathop{:}}=\sum_{i=1}^{n}\frac{1}{n}c_{i},

then $c\in X$ as $X$ is a convex algebra and hence it is also closed under arbitrary convex combinations. We have

c=P\Big{(}c_{i},\frac{n-1}{n},\sum_{\begin{subarray}{c}j=1\\ j\neq i\end{subarray}}^{n}\frac{1}{n-1}c_{j}\Big{)},

and by Equation 10 thus

P\Big{(}c,p_{i}\frac{1-\frac{n-1}{n}}{1-p_{i}\frac{n-1}{n}},x_{i}\Big{)}=P\Big% {(}\sum_{\begin{subarray}{c}j=1\\ j\neq i\end{subarray}}^{n}\frac{1}{n-1}c_{j},\frac{1-\frac{n-1}{n}}{1-p_{i}% \frac{n-1}{n}},P(c_{i},p_{i},x_{i})\Big{)}\in X.

Now choose $p$ with $0<p<\min\limits_{i\in\{1,\ldots,n\}}p_{i}\frac{1-\frac{n-1}{n}}{1-p_{i}\frac{n% -1}{n}}$ and use Step ➀: it follows that indeed $P(c,p,x_{i})\in X$ .

Step ➂.

We show that $W$ is a linear subspace of $V$ and contains $X$ . It is easy to see that $W$ is convex. Given $x,y\in W$ choose $c\in X$ and $p\in(0,1]$ with $P(c,p,x)\in X$ and $P(c,p,y)\in X$ , which is possible by Step ➁. Then, for each $q\in[0,1]$ ,

	$\displaystyle P(c,p,qx+(1-q)y)=$	$\displaystyle\,p\big{[}qx+(1-q)y\big{]}+(1-p)c$
	$\displaystyle=$	$\displaystyle\,q\big{[}px+(1-p)c\big{]}+(1-q)\big{[}py+(1-p)c\big{]}\in X,$

and hence $qx+(1-q)y\in W$ .

Next we show that $x\in W$ and $q\geq 0$ implies $qx\in W$ . If $q\in[0,1]$ we can use that $0\in X\subseteq W$ and $W$ is already known to be convex to arrive at $qx=qx+(1-q)0\in W$ . Assume now that $q>1$ . Choose $c\in X,p\in(0,1]$ with $P(c,p,x)\in X$ . We apply Lemma 11 and Remark 12.2. to obtain, with $p$ in place of $q$ , $\frac{1}{q}$ in place of $p$ , $q x$ in place of $x$ , and $c, d$ exchanged:
$P\Big{(}\underbrace{P\Big{(}0,\frac{1-p}{1-\frac{p}{q}},c\Big{)}}_{\in X},% \underbrace{\frac{p}{q}}_{\in[0,1)},qx\Big{)}\\ =P\big{(}c,p,\underbrace{P\big{(}0,\tfrac{1}{q},qx\big{)}}_{\in X}\big{)}\in X$
and hence $qx\in W$ .

Finally, we show that $x\in W$ implies $-x\in W$ . Choose $c\in X,p\in(0,1)$ with $P(c,p,x)\in X$ . Avoiding $p=1$ is possible by Step ➀. Then again using Lemma 11 (with $c=x$ and $d=c$ ) and the second part of Remark 12.2. by simultaneously substituting $\frac{1}{2}$ for $p$ and $1-p$ for $r$ , we obtain $q$ and $s$ , which are in $(0,1)$ by Remark 12.3., with
$P\Big{(}\underbrace{P(x,1-p,c)}_{=P(c,p,x)\in X},\underbrace{s}_{\in[0,1)},-x% \Big{)}\\ =P\Big{(}c,q,\underbrace{P(x,\tfrac{1}{2},-x)}_{=0}\Big{)}\in X$
and thus $-x$ satisfies the defining property of $W$ . The numerical values of these $q$ and $s$ are $\frac{2p}{1+p}$ and $\frac{p}{1+p}$ , respectively.

Step ➃.

We show that by the following procedure a binary operation on $W$ extending $\oplus$ is well-defined: given $x_{1},x_{2}\in W$ , choose $c\in X,p\in(0,1]$ with $P(c,p,x_{i})\in X$ , $i\in\{1,2\}$ , and set

x_{1}\boxplus x_{2}\mathrel{\mathop{:}}=P\Big{(}c,\frac{1}{p},P(c,p,x_{1})% \oplus P(c,p,x_{2})\Big{)}.

(11)

For the time being, denote the element of $V$ given by the right hand side of Equation 11 as $w$ . First,

P(c,p,w)=P(c,p,x_{1})\oplus P(c,p,x_{2})\in X,

and it follows that $w\in W$ . Now assume we have $d\in X,q\in(0,1]$ that also satisfy $P(d,q,x_{i})\in X$ , $i=1,2$ . Since $p,q\in(0,1]$ , we have $(1-p)(1-q)\neq 1$ and Lemma 10.3. applies. Taking inverses in Equation 6 (here $r, s$ are as in Equation 5 and we note that $r,s\in(0,1]$ ) yields that also

P(c,\tfrac{1}{p},\text{\_\kern 1.0pt})\circ P(d,\tfrac{1}{r},\text{\_\kern 1.0% pt})=P(d,\tfrac{1}{q},\text{\_\kern 1.0pt})\circ P(c,\tfrac{1}{s},\text{\_% \kern 1.0pt}).

Set

y_{i}\mathrel{\mathop{:}}=P\big{(}d,r,\underbrace{P(c,p,x_{i})}_{\in X}\big{)}% =P\big{(}c,s,\underbrace{P(d,q,x_{i})}_{\in X}\big{)}\in X.

The maps $P(d,r,\text{\_\kern 1.0pt})|_{X}$ and $P(c,s,\text{\_\kern 1.0pt})|_{X}$ are convex semilattice homomorphisms on $X$ , by Lemma 13, and hence

y_{1}\oplus y_{2}=P\big{(}d,r,P(c,p,x_{1})\oplus P(c,p,x_{2})\big{)}=P\big{(}c% ,s,P(d,q,x_{1})\oplus P(d,q,x_{2})\big{)}.

We obtain

$\displaystyle P\big{(}c,\tfrac{1}{p},P(c,p,x_{1})\oplus P(c,p,x_{2})\big{)}$	$\displaystyle=$	$\displaystyle\big{[}P(c,\tfrac{1}{p},\text{\_\kern 1.0pt})\circ P(d,\tfrac{1}{% r},\text{\_\kern 1.0pt})\big{]}(y_{1}\oplus y_{2})$
	$\displaystyle=$	$\displaystyle\big{[}P(d,\tfrac{1}{q},\text{\_\kern 1.0pt})\circ P(c,\tfrac{1}{% s},\text{\_\kern 1.0pt})\big{]}(y_{1}\oplus y_{2})$
	$\displaystyle=$	$\displaystyle P\big{(}d,\tfrac{1}{q},P(d,q,x_{1})\oplus P(d,q,x_{2})\big{)}.$

which proves that $w$ is independent of the choice of $c$ and $q$ .

Finally, note that for $x_{1},x_{2}\in X$ we can choose $p=1$ (and arbitrary $c\in X$ ). This choice gives $x_{1}\boxplus x_{2}=x_{1}\oplus x_{2}$ .

Step ➄.

We show that $W$ is a convex semilattice with $\boxplus$ . We start with the semilattice axioms, which are checked simply by unfolding the definitions. Let $c\in X$ and $p\in(0,1]$ always be chosen appropriately according to the definition of $W$ .
Idempotence is immediate:

{x\boxplus x=P\big{(}c,\tfrac{1}{p},P(c,p,x)\oplus P(c,p,x)\big{)}=P\big{(}c,% \tfrac{1}{p},P(c,p,x)\big{)}=x}.

Similarly, commutativity follows:

{x\boxplus y=P\big{(}c,\tfrac{1}{p},P(c,p,x)\oplus P(c,p,y)\big{)}=P\big{(}c,% \tfrac{1}{p},P(c,p,y\oplus P(c,p,x))\big{)}=y\boxplus x}.

Finally, we derive associativity by:

	$\displaystyle\mkern-27.0mu(x\boxplus y)\boxplus z=$	$\displaystyle\,P\big{(}c,\tfrac{1}{p},P(c,p,x\boxplus y)\oplus P(c,p,z)\big{)}$
	$\displaystyle=$	$\displaystyle\,P\big{(}c,\tfrac{1}{p},P\big{(}c,p,P\big{(}c,\tfrac{1}{p},P(c,p% ,x)\oplus P(c,p,y)\big{)}\big{)}\oplus P(c,p,z)\big{)}$
	$\displaystyle=$	$\displaystyle\,P\big{(}c,\tfrac{1}{p},\big{[}P(c,p,x)\oplus P(c,p,y)\big{]}% \oplus P(c,p,z)\big{)}$
	$\displaystyle=$	$\displaystyle\,P\big{(}c,\tfrac{1}{p},P(c,p,x)\oplus\big{[}P(c,p,y)\oplus P(c,% p,z)\big{]}\big{)}$
	$\displaystyle=$	$\displaystyle\,P\big{(}c,\tfrac{1}{p},P(c,p,x)\oplus P(c,p,y\boxplus z)\big{)}$
	$\displaystyle=$	$\displaystyle\,x\boxplus(y\boxplus z).$

The proof of distributivity is slightly more complicated. We first show a particular case, namely,

\forall x,y\in W,d\in X,q\in(0,1){\mathop{:}\kern 5.0pt}(x\boxplus y)+_{q}d=(x% +_{q}d)\boxplus(y+_{q}d)

(12)

Choose $c, p$ suitable and set again $s\mathrel{\mathop{:}}=\frac{p}{p+q-pq},r\mathrel{\mathop{:}}=\frac{q}{p+q-pq}$ . Then, using Equation 6 twice, also in a somewhat peculiar way – by composing with the inverse of $P(c,s,\text{\_\kern 1.0pt})$ on the left and the inverse of $P(c,p,\text{\_\kern 1.0pt})$ on the right, we get

	$\displaystyle(x\boxplus y)+_{q}d=$	$\displaystyle\,P\big{(}d,q,P\big{(}c,\tfrac{1}{p},P(c,p,x)\oplus P(c,p,y)\big{% )}\big{)}$
	$\displaystyle=$	$\displaystyle\,P\big{(}c,\tfrac{1}{s},P\big{(}d,r,P(c,p,x)\oplus P(c,p,y)\big{% )}\big{)}$
	$\displaystyle=$	$\displaystyle\,P\big{(}c,\tfrac{1}{s},P(d,r,P(c,p,x))\oplus P(d,r,P(c,p,y))% \big{)}$
	$\displaystyle=$	$\displaystyle\,P\big{(}c,\tfrac{1}{s},P(c,s,P(d,q,x))\oplus P(c,s,P(d,q,y))% \big{)}$
	$\displaystyle=$	$\displaystyle\,P(d,q,x)\boxplus P(d,q,y)$
	$\displaystyle=$	$\displaystyle\,(x+_{q}d)\boxplus(y+_{q}d).$

Note here that $P(c,s,P(d,q,x)),P(c,s,P(d,q,y))\in X$ .

Now let $x,y,z\in W$ and $p\in(0,1)$ . Choose $d\in X,q\in(0,1]$ with $P(d,q,x),P(d,q,y),$ $P(d,q,z)\in X$ . Using that $P(d,q,\text{\_\kern 1.0pt})$ is a convex algebra homomorphism, the definition of $\boxplus$ , distributivity in $X$ , once again that $P(d,q,\text{\_\kern 1.0pt})$ is a convex algebra homomorphism, the coincidence of $\boxplus$ and $\oplus$ on $X$ , and finally Equation 12 translated in terms of perspective shift, we find

	$\displaystyle P\big{(}d,q,$	$\displaystyle\,(x\boxplus y)+_{p}z\big{)}=\Big{[}P(d,q,x\boxplus y)\Big{]}+_{p% }P(d,q,z)$
	$\displaystyle=$	$\displaystyle\,\Big{[}P(d,q,x)\oplus P(d,q,y)\Big{]}+_{p}P(d,q,z)$
	$\displaystyle=$	$\displaystyle\,\Big{[}P(d,q,x)+_{p}P(d,q,z)\Big{]}\oplus\Big{[}P(d,q,y)+_{p}P(% d,q,z)\Big{]}$
	$\displaystyle=$	$\displaystyle\,P(d,q,x+_{p}z)\oplus P(d,q,y+_{p}z)$
	$\displaystyle=$	$\displaystyle P(d,q,x+_{p}z)\boxplus P(d,q,y+_{p}z)$
	$\displaystyle=$	$\displaystyle\,P\big{(}d,q,(x+_{p}z)\boxplus(y+_{p}z)\big{)}.$

Since $P(d,q,\text{\_\kern 1.0pt})$ is injective, it follows that $(x\boxplus y)+_{p}z=(x+_{p}z)\boxplus(y+_{p}z)$ . $\hfill\blacktriangleleft$

3.3 The constructed space is a Riesz space

The proof of Theorem 6 will be complete once we prove the following lemma already mentioned in Remark 7.

Lemma 15.

Let $V$ be a vector space over $\mathbb{R}$ and set $x+_{p}y\mathrel{\mathop{:}}=px+(1-p)y$ for $x,y\in V$ , $p\in(0,1)$ . Further, let $\oplus$ be a binary operation on $V$ such that $\langle V,+_{p},\oplus\rangle$ is a convex semilattice, and let $\leq$ be the partial order induced by $\oplus$ via Equation 2. Then $\langle V,\leq\rangle$ is a Riesz space.

Proof.

We first show that

\forall x,y\in V,q>0{\mathop{:}\kern 5.0pt}qx\oplus qy=q(x\oplus y)

(13)

If $q\leq 1$ , we can use the distributive law to compute

q(x\oplus y)=(x\oplus y)+_{q}0=(x+_{q}0)\oplus(y+_{q}0)=qx\oplus qy.

If $q>1$ , we apply this rule with $\frac{1}{q}$ and $q x, q y$ to obtain

\frac{1}{q}\big{(}qx\oplus qy\big{)}=x\oplus y.

Hence, also in this case $qx\oplus qy=q(x\oplus y)$ .

From Equation 13 we can now deduce that $\langle V,\leq\rangle$ is an ordered vector space. First, for $x,y\in V$ and $q>0$ ,

x\leq y\Leftrightarrow x\oplus y=y\Leftrightarrow q(x\oplus y)=qy% \Leftrightarrow qx\oplus qy=qy\Leftrightarrow qx\leq qy

and in particular for $x=0$ we get first needed property for ordered space.
Second, for $x,y,z\in V$ with $x\leq y$ we have

$\displaystyle(x+z)\oplus(y+z)$	$\displaystyle=$	$\displaystyle 2(x+_{\frac{1}{2}}z)\oplus 2(y+_{\frac{1}{2}}z)$
	$\displaystyle=$	$\displaystyle 2\big{[}(x+_{\frac{1}{2}}z)\oplus(y+_{\frac{1}{2}}z)\big{]}$
	$\displaystyle=$	$\displaystyle 2\big{[}(x\oplus y)+_{\frac{1}{2}}z\big{]}=2(y+_{\frac{1}{2}}z)$
	$\displaystyle=$	$\displaystyle y+z.$

It remains to establish existence of infima. For each two elements $x,y\in V$ it holds that

x\leq y\Leftrightarrow x+(-x-y)\leq y+(-x-y)\Leftrightarrow-y\leq-x.

Now let $x,y\in V$ be given. Then

\{z\in V\mid\mkern 3.0mu-x\leq z\wedge-y\leq z\}=\{z\in V\mid\mkern 3.0mu-z% \leq x\wedge-z\leq y\},

and hence $-\sup\{-x,-y\}$ is the infimum of $x$ and $y$ .
$\hfill\blacktriangleleft$

4 Conclusions

We have proven an analogue in the setting of convex semilattices of what we refer to as the Stone-Kneser theorem for cancellative convex algebras. We showed in Theorem 6 that a convex semilattice is cancellative if and only if it can be homomorphically embedded in a Riesz space. Here, we call a convex semilattice cancellative when its underlying convex algebra is cancellative.

Interestingly, as mentioned in Remark 8, the result does not impose any condition on the semilattice structure.

The work presented here is a first step towards understanding the structure of convex semilattices. Other directions that we will explore involve more specific notions of cancellativity as well as understanding of homomorphisms and congruences of convex semilattices.

By more specific notions of cancellativity of convex semilattices, that are also worth investigating, we mean, e.g., the following property that we call “mid-point cancellativity”

x+_{\frac{1}{2}}y=u+_{\frac{1}{2}}v\wedge x\oplus y=u\oplus v\Rightarrow(x=u% \wedge y=v)\vee(x=v\wedge y=u).

We have some preliminary results on this topic that we will fully explore in future work.

References

[1] Alejandro Aguirre and Lars Birkedal. Step-indexed logical relations for countable nondeterminism and probabilistic choice. Proc. ACM Program. Lang., 7(POPL), 2023. doi:10.1145/3571195.
[2] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.
[3] Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. The theory of traces for systems with nondeterminism and probability. In Proc. LICS’19, pages 1–14, 2019. doi:10.1109/LICS.2019.8785673.
[4] Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases. In Proc. CALCO’21, volume 211 of LIPIcs, pages 11:1–11:18, 2021. doi:10.4230/LIPIcs.CALCO.2021.11.
[5] Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. The theory of traces for systems with nondeterminism, probability, and termination. Logical Methods in Computer Science, Volume 18, Issue 2, June 2022. doi:10.46298/lmcs-18(2:21)2022.
[6] Pablo S. Castro, Prakash Panangaden, and Doina Precup. Equivalence relations in fully and partially observable markov decision processes. In Proc. IJCAI’09, pages 1653–1658, 2009.
[7] Ep de Jonge and Arnoud C.M. van Rooij. Introduction to Riesz spaces, volume 78 of Math. Cent. Tracts. Centrum voor Wiskunde en Informatica (CWI), Amsterdam, 1977.
[8] Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk. A storm is coming: A modern probabilistic model checker. In Proc. CAV 2017, volume 10427 of LNCS, pages 592–600, 2017. doi:10.1007/978-3-319-63390-9_31.
[9] Ernst-Erich Doberkat. Eilenberg-Moore algebras for stochastic relations. Inform. and Comput., 204(12):1756–1781, 2006. doi:10.1016/j.ic.2006.09.001.
[10] Ernst-Erich Doberkat. Erratum and addendum: Eilenberg-Moore algebras for stochastic relations [mr2277336]. Inform. and Comput., 206(12):1476–1484, 2008. doi:10.1016/j.ic.2008.08.002.
[11] Jean Goubault-Larrecq. Prevision domains and convex powercones. In Proc. FOSSACS’08, volume 4962 of LNCS, pages 318–333, 2008. doi:10.1007/978-3-540-78499-9_23.
[12] Alexandre Goy and Daniela Petrisan. Combining probabilistic and non-deterministic choice via weak distributive laws. In Proc. LICS’20, pages 454–464. ACM, 2020. doi:10.1145/3373718.3394795.
[13] Hans A. Hansson. Time and probability in formal design of distributed systems. PhD thesis, Uppsala University, 1991.
[14] Jerry I. den Hartog and Erik P. de Vink. Mixing up nondeterminism and probability: A preliminary report. In Proc. PROBMIV’98. ENTCS 22, 1998.
[15] Holger Hermanns, Jan Krcál, and Jan Kretínský. Probabilistic bisimulation: Naturally on distributions. In Proc. CONCUR’14, volume 8704 of LNCS, pages 249–265, 2014. doi:10.1007/978-3-662-44584-6_18.
[16] Holger Hermanns, Augusto Parma, Roberto Segala, Björn Wachter, and Lijun Zhang. Probabilistic logical characterization. Information and Computation, 209(2):154–172, 2011. doi:10.1016/J.IC.2010.11.024.
[17] Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. A convenient category for higher-order probability theory. CoRR, abs/1701.02547, 2017. arXiv:1701.02547.
[18] Jennifer Hyndman, James B. Nation, and Joy Nishida. Congruence lattices of semilattices with operators. Studia Logica, 104(2):305–316, 2016. doi:10.1007/s11225-015-9641-0.
[19] Bart Jacobs. Coalgebraic trace semantics for combined possibilitistic and probabilistic systems. Electr. Notes Theor. Comput. Sci., 203(5):131–152, 2008. doi:10.1016/J.ENTCS.2008.05.023.
[20] Bart Jacobs. Convexity, duality and effects. In Theoretical computer science, volume 323 of IFIP Adv. Inf. Commun. Technol., pages 1–19. Springer, Berlin, 2010. doi:10.1007/978-3-642-15240-5_1.
[21] Leslie P. Kaelbling, Michael L Littman, and Anthony R. Cassandra. Planning and Acting in Partially Observable Stochastic Domains. Artif. Intell., 1998.
[22] Klaus Keimel and Gordon D. Plotkin. Mixed powerdomains for probability and nondeterminism. Log. Methods Comput. Sci., 13(1):84, 2017. Id/No 2. doi:10.23638/LMCS-13(1:2)2017.
[23] Hellmuth Kneser. Konvexe Räume. Arch. Math., 3:198–206, 1952. doi:10.1007/BF01899364.
[24] Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Prism: Probabilistic symbolic model checker. In Computer Performance Evaluation / TOOLS, volume 2324 of LNCS, pages 200–204, 2002. doi:10.1007/3-540-46029-2_13.
[25] Wilhelmus A.J. Luxemburg and Adriaan C. Zaanen. Riesz spaces. Vol. I, volume 1 of North-Holland Math. Libr. Elsevier (North-Holland), Amsterdam, 1971.
[26] Matteo Mio. Upper-expectation bisimilarity and łukasiewicz $\mu$ -calculus. In Proc. FOSSACS’14, volume 8412 of LNCS, pages 335–350, 2014. doi:10.1007/978-3-642-54830-7_22.
[27] Matteo Mio, Ralph Sarkis, and Valeria Vignudelli. Combining nondeterminism, probability, and termination: Equational and metric reasoning. In Proc. LICS’21, pages 1–14, 2021. doi:10.1109/LICS52264.2021.9470717.
[28] Matteo Mio and Valeria Vignudelli. Monads and quantitative equational theories for nondeterminism and probability. In Proc. CONCUR’20, volume 171 of LIPIcs, pages 28:1–28:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.CONCUR.2020.28.
[29] Michael W. Mislove. Nondeterminism and probabilistic choice: Obeying the laws. In Proc CONCUR’00, volume 1877 of LNCS, pages 350–364, 2000. doi:10.1007/3-540-44618-4_26.
[30] Michael W. Mislove, Joel Ouaknine, and James Worrell. Axioms for probability and nondeterminism. In Proc. EXPRESS’03, volume 96 of ENTCS, pages 7–28. Elsevier, 2003. doi:10.1016/J.ENTCS.2004.04.019.
[31] Aloïs Rosset, Helle H. Hansen, and Jörg Endrullis. Algebraic presentation of semifree monads. In Proc. CMCS’22, volume 13225 of LNCS, pages 110–132, 2022. doi:10.1007/978-3-031-10736-8_6.
[32] Stuart Russell and Peter Norvig. Artificial Intelligence: A Modern Approach. Prentice Hall, 2009.
[33] Roberto Segala. Modeling and verification of randomized distributed real-time systems. PhD thesis, MIT, 1995.
[34] Roberto Segala and Nancy Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 2(2):250–273, 1995.
[35] Jonathan D.H. Smith. Modes, modals, and barycentric algebras: a brief survey and an additivity theorem. Demonstr. Math., 44(3):571–587, 2011. doi:10.1515/dema-2013-0332.
[36] Ana Sokolova and Harald Woracek. Congruences of convex algebras. J. Pure Appl. Algebra, 219(8):3110–3148, 2015. doi:10.1016/j.jpaa.2014.10.005.
[37] Sam Staton, Hongseok Yang, Frank Wood, Chris Heunen, and Ohad Kammar. Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In Proc. LICS’16, pages 525–534, 2016. doi:10.1145/2933575.2935313.
[38] Marshall H. Stone. Postulates for the barycentric calculus. Ann. Mat. Pura Appl. (4), 29:25–30, 1949. doi:10.1007/BF02413910.
[39] Tadeusz Świrszcz. Monadic functors and convexity. Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys., 22:39–42, 1974.
[40] Regina Tix, Klaus Keimel, and Gordon D. Plotkin. Semantic domains for combining probability and non-determinism. ENTCS, 222:3–99, 2009. doi:10.1016/j.entcs.2009.01.002.
[41] Daniele Varacca. Probability, Nondeterminism and Concurrency: Two Denotational Models for Probabilistic Computation. PhD thesis, Univ. Aarhus, 2003. BRICS Dissertation Series, DS-03-14.
[42] Daniele Varacca and Glynn Winskel. Distributing probabililty over nondeterminism. MSCS, 16(1):87–113, 2006. doi:10.1017/S0960129505005074.
[43] Moshe Y. Vardi. Automatic verification of probabilistic concurrent finite state programs. In Foundations of Computer Science, 1985., 26th Annual Symposium on, pages 327–338. IEEE, 1985. doi:10.1109/SFCS.1985.12.
[44] Noam Zilberstein, Dexter Kozen, Alexandra Silva, and Joseph Tassarotti. A demonic outcome logic for randomized nondeterminism. Proc. ACM Program. Lang., 9(POPL), 2025. doi:10.1145/3704855.

[bib.bib1] [1] Alejandro Aguirre and Lars Birkedal. Step-indexed logical relations for countable nondeterminism and probabilistic choice. Proc. ACM Program. Lang., 7(POPL), 2023. doi:10.1145/3571195.

[bib.bib2] [2] Christel Baier and Joost-Pieter Katoen. Principles of model checking. MIT Press, 2008.

[bib.bib3] [3] Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. The theory of traces for systems with nondeterminism and probability. In Proc. LICS’19, pages 1–14, 2019. doi:10.1109/LICS.2019.8785673.

[bib.bib4] [4] Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. Presenting Convex Sets of Probability Distributions by Convex Semilattices and Unique Bases. In Proc. CALCO’21, volume 211 of LIPIcs, pages 11:1–11:18, 2021. doi:10.4230/LIPIcs.CALCO.2021.11.

[bib.bib5] [5] Filippo Bonchi, Ana Sokolova, and Valeria Vignudelli. The theory of traces for systems with nondeterminism, probability, and termination. Logical Methods in Computer Science, Volume 18, Issue 2, June 2022. doi:10.46298/lmcs-18(2:21)2022.

[bib.bib6] [6] Pablo S. Castro, Prakash Panangaden, and Doina Precup. Equivalence relations in fully and partially observable markov decision processes. In Proc. IJCAI’09, pages 1653–1658, 2009.

[bib.bib7] [7] Ep de Jonge and Arnoud C.M. van Rooij. Introduction to Riesz spaces, volume 78 of Math. Cent. Tracts. Centrum voor Wiskunde en Informatica (CWI), Amsterdam, 1977.

[bib.bib8] [8] Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk. A storm is coming: A modern probabilistic model checker. In Proc. CAV 2017, volume 10427 of LNCS, pages 592–600, 2017. doi:10.1007/978-3-319-63390-9_31.

[bib.bib9] [9] Ernst-Erich Doberkat. Eilenberg-Moore algebras for stochastic relations. Inform. and Comput., 204(12):1756–1781, 2006. doi:10.1016/j.ic.2006.09.001.

[bib.bib10] [10] Ernst-Erich Doberkat. Erratum and addendum: Eilenberg-Moore algebras for stochastic relations [mr2277336]. Inform. and Comput., 206(12):1476–1484, 2008. doi:10.1016/j.ic.2008.08.002.

[bib.bib11] [11] Jean Goubault-Larrecq. Prevision domains and convex powercones. In Proc. FOSSACS’08, volume 4962 of LNCS, pages 318–333, 2008. doi:10.1007/978-3-540-78499-9_23.

[bib.bib12] [12] Alexandre Goy and Daniela Petrisan. Combining probabilistic and non-deterministic choice via weak distributive laws. In Proc. LICS’20, pages 454–464. ACM, 2020. doi:10.1145/3373718.3394795.

[bib.bib13] [13] Hans A. Hansson. Time and probability in formal design of distributed systems. PhD thesis, Uppsala University, 1991.

[bib.bib14] [14] Jerry I. den Hartog and Erik P. de Vink. Mixing up nondeterminism and probability: A preliminary report. In Proc. PROBMIV’98. ENTCS 22, 1998.

[bib.bib15] [15] Holger Hermanns, Jan Krcál, and Jan Kretínský. Probabilistic bisimulation: Naturally on distributions. In Proc. CONCUR’14, volume 8704 of LNCS, pages 249–265, 2014. doi:10.1007/978-3-662-44584-6_18.

[bib.bib16] [16] Holger Hermanns, Augusto Parma, Roberto Segala, Björn Wachter, and Lijun Zhang. Probabilistic logical characterization. Information and Computation, 209(2):154–172, 2011. doi:10.1016/J.IC.2010.11.024.

[bib.bib17] [17] Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. A convenient category for higher-order probability theory. CoRR, abs/1701.02547, 2017. arXiv:1701.02547.

[bib.bib18] [18] Jennifer Hyndman, James B. Nation, and Joy Nishida. Congruence lattices of semilattices with operators. Studia Logica, 104(2):305–316, 2016. doi:10.1007/s11225-015-9641-0.

[bib.bib19] [19] Bart Jacobs. Coalgebraic trace semantics for combined possibilitistic and probabilistic systems. Electr. Notes Theor. Comput. Sci., 203(5):131–152, 2008. doi:10.1016/J.ENTCS.2008.05.023.

[bib.bib20] [20] Bart Jacobs. Convexity, duality and effects. In Theoretical computer science, volume 323 of IFIP Adv. Inf. Commun. Technol., pages 1–19. Springer, Berlin, 2010. doi:10.1007/978-3-642-15240-5_1.

[bib.bib21] [21] Leslie P. Kaelbling, Michael L Littman, and Anthony R. Cassandra. Planning and Acting in Partially Observable Stochastic Domains. Artif. Intell., 1998.

[bib.bib22] [22] Klaus Keimel and Gordon D. Plotkin. Mixed powerdomains for probability and nondeterminism. Log. Methods Comput. Sci., 13(1):84, 2017. Id/No 2. doi:10.23638/LMCS-13(1:2)2017.

[bib.bib23] [23] Hellmuth Kneser. Konvexe Räume. Arch. Math., 3:198–206, 1952. doi:10.1007/BF01899364.

[bib.bib24] [24] Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Prism: Probabilistic symbolic model checker. In Computer Performance Evaluation / TOOLS, volume 2324 of LNCS, pages 200–204, 2002. doi:10.1007/3-540-46029-2_13.

[bib.bib25] [25] Wilhelmus A.J. Luxemburg and Adriaan C. Zaanen. Riesz spaces. Vol. I, volume 1 of North-Holland Math. Libr. Elsevier (North-Holland), Amsterdam, 1971.

[bib.bib26] [26] Matteo Mio. Upper-expectation bisimilarity and łukasiewicz $\mu$ -calculus. In Proc. FOSSACS’14, volume 8412 of LNCS, pages 335–350, 2014. doi:10.1007/978-3-642-54830-7_22.

[bib.bib27] [27] Matteo Mio, Ralph Sarkis, and Valeria Vignudelli. Combining nondeterminism, probability, and termination: Equational and metric reasoning. In Proc. LICS’21, pages 1–14, 2021. doi:10.1109/LICS52264.2021.9470717.

[bib.bib28] [28] Matteo Mio and Valeria Vignudelli. Monads and quantitative equational theories for nondeterminism and probability. In Proc. CONCUR’20, volume 171 of LIPIcs, pages 28:1–28:18. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.CONCUR.2020.28.

[bib.bib29] [29] Michael W. Mislove. Nondeterminism and probabilistic choice: Obeying the laws. In Proc CONCUR’00, volume 1877 of LNCS, pages 350–364, 2000. doi:10.1007/3-540-44618-4_26.

[bib.bib30] [30] Michael W. Mislove, Joel Ouaknine, and James Worrell. Axioms for probability and nondeterminism. In Proc. EXPRESS’03, volume 96 of ENTCS, pages 7–28. Elsevier, 2003. doi:10.1016/J.ENTCS.2004.04.019.

[bib.bib31] [31] Aloïs Rosset, Helle H. Hansen, and Jörg Endrullis. Algebraic presentation of semifree monads. In Proc. CMCS’22, volume 13225 of LNCS, pages 110–132, 2022. doi:10.1007/978-3-031-10736-8_6.

[bib.bib32] [32] Stuart Russell and Peter Norvig. Artificial Intelligence: A Modern Approach. Prentice Hall, 2009.

[bib.bib33] [33] Roberto Segala. Modeling and verification of randomized distributed real-time systems. PhD thesis, MIT, 1995.

[bib.bib34] [34] Roberto Segala and Nancy Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 2(2):250–273, 1995.

[bib.bib35] [35] Jonathan D.H. Smith. Modes, modals, and barycentric algebras: a brief survey and an additivity theorem. Demonstr. Math., 44(3):571–587, 2011. doi:10.1515/dema-2013-0332.

[bib.bib36] [36] Ana Sokolova and Harald Woracek. Congruences of convex algebras. J. Pure Appl. Algebra, 219(8):3110–3148, 2015. doi:10.1016/j.jpaa.2014.10.005.

[bib.bib37] [37] Sam Staton, Hongseok Yang, Frank Wood, Chris Heunen, and Ohad Kammar. Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In Proc. LICS’16, pages 525–534, 2016. doi:10.1145/2933575.2935313.

[bib.bib38] [38] Marshall H. Stone. Postulates for the barycentric calculus. Ann. Mat. Pura Appl. (4), 29:25–30, 1949. doi:10.1007/BF02413910.

[bib.bib39] [39] Tadeusz Świrszcz. Monadic functors and convexity. Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys., 22:39–42, 1974.

[bib.bib40] [40] Regina Tix, Klaus Keimel, and Gordon D. Plotkin. Semantic domains for combining probability and non-determinism. ENTCS, 222:3–99, 2009. doi:10.1016/j.entcs.2009.01.002.

[bib.bib41] [41] Daniele Varacca. Probability, Nondeterminism and Concurrency: Two Denotational Models for Probabilistic Computation. PhD thesis, Univ. Aarhus, 2003. BRICS Dissertation Series, DS-03-14.

[bib.bib42] [42] Daniele Varacca and Glynn Winskel. Distributing probabililty over nondeterminism. MSCS, 16(1):87–113, 2006. doi:10.1017/S0960129505005074.

[bib.bib43] [43] Moshe Y. Vardi. Automatic verification of probabilistic concurrent finite state programs. In Foundations of Computer Science, 1985., 26th Annual Symposium on, pages 327–338. IEEE, 1985. doi:10.1109/SFCS.1985.12.

[bib.bib44] [44] Noam Zilberstein, Dexter Kozen, Alexandra Silva, and Joseph Tassarotti. A demonic outcome logic for randomized nondeterminism. Proc. ACM Program. Lang., 9(POPL), 2025. doi:10.1145/3704855.

	$\displaystyle P\big{(}c,p,P(c,q,x)\big{)}=$	$\displaystyle\,p\big{[}qx+(1-q)c\big{]}+(1-p)c$
	$\displaystyle=$	$\displaystyle\,pq\cdot x+\big{(}\underbrace{p(1-q)+(1-p)}_{1-pq}\big{)}\cdot c% =P(c,pq,x).$

Cancellative Convex Semilattices

Abstract

Keywords and phrases:

Copyright and License:

2012 ACM Subject Classification:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

2 Background and main result

Revisiting convex algebras

Definition 1.

Example 2.

Theorem 3 (Stone-Kneser).

Cancellative convex semilattices

Definition 4.

Example 5.

Theorem 6.

▶ Remark 7.

▶ Remark 8.

3 Ideas, tools, construction, proof

3.1 Perspective shift

Definition 9.

Lemma 10.

Proof.

Lemma 11.

Proof.

▶ Remark 12.

Lemma 13.

Proof.

3.2 Constructing the needed space

Proposition 14.

Proof.

Step ➀.

Step ➁.

Step ➂.

Step ➃.

Step ➄.

3.3 The constructed space is a Riesz space

Lemma 15.

Proof.

4 Conclusions

References

$\blacktriangleright$ Remark 7.

$\blacktriangleright$ Remark 8.

$\blacktriangleright$ Remark 12.