Cancellative Convex Semilattices

Ana Sokolova; Harald Woracek

Cancellative Convex Semilattices

T0 review · 0 major / 4 minor · reviewed 2026-08-06 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Cancellative convex semilattices are exactly the convex subsemilattices of Riesz spaces.

desk verdict Clean structural theorem: cancellative convex semilattices embed into Riesz spaces, with a careful proof worth refereeing. read the letter →

arxiv 2507.11186 v1 pith:SCBNCHRY submitted 2025-07-15 cs.LO

Ana Sokolova , Harald Woracek This is my paper · ORCID

classification cs.LO MSC 06F2006A1252A01

keywords convexsemilatticecancellativityRieszspacelattice-orderedvectorperspectiveshiftalgebraprobabilityandnondeterminismdistributivitylaw

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

The paper proves a representation theorem for convex semilattices, the algebraic structures combining probabilistic choice (a family of 'biased coin' operations $+_p$ for $p \in (0,1)$) with nondeterministic choice (a join operation $\oplus$). The main result says that if the probabilistic operations are cancellative — meaning $x +_p z = y +_p z$ implies $x = y$ — then the whole structure is isomorphic to a convex subset of a Riesz space (a vector space whose order is a lattice) closed under binary suprema. This is the exact analogue, for probability plus nondeterminism, of the classical theorem that cancellative convex algebras are precisely the convex subsets of vector spaces. It matters because these algebras are the algebras for the monad of finitely generated convex subsets of probability distributions, so the result gives a concrete linear and order-theoretic home to the semantics of combined probabilistic and nondeterministic computation.

What carries the argument

The workhorse is the perspective shift $P(c,p,x) = p x + (1-p) c$, a geometric transformation that fixes the center $c$ and moves $x$ toward $c$ with ratio $p$; in the convex-algebra notation this is just $x +_p c$. The paper develops identities for composing perspective shifts (compositions and an associativity rule) and shows that, on a convex semilattice $X$ sitting inside a vector space, each $P(c,p,\_)$ restricts to a convex semilattice homomorphism. These facts are used to construct a linear subspace $W$ of the ambient vector space, containing $X$, and a binary operation $\boxplus$ on $W$ extending the original join; the construction is shown to be well-defined by the homomorphism property. A short lemma then proves that the order induced by $\boxplus$ on $W$ is a lattice order compatible with the vector space structure, so $W$ is a Riesz space.

What would settle it

The theorem asserts an embedding for every cancellative convex semilattice, so one counterexample suffices to falsify it. Because the proof is constructive, a concrete check is available: take any cancellative convex semilattice $X$ embedded in a vector space, run the perspective-shift construction to form $W$ and $\boxplus$, and verify the distributive law $(x \boxplus y) +_p z = (x +_p z) \boxplus (y +_p z)$; a single failure would disprove the theorem, while verification on nontrivial examples such as convex subsets of $\mathbb{R}^2$ with a designated join would test the construction directly.

Watch

Extended reading notes

Core claim

The central discovery is Theorem 6: if $\langle X, +_p, \oplus\rangle$ is a cancellative convex semilattice, then there exists a Riesz space $V$ and a convex subset $Y \subseteq V$ closed under binary suprema such that $X$ is isomorphic to the convex semilattice induced by $V$ on $Y$, with $+_p$ computed as $p x + (1-p) y$ and $\oplus$ as $\sup\{x,y\}$. Equivalently, cancellative convex semilattices are exactly the convex subsemilattices of Riesz spaces. The theorem is established by first embedding the underlying convex algebra into a real vector space via the classical embedding theorem for cancellative convex algebras, then extending the semilattice operation from $X$ to a linear subspace $W$ by a perspective-shift construction, and finally showing the induced order on $W$ makes it a Riesz space. The converse, that any convex supremum-closed subset of a Riesz space is a cancellative convex semilattice, is immediate from linearity and lattice identities.

Load-bearing premise

The argument depends on the classical theorem that every cancellative convex algebra can be embedded into a real vector space; the entire construction of the subspace $W$ and the extended join takes place inside that ambient vector space, so if that embedding theorem were false the proof would have no starting point.

Editorial extensions

If this is right

Every cancellative convex semilattice is a subalgebra of a Riesz space, so all equational identities that hold in Riesz spaces (with $+_p$ and $\sup$) also hold in all cancellative convex semilattices.
No additional assumption on the semilattice order is needed: cancellativity of the convex operations alone forces representability in an ordered vector space, improving on the earlier condition that an order-cancellation axiom be imposed.
The proof provides an explicit construction: embed the underlying convex algebra into a vector space, extend the join to the linear span via perspective shifts, and the resulting ordered vector space is automatically a Riesz space.
Since convex semilattices are the algebras for the monad of finitely generated convex subsets of probability distributions, the cancellative ones now have a complete geometric representation as convex subsemilattices of Riesz spaces.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The perspective-shift extension is a general technique that should transfer to other varieties of algebras with a convex-algebra reduct plus additional idempotent operations; the same construction may yield representation theorems for cancellative variants of such mixed theories.
The paper leaves implicit that the result transfers to any ordered field: the classical embedding theorem holds over ordered skew fields, so the same proof should produce embeddings into Riesz spaces over other ordered fields.
A testable strengthening suggested by the proof: if a convex semilattice is cancellative, then the perspective-shift construction gives an explicit algorithmic representation, which could be implemented to compute the ambient Riesz space and the extended join for finitely presented examples.
The 'mid-point cancellativity' condition proposed at the end of the paper is a natural candidate for a weaker assumption under which the ordering, not just the convex structure, becomes recoverable from the semilattice; this is a possible direction for non-cancellative or partially cancellative structures.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Colleague —

The one thing to know: this paper delivers the expected Stone-Kneser analogue for convex semilattices, and the proof is solid. Cancellative convex semilattices are exactly the convex subsemilattices of Riesz spaces. That is a real theorem, not a corollary of the classical one, because you have to extend the semilattice operation from the original set to the whole vector space.

What is genuinely new: Keimel and Plotkin had an embeddability criterion for ordered barycentric algebras under an order-cancellation axiom. This paper shows that when suprema exist, that order assumption is unnecessary. That is a clean gap to close, and the construction deserves credit.

The proof is the main achievement. The perspective-shift machinery is explained well, and the five-step construction in Proposition 14 is verified in detail. I checked the delicate step—well-definedness of the extended join—and it works: Lemma 13 gives homomorphisms, and the independence argument is coherent. The stress-test note goes through every step with numbers and they check out. Lemma 15, converting the vector-space convex semilattice into a Riesz space, is neat.

Soft spots are minor: a couple of notation slips (the bound variable in Step 1 of Prop 14, a typo in the commutativity computation). They do not hinder the argument. The paper is dense, but the pictures help. It leans on Stone-Kneser as a black box, which is fine—it is a classical, correctly cited theorem.

This is for researchers in quantitative semantics, universal algebra, and monad theory. It is a solid structural result, not a flashy one. I would send it to peer review; it deserves careful refereeing, and I expect it to be accepted after minor revision.

Referee Report

0 major / 4 minor

Summary. The paper proves a representation theorem for cancellative convex semilattices: every cancellative convex semilattice is isomorphic to a convex subset of a Riesz space that is closed under binary suprema, with the convex semilattice operations induced by the ambient vector space (Theorem 6). The proof embeds the underlying cancellative convex algebra into a vector space via the classical Stone-Kneser theorem, translates so that 0 lies in the set, and then constructs a linear subspace W to which the semilattice operation is extended by a perspective-shift procedure (Proposition 14). A final lemma shows that any convex semilattice whose underlying convex algebra is a vector space is a Riesz space (Lemma 15). The development is self-contained apart from Stone-Kneser, and all perspective-shift properties used in the main construction are re-proved in Section 3.1.

Significance. The main theorem is a natural and nontrivial analogue of the Stone-Kneser theorem for convex algebras and provides a clean structural characterization of cancellative convex semilattices, relevant to the algebraic theory of probabilistic and nondeterministic computation. The proof is elementary, detailed, and constructive, making the result potentially useful for further study of convex semilattices. The paper is carefully written, and the external dependence on Stone-Kneser is clearly flagged and appropriate; the authors re-prove all auxiliary perspective-shift facts instead of relying on their previous work, so the argument is self-contained in the relevant sense.

minor comments (4)

[Proposition 14, Step 1] The notation p(x) for the supremum is misleading because the value depends on the fixed center c chosen at the start of the step; the dependence should be made explicit, e.g., by writing p_c(x) or by stating that c is fixed throughout the argument.
[Proposition 14, Step 5, commutativity proof] The displayed expression 'P(c,p,y⊕P(c,p,x))' is not well-formed, since ⊕ is not yet defined for arbitrary elements of W; it should read 'P(c,p,y)⊕P(c,p,x)' (or an equivalent correct expression).
[Lemma 15] The sentence 'in particular for x=0 we get first needed property for ordered space' is mislabeled; the implication for x=0 yields the second property (positive homogeneity), while the first property (translation invariance) is proved immediately afterwards.
[Section 3.1] The proofs of Lemmas 10 and 11 contain LaTeX artifacts (e.g., '/bracehtipupleft/.../') that should be cleaned up in the final version; these artifacts obscure the otherwise clear computations.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the main proof is self-contained modulo the externally cited Stone-Kneser theorem.

full rationale

The central theorem (Theorem 6) is derived from the classical Stone-Kneser theorem (Theorem 3), which is external to the paper, plus an explicit and detailed construction. The only self-citation is [36], used for the intuition of perspective shift; every property of the perspective function P is re-proved in Lemmas 10-13, so the citation is not load-bearing. The reduction at the start of Section 3 embeds only the convex algebra into a vector space via Stone-Kneser, and the semilattice operation is transferred along that isomorphism; this is not circular. Proposition 14 constructs the subspace W and the operation ⊞ using only the convex semilattice axioms and vector-space identities, with all steps verified by explicit computation. Lemma 15 then derives the Riesz-space order properties from distributivity and Equation (13), again without assuming the conclusion. No fitted parameters, no author-imported uniqueness theorems, and no target statement assumed by definition. The result is therefore self-contained modulo the external classical Stone-Kneser theorem.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The central claim rests on the classical Stone-Kneser theorem as the only substantive external input. The remaining assumptions are part of the definitions (distributivity, cancellativity) or elementary WLOG reductions (translation, nonempty case). No free parameters or invented entities appear.

assumptions (4)

domain assumption Stone-Kneser theorem: every cancellative convex algebra is isomorphic to a convex subset of a vector space over R.
Invoked at the start of Section 3 to assume X sits inside a vector space with 0 in X. It is the main external theorem used, and the paper does not prove it.
domain assumption Distributivity axiom in the definition of convex semilattice (Definition 4).
Used throughout, e.g., in Lemma 13, the construction of the extended join, and Lemma 15. This is an intrinsic part of the objects under study, not an ad hoc assumption.
standard math The empty convex semilattice case is trivial.
Section 3 explicitly discards the empty case as trivial; no proof is given.
standard math 0 can be assumed to lie in X via translation in the ambient vector space.
Section 3 states that translations in a vector space are isomorphisms with respect to the convex algebra structure; this is an elementary without-loss-of-generality reduction.

how reviews work

0 comments

Cite this review

Pith. "Pith review of Cancellative Convex Semilattices." pith.science (2026). https://pith.science/paper/SCBNCHRY

@misc{pith2026250711186,
  author       = {Pith},
  title        = {Pith review of: Cancellative Convex Semilattices},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/SCBNCHRY}},
  note         = {Machine review of arXiv:2507.11186}
}

read the original 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).

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

22 extracted references · 12 canonical work pages

[13]

23 Hellmuth Kneser

Id/No 2.doi:10.23638/LMCS-13(1:2)2017. 23 Hellmuth Kneser. Konvexe Räume.Arch. Math., 3:198–206,

doi:10.23638/lmcs-13(1:2)2017 2017
[15]

28 Matteo Mio and Valeria Vignudelli

doi:10.1109/LICS52264.2021.9470717. 28 Matteo Mio and Valeria Vignudelli. Monads and quantitative equational theories for non- determinism and probability. InProc. CONCUR’20, volume 171 ofLIPIcs, pages 28:1–28:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.doi:10.4230/LIPIcs.CONCUR.2020

arXiv 2021
[17]

36 Ana Sokolova and Harald Woracek

doi:10.1515/dema-2013-0332. 36 Ana Sokolova and Harald Woracek. Congruences of convex algebras.J. Pure Appl. Algebra, 219(8):3110–3148,

work page doi:10.1515/dema-2013-0332 2013
[19]

URL:http://doi.acm.org/10.1145/ 2933575.2935313, doi:10.1145/2933575.2935313. A. Sokolova and H. Woracek 12:15 38 Marshall H. Stone. Postulates for the barycentric calculus.Ann. Mat. Pura Appl. (4), 29:25–30,

arXiv
[22]

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,

work page 1985
[28]

29 Michael W. Mislove. Nondeterminism and probabilistic choice: Obeying the laws. InProc CON- CUR’00, volume 1877 ofLNCS, 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 non- determinism. In Proc. EXPRESS’03, volume 96 ofENTCS, pages 7–28. Elsevier,

doi:10.1007/3-540-44618-4
[1949]

39 Tadeusz Świrszcz

URL: http://dx.doi.org/10.1007/BF02413910, doi:10.1007/BF02413910. 39 Tadeusz Świrszcz. Monadic functors and convexity.Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys., 22:39–42,

work page doi:10.1007/bf02413910
[1952]

24 Marta Z

URL:http://dx.doi.org/ 10.1007/BF01899364, doi:10.1007/BF01899364. 24 Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Prism: Probabilistic symbolic model checker. InComputer Performance Evaluation / TOOLS, volume 2324 ofLNCS, pages 200–204,

work page doi:10.1007/bf01899364

Show all 22 references

[1977]

A storm is coming: A modern probabilistic model checker

8 Christian Dehnert, Sebastian Junges, Joost-Pieter Katoen, and Matthias Volk. A storm is coming: A modern probabilistic model checker. InProc. CAV 2017, volume 10427 ofLNCS, pages 592–600,

2017
[2006]

1016/j.ic.2006.09.001

URL: http://dx.doi.org/10.1016/j.ic.2006.09.001, 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,

2006 doi
[2008]

org/10.1016/j.ic.2008.08.002, doi:10.1016/j.ic.2008.08.002

URL:http://dx.doi. org/10.1016/j.ic.2008.08.002, doi:10.1016/j.ic.2008.08.002. 11 Jean Goubault-Larrecq. Prevision domains and convex powercones. InProc. FOSSACS’08, volume 4962 ofLNCS, pages 318–333, 2008.doi:10.1007/978-3-540-78499-9\_23. 12 Alexandre Goy and Daniela Petrisa...

2008 doi
[2009]

41 Daniele Varacca.Probability, Nondeterminism and Concurrency: Two Denotational Models for Probabilistic Computation

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,

2009 doi
[2010]

org/10.1007/978-3-642-15240-5_1, doi:10.1007/978-3-642-15240-5\_1

URL:http://dx.doi. org/10.1007/978-3-642-15240-5_1, 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.,

doi
[2015]

1016/j.jpaa.2014.10.005

URL: http://dx.doi.org/10.1016/j.jpaa.2014.10.005, 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...

2014 doi
[2016]

19 Bart Jacobs

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,

doi
[2017]

18 Jennifer Hyndman, James B

URL:http://arxiv.org/abs/ 1701.02547. 18 Jennifer Hyndman, James B. Nation, and Joy Nishida. Congruence lattices of semilattices with operators. Studia Logica, 104(2):305–316,

arXiv
[2019]

2019.8785673

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. InProc. CALCO’21, volume 211 of LIPIcs, pages 11:1–11:18,

2019
[2020]

13 Hans A

doi:10.1145/ 3373718.3394795. 13 Hans A. Hansson.Time and probability in formal design of distributed systems. PhD thesis, Uppsala University,
[2021]

4230/LIPIcs.CALCO.2021.11, doi:10.4230/LIPIcs.CALCO.2021.11

URL:https://drops.dagstuhl.de/entities/document/10. 4230/LIPIcs.CALCO.2021.11, 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 Comput...

2021 doi
[2022]

6 Pablo S

URL:https://lmcs.episciences.org/6261, 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. InProc. IJCAI’09, pages 1653–1658,

2022
[2023]

2 Christel Baier and Joost-Pieter Katoen.Principles of model checking

doi: 10.1145/3571195. 2 Christel Baier and Joost-Pieter Katoen.Principles of model checking. MIT Press,

doi
[2025]

CALCO 2025

doi: 10.1145/3704855. CALCO 2025

2025 doi

Pith tools

Reviewed August 6, 2026 · model on record in the stance chip above.

[1] [13]

23 Hellmuth Kneser

Id/No 2.doi:10.23638/LMCS-13(1:2)2017. 23 Hellmuth Kneser. Konvexe Räume.Arch. Math., 3:198–206,

doi:10.23638/lmcs-13(1:2)2017 2017

[2] [15]

28 Matteo Mio and Valeria Vignudelli

doi:10.1109/LICS52264.2021.9470717. 28 Matteo Mio and Valeria Vignudelli. Monads and quantitative equational theories for non- determinism and probability. InProc. CONCUR’20, volume 171 ofLIPIcs, pages 28:1–28:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020.doi:10.4230/LIPIcs.CONCUR.2020

arXiv 2021

[3] [17]

36 Ana Sokolova and Harald Woracek

doi:10.1515/dema-2013-0332. 36 Ana Sokolova and Harald Woracek. Congruences of convex algebras.J. Pure Appl. Algebra, 219(8):3110–3148,

work page doi:10.1515/dema-2013-0332 2013

[4] [19]

URL:http://doi.acm.org/10.1145/ 2933575.2935313, doi:10.1145/2933575.2935313. A. Sokolova and H. Woracek 12:15 38 Marshall H. Stone. Postulates for the barycentric calculus.Ann. Mat. Pura Appl. (4), 29:25–30,

arXiv

[5] [22]

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,

work page 1985

[6] [28]

29 Michael W. Mislove. Nondeterminism and probabilistic choice: Obeying the laws. InProc CON- CUR’00, volume 1877 ofLNCS, 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 non- determinism. In Proc. EXPRESS’03, volume 96 ofENTCS, pages 7–28. Elsevier,

doi:10.1007/3-540-44618-4

[7] [1949]

39 Tadeusz Świrszcz

URL: http://dx.doi.org/10.1007/BF02413910, doi:10.1007/BF02413910. 39 Tadeusz Świrszcz. Monadic functors and convexity.Bull. Acad. Polon. Sci. Sér. Sci. Math. Astronom. Phys., 22:39–42,

work page doi:10.1007/bf02413910

[8] [1952]

24 Marta Z

URL:http://dx.doi.org/ 10.1007/BF01899364, doi:10.1007/BF01899364. 24 Marta Z. Kwiatkowska, Gethin Norman, and David Parker. Prism: Probabilistic symbolic model checker. InComputer Performance Evaluation / TOOLS, volume 2324 ofLNCS, pages 200–204,

work page doi:10.1007/bf01899364