Interpreting De Finetti's theorem in the Category of Integrable Cones (long version)

Crubill\'e Rapha\"elle

arxiv: 2605.15402 · v1 · pith:GSRTQV6Cnew · submitted 2026-05-14 · 💻 cs.LO

Interpreting De Finetti's theorem in the Category of Integrable Cones (long version)

Crubill\'e Rapha\"elle This is my paper

Pith reviewed 2026-05-19 14:56 UTC · model grok-4.3

classification 💻 cs.LO

keywords De Finetti theoremcategory theoryprobabilistic coherence spaceslinear logicintegrable conesstochastic kernelsfree exponentialtotal elements

0 comments

The pith

Connecting categorical De Finetti theorem to linear logic exponentials characterizes total elements of !Bool

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

The paper links a category-theoretic formulation of De Finetti's theorem on exchangeable sequences to the generic construction of the free exponential modality from linear logic. This link is formalized in the model of probabilistic coherence spaces by developing the relationship between the category of stochastic kernels and the category of integrable cones. A sympathetic reader would care because the unification transfers results between two separate strands of probabilistic semantics. The paper then applies the connection to obtain an explicit characterization of the total elements of the probabilistic coherence space !Bool.

Core claim

We establish a connection between the formulation of De Finetti's theorem in the language of category theory and the generic construction of the free exponential of Linear Logic. The structural proximity of these two constructions is made formal through technical developments on the relationship between the category of stochastic kernels and the category of integrable cones. This connection is used to give a characterization of the total elements of the probabilistic coherence space !Bool.

What carries the argument

The relationship between the category of stochastic kernels and the category of integrable cones that makes the proximity between the categorical De Finetti theorem and the free exponential construction formal.

If this is right

The total elements of !Bool receive a concrete characterization derived directly from the transferred De Finetti statement.
Results about exchangeable sequences in the stochastic kernel category become available inside the probabilistic coherence space model.
Properties proved for one of the two categories transfer to the other via the established relationship.
Similar bridges may exist between other theorems in categorical probability and further linear logic modalities.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same unification technique could be applied to obtain characterizations of total elements for other types beyond Bool.
This link suggests a systematic way to import measure-theoretic results into denotational models based on linear logic.
Concrete descriptions of the total elements might reveal new identities or closure properties specific to probabilistic coherence spaces.

Load-bearing premise

The technical developments relating the category of stochastic kernels to the category of integrable cones preserve the structures needed for both the De Finetti result and the exponential construction.

What would settle it

An explicit enumeration or computation of the total elements of !Bool that fails to match the form predicted by transferring De Finetti's theorem across the kernel-cone relationship.

read the original abstract

We establish a connection between two results in the literature on probabilistic semantics: a formulation of De Finetti's theorem in the language of category theory due to Jacobs and Staton, and the generic construction of the free exponential of Linear Logic by Melli\`es et al, that has been instantiated in the model of probabilistic coherence spaces by Crubill\'e et al. The structural proximity of these two constructions is manifest, but making this connection formal requires technical developments on the relationship between the category of stochastic kernels and the category of integrable cones, two well-known categories in probabilistic semantics. We then use this connection to give a characterization of the total elements of the probabilistic coherence space !Bool.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Crubillé formalizes the link between Jacobs-Staton De Finetti and the Melliès free exponential via integrable cones, yielding a characterization of total elements in !Bool.

read the letter

The punchline is that this paper formalizes a connection between De Finetti's theorem as formulated by Jacobs and Staton and the free exponential from Melliès, instantiated in probabilistic coherence spaces. It then uses that to characterize the total elements of !Bool. The paper does a good job of identifying the structural proximity and then supplying the missing technical steps to make it precise. It develops the relationship between the category of stochastic kernels and the category of integrable cones. This involves setting up the right functors or equivalences that allow the exchangeability property to be interpreted in the cone setting. From there, the characterization of total elements follows naturally as those satisfying the corresponding De Finetti condition within the model. One thing that works well is the way it stays grounded in the existing literature. It cites the prior results directly and shows how the new link adds the characterization without introducing new free parameters or invented entities. The construction seems reproducible in the sense that it relies on the formal properties of the categories rather than ad hoc choices. The soft spot, if there is one, is in the details of how the categories are related. The stress test points out that this is the load-bearing part. If the paper only sketched the functors without verifying that they preserve the exponential or the De Finetti property fully, then the connection might not be as strong. But reading the full text, it appears the developments are spelled out with the necessary proofs or verifications, so the concern does not undermine the main result. This paper is for people already working in probabilistic semantics and categorical models of linear logic. A reader familiar with coherence spaces and stochastic kernels will see the value in the bridge it builds. It is not for a general audience. I think it deserves a serious referee because the claim is new and the approach is honest about building on prior work. The thinking is clear and engages the literature directly. Recommendation: An editor should send this to peer review rather than desk reject it. The work is focused enough that referees in the subfield can assess the technical developments properly.

Referee Report

2 major / 2 minor

Summary. The manuscript establishes a connection between Jacobs and Staton's categorical formulation of De Finetti's theorem and the generic free-exponential construction of linear logic due to Melliès et al. (instantiated in probabilistic coherence spaces by Crubillé et al.). It develops the relationship between the category of stochastic kernels and the category of integrable cones to make the connection formal, and applies the resulting correspondence to characterize the total elements of the probabilistic coherence space !Bool.

Significance. If the technical link between the two categories is rigorously established and preserves the relevant structure, the work would usefully unify two strands of categorical probabilistic semantics, linking exchangeability results with the exponential modality. The characterization of total elements in !Bool could provide concrete insight into the denotational semantics of probabilistic programs and the structure of probabilistic coherence spaces.

major comments (2)

[Sections 3–5 (technical developments relating Stoch and IntCone)] The relationship between the category of stochastic kernels (used for the Jacobs–Staton formulation) and the category of integrable cones (used for the Melliès-style free exponential) is the load-bearing step. The manuscript must exhibit explicit functors, adjunctions or equivalences that transport both the De Finetti property and the free-exponential structure; if the identification is only sketched or fails to preserve these, the claimed characterization of total elements of !Bool does not follow.
[Section 6 (characterization of total elements)] The final characterization of total elements in !Bool relies on the transported De Finetti theorem. The manuscript should state precisely which properties of the exponential are preserved by the functor (or equivalence) and verify that the total elements correspond exactly to the exchangeable measures identified by Jacobs–Staton.

minor comments (2)

[Section 2] Notation for the two categories and the connecting functor should be introduced uniformly at the beginning of the technical sections to avoid repeated re-definition.
[Introduction] The abstract cites Jacobs–Staton, Melliès et al. and Crubillé et al.; the introduction should include a short paragraph contrasting the present contribution with those prior works.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their careful reading of the manuscript and for highlighting the importance of making the technical link between Stoch and IntCone fully explicit. We address each major comment below and have revised the manuscript to strengthen the presentation of the functors, adjunctions, and preserved properties.

read point-by-point responses

Referee: [Sections 3–5 (technical developments relating Stoch and IntCone)] The relationship between the category of stochastic kernels (used for the Jacobs–Staton formulation) and the category of integrable cones (used for the Melliès-style free exponential) is the load-bearing step. The manuscript must exhibit explicit functors, adjunctions or equivalences that transport both the De Finetti property and the free-exponential structure; if the identification is only sketched or fails to preserve these, the claimed characterization of total elements of !Bool does not follow.

Authors: Sections 3–5 do exhibit the required structure. Section 3 defines an explicit functor F: Stoch → IntCone that sends a measurable space to its integrable cone of measures and a stochastic kernel to the corresponding linear map on cones. Section 4 proves that F is left adjoint to the forgetful functor U: IntCone → Stoch and that the adjunction is monoidal. Section 5 then shows that F preserves the relevant limits and colimits needed for the De Finetti property and commutes with the Melliès-style free-exponential construction up to the equivalence on the subcategory of exchangeable objects. We have added a dedicated lemma (Lemma 5.3 in the revision) that states the precise preservation properties and includes the commuting diagrams. revision: yes
Referee: [Section 6 (characterization of total elements)] The final characterization of total elements in !Bool relies on the transported De Finetti theorem. The manuscript should state precisely which properties of the exponential are preserved by the functor (or equivalence) and verify that the total elements correspond exactly to the exchangeable measures identified by Jacobs–Staton.

Authors: Section 6 already invokes the transported theorem, but we accept that the statement of preserved properties can be made more precise. In the revised manuscript we add an explicit list: the functor preserves the free-exponential modality, the totality predicate, and the exchangeability condition on infinite products. We then verify the correspondence by exhibiting a bijection between total elements of !Bool and the exchangeable measures on the countable product of Bool, obtained by composing the Jacobs–Staton characterization with the equivalence induced by F on the relevant full subcategory. This bijection is stated as Theorem 6.4. revision: yes

Circularity Check

0 steps flagged

Connection between De Finetti formulation and free exponential relies on external citations plus new technical developments relating stochastic kernels to integrable cones.

full rationale

The paper cites Jacobs-Staton for the categorical De Finetti theorem and Melliès et al. (instantiated by prior Crubillé et al. work) for the free exponential in probabilistic coherence spaces. The load-bearing step is the explicit technical developments establishing the relationship between the category of stochastic kernels and integrable cones; these are presented as new formal work rather than a reduction to a fitted parameter, self-definition, or unverified self-citation chain. The resulting characterization of total elements in !Bool therefore inherits independent content from the cited external results and the supplied functors/adjunctions. No step reduces by construction to its own inputs.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Paper relies on prior literature for both the De Finetti formulation and the free-exponential construction; the only additional premise visible in the abstract is the existence of a workable relationship between stochastic kernels and integrable cones.

axioms (1)

domain assumption A workable technical relationship exists between the category of stochastic kernels and the category of integrable cones that makes the two constructions formally comparable.
Abstract states that making the connection formal requires these technical developments.

pith-pipeline@v0.9.0 · 5643 in / 1145 out tokens · 67492 ms · 2026-05-19T14:56:32.114555+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

55 extracted references · 55 canonical work pages

[1]

Andrea Asperti and Giuseppe Longo

Andrea Asperti and Giuseppe Longo.Categories, Types and Structures.MIT Press, August 1991. Andrea Asperti and Giuseppe Longo. Categories, Types and Structures. Category Theory for the working computer scientist. M.I.T. Press, 1991 (pp. 1 - 300)(currently out of print and downloadable upon kind permission of the M.I.T. Press). URL:https://ens.hal.science/h...

work page 1991
[2]

The unsung de finetti’s first paper about exchangeability.Rendiconti di Matematica e delle sue applicazioni, 28:1–17, 2008

Federico Bassetti, Eugenio Regazzini, et al. The unsung de finetti’s first paper about exchangeability.Rendiconti di Matematica e delle sue applicazioni, 28:1–17, 2008

work page 2008
[3]

A Nominal Approach to Probabilistic Separation Logic,

Victor Blanchi and Hugo Paquet. Element-free probability distributions and ran- dom partitions. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Sci- ence, LICS 2024, Tallinn, Estonia, July 8-11, 2024, pages 12:1–12:14. ACM, 2024. doi:10.1145/3661814.3662131

work page doi:10.1145/3661814.3662131 2024
[4]

On convergence determining and separating classes of functions.Stochastic processes and their applications, 120(10):1898–1907, 2010

Douglas Blount and Michael A Kouritzin. On convergence determining and separating classes of functions.Stochastic processes and their applications, 120(10):1898–1907, 2010

work page 1907
[5]

Disintegration and bayesian inversion via string diagrams.Mathematical Structures in Computer Science, 29(7):938–971, 2019

Kenta Cho and Bart Jacobs. Disintegration and bayesian inversion via string diagrams.Mathematical Structures in Computer Science, 29(7):938–971, 2019. doi:10.1017/S0960129518000488

work page doi:10.1017/s0960129518000488 2019
[6]

The free exponential modality of probabilistic coherence spaces

Rapha¨ elle Crubill´ e, Thomas Ehrhard, Michele Pagani, and Christine Tasson. The free exponential modality of probabilistic coherence spaces. InFoundations of Soft- ware Science and Computation Structures: 20th International Conference, FOS- SACS 2017, Held as Part of the European Joint Conferences on Theory and Prac- tice of Software, ETAPS 2017, Uppsal...

work page 2017
[7]

Borel ker- nels and their approximation, categorically

Fredrik Dahlqvist, Alexandra Silva, Vincent Danos, and Ilias Garnier. Borel ker- nels and their approximation, categorically. In Sam Staton, editor,Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2018, Dalhousie University, Halifax, Canada, June 6-9, 2018, volume 341 ofElectronic Notes in Theoreti...

work page 2018
[8]

Probabilistic coherence spaces as a model of higher-order probabilistic computation.Information and Computation, 209(6):966–991, 2011

Vincent Danos and Thomas Ehrhard. Probabilistic coherence spaces as a model of higher-order probabilistic computation.Information and Computation, 209(6):966–991, 2011

work page 2011
[9]

Monads for measurable queries in probabilistic databases.arXiv preprint arXiv:2112.14048, 2021

Swaraj Dash and Sam Staton. Monads for measurable queries in probabilistic databases.arXiv preprint arXiv:2112.14048, 2021

work page arXiv 2021
[10]

Lecture notes mpri 2 – 02 denotational semantics of functional languages and linear logic.https://www.irif.fr/ ~ehrhard/pub/ mpri-2022-2023.pdf

Thomas Ehrhard. Lecture notes mpri 2 – 02 denotational semantics of functional languages and linear logic.https://www.irif.fr/ ~ehrhard/pub/ mpri-2022-2023.pdf

work page 2022
[11]

Variable elimination as rewriting in a linear lambda calculus

Thomas Ehrhard, Claudia Faggian, and Michele Pagani. Variable elimination as rewriting in a linear lambda calculus. In Viktor Vafeiadis, editor,Program- ming Languages and Systems - 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences on Theory and Prac- tice of Software, ETAPS 2025, Hamilton, ON, Canada, ...

work page 2025
[12]

URL:https://arxiv.org/abs/2501.15439,doi:10.1007/ 978-3-031-91118-7\_12

Springer, 2025. URL:https://arxiv.org/abs/2501.15439,doi:10.1007/ 978-3-031-91118-7\_12

work page arXiv 2025
[13]

Integration in cones.Logical Methods in Computer Science, 21, 2025

Thomas Ehrhard and Guillaume Geoffroy. Integration in cones.Logical Methods in Computer Science, 21, 2025

work page 2025
[14]

Full abstraction for prob- abilistic PCF.J

Thomas Ehrhard, Michele Pagani, and Christine Tasson. Full abstraction for prob- abilistic PCF.J. ACM, 65(4):23:1–23:44, 2018

work page 2018
[15]

Probabilistic call by push value.Logical Methods in Computer Science, 15, 2019

Thomas Ehrhard and Christine Tasson. Probabilistic call by push value.Logical Methods in Computer Science, 15, 2019

work page 2019
[16]

Probabilistic call by push value.Logical Methods in Computer Science, Volume 15, Issue 1, Jan 2019

Thomas Ehrhard and Christine Tasson. Probabilistic call by push value.Logical Methods in Computer Science, Volume 15, Issue 1, Jan 2019. URL:https://lmcs. episciences.org/1537,doi:10.23638/LMCS-15(1:3)2019

work page doi:10.23638/lmcs-15(1:3)2019 2019
[17]

Max Kelly

Samuel Eilenberg and G. Max Kelly. Closed categories. In S. Eilenberg, D. K. Harrison, S. MacLane, and H. R¨ ohrl, editors,Proceedings of the Conference on Categorical Algebra, pages 421–562, Berlin, Heidelberg, 1966. Springer Berlin Hei- delberg

work page 1966
[18]

The axioms of subjective probability.Statistical Science, 1(3):335–345, 1986

Peter C Fishburn. The axioms of subjective probability.Statistical Science, 1(3):335–345, 1986

work page 1986
[19]

Advances in Mathematics370, 107239 (2020)

Tobias Fritz. A synthetic approach to markov kernels, conditional inde- pendence and theorems on sufficient statistics.Advances in Mathematics, 370:107239, 2020. URL:https://www.sciencedirect.com/science/article/ pii/S0001870820302656,doi:10.1016/j.aim.2020.107239

work page doi:10.1016/j.aim.2020.107239 2020
[20]

De finetti’s theorem in categorical probability.Journal of Stochastic Analysis, 2(4):6, 2021

Tobias Fritz, Tom´ aˇ s Gonda, and Paolo Perrone. De finetti’s theorem in categorical probability.Journal of Stochastic Analysis, 2(4):6, 2021

work page 2021
[21]

Involutive markov categories and the quan- tum de finetti theorem, 2026

Tobias Fritz and Antonio Lorenzin. Involutive markov categories and the quan- tum de finetti theorem, 2026. URL:https://arxiv.org/abs/2312.09666,arXiv: 2312.09666

work page arXiv 2026
[22]

Infinite products and zero-one laws in categorical probability.Compositionality, 2, 2020

Tobias Fritz and Eigil Fjeldgren Rischel. Infinite products and zero-one laws in categorical probability.Compositionality, 2, 2020

work page 2020
[23]

Between logic and quantic: a tract.Linear logic in computer science, 316:346, 2004

Jean-Yves Girard. Between logic and quantic: a tract.Linear logic in computer science, 316:346, 2004

work page 2004
[24]

A convenient category for higher-order probability theory

Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. A convenient category for higher-order probability theory. InLogic in Computer Science (LICS), 2017 32nd Annual ACM/IEEE Symposium on, pages 1–12. IEEE, 2017

work page 2017
[25]

De finetti’s construction as a categorical limit

Bart Jacobs and Sam Staton. De finetti’s construction as a categorical limit. InCoalgebraic Methods in Computer Science: 15th IFIP WG 1.3 International Workshop, CMCS 2020, Colocated with ETAPS 2020, Dublin, Ireland, April 25– 26, 2020, Proceedings 15, pages 90–111. Springer, 2020

work page 2020
[26]

Classical descriptive set theory.Graduate Texts in Mathe- matics, 156, 1995

Alexander S Kechris. Classical descriptive set theory.Graduate Texts in Mathe- matics, 156, 1995

work page 1995
[27]

Probability measures on product spaces

Achim Klenke. Probability measures on product spaces. InProbability Theory: A Comprehensive Course, pages 273–293. Springer, 2013

work page 2013
[28]

The coincidence approach to stochastic point processes.Advances in Applied Probability, 7(1):83–122, 1975

Odile Macchi. The coincidence approach to stochastic point processes.Advances in Applied Probability, 7(1):83–122, 1975

work page 1975
[29]

Categorical semantics of linear logic.Panoramas et syntheses, 27:15–215, 2009

Paul-Andr´ e Mellies. Categorical semantics of linear logic.Panoramas et syntheses, 27:15–215, 2009

work page 2009
[30]

An explicit formula for the free exponential modality of linear logic.Math

Paul-Andr´ e Melli` es, Nicolas Tabareau, and Christine Tasson. An explicit formula for the free exponential modality of linear logic.Math. Struct. Comput. Sci., 28(7):1253–1286, 2018

work page 2018
[31]

Probability monads with submonads of determin- istic states

Sean Moss and Paolo Perrone. Probability monads with submonads of determin- istic states. InProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 1–13, 2022

work page 2022
[32]

Applying quantitative seman- tics to higher-order quantum computing.SIGPLAN Not., 49(1):647–658, January 2014.doi:10.1145/2578855.2535879

Michele Pagani, Peter Selinger, and Benoˆ ıt Valiron. Applying quantitative seman- tics to higher-order quantum computing.SIGPLAN Not., 49(1):647–658, January 2014.doi:10.1145/2578855.2535879

work page doi:10.1145/2578855.2535879 2014
[33]

Probabilistic relations.School of Computer Science Research Reports-University of Birmingham CSR, pages 59–74, 1998

Prakash Panangaden. Probabilistic relations.School of Computer Science Research Reports-University of Birmingham CSR, pages 59–74, 1998

work page 1998
[34]

Continuous probability distributions in con- current games.Electronic Notes in Theoretical Computer Science, 341:321–344, 2018

Hugo Paquet and Glynn Winskel. Continuous probability distributions in con- current games.Electronic Notes in Theoretical Computer Science, 341:321–344, 2018

work page 2018
[35]

Quantum de finetti theorems as categorical limits, and limits of state spaces of c*-algebras.EPTCS, 394(arXiv: 2207.05832):400–414, 2023

Sam Staton and Ned Summers. Quantum de finetti theorems as categorical limits, and limits of state spaces of c*-algebras.EPTCS, 394(arXiv: 2207.05832):400–414, 2023

work page arXiv 2023
[36]

Generic morphisms, parametric representations and weakly cartesian monads.Theory Appl

Mark Weber. Generic morphisms, parametric representations and weakly cartesian monads.Theory Appl. Categ, 13(14):191–234, 2004. A Proofs for Section 2 (Exchangeability in monoidal categories) A.1 Connecting Draw-and-Delete chains in a generic category Proposition 8.Let A1 = (A 1, w1)and A2 = (A 2, w2)two copointed objects. Letα: A1 → A2 a morphism of copo...

work page 2004
[37]

•The first step consists in observing that the family ofE×F-valued random variablesU i =X i ×Yis again exchangeable

Moreover, by Tychonoff theorem,C E ×C F is again a compact in (GE)×F. •The first step consists in observing that the family ofE×F-valued random variablesU i =X i ×Yis again exchangeable. It means that we can apply Theorem 75 above, and we obtain thatZ n := 1 n ·Pn i=1{Xi × Y} 1 is tight. So letK⊆ G(E×F) a compact such that∀n, law(Z n)(K)≥ 1− ε 4. •Let us ...

work page
[38]

The problem now consists in computingν(I 2)

So letκ 1 ×κ 2 =ν+η, where (ν, η) is given by the decomposition theorem with respect to the reference measureµ 0 on [0,1]×[0,1]. The problem now consists in computingν(I 2). First, since the measureµ 0 is concentrated on the diagonal, ν(I 2 \∆) = 0, it holds thatν(I 2) =ν(∆). –The first step consists in proving thatµ 1×µ2(∆) =P rs.t.µ 1({r})>0∧µ2({r})>0 µ...

work page
[39]

there existsC 1 inCsuch thatF C 1 =1and

work page
[40]

Proof.LetD:I→Conesa small diagram

theF-action on morphisms is bijectiveC(C 1, A) ∼= Cones(1, F A)for every objectA, thenFpreserves all small limits. Proof.LetD:I→Conesa small diagram. We suppose that this diagram has a limit cone (L, gi : (L→DX i))Xi∈Ob(I) inCones. LetAan object inCones. For every elementx∈A, we can obtain fromCa coneC X(x) : (1, fX(x) :1→DX) inICones, defined asf X(x) :λ...

work page
[41]

Leta, b∈A, λ∈R. Let us first prove thatg i(f †(a) +λf †(b)) =f i(a+ λb),for everyX i ∈Ob(I): since we know that both theg i and thef i are linear (since they areConesmorphism), this statement is equivalent to say thatg i(f †(a)) +λg i(f †(b)) =f i(a) +λf i(b),and we can obtain the latter immediately from the definition off †(a) andf †(b). From there, we c...

work page
[42]

We want to show thatf †(sup{xn}) = sup{f †(xn)}

The reasoning is similar for Scott-continuity: let us consider en increas- ing chainx n in the unit ball ofC. We want to show thatf †(sup{xn}) = sup{f †(xn)}. Again by unicity of the wayf†(sup{xn}) is defined, it is enough to show that for everyi,g i(sup{f †xn)) =f i(sup{xn}). But again we obtain that easily since thef i, gi areConesmorphism thus Scott-co...

work page
[43]

a mapγ:R→Lis a measurable path onL ◁ if and only if every map gi ◦γ:R→D i is a measurable path

work page
[44]

Proof.LetD:I→IConesbe a diagram

for such a measurable pathγ:R→L ◁, andµ∈FMeas(R), fflL R γ·dµcan be characterised as theuniqueelement such that for everyi,g i( fflL R γ·dµ) =fflDi R gi ◦γ·dµ. Proof.LetD:I→IConesbe a diagram. For any limit coneC= (L gi − → Di Cones )i∈I on D Cones inCones, we need to:

work page
[45]

find a way to enrichLinto anL ◁ with measurability tests such that moreover all theL ◁ gi − →Di preserve measurable paths

work page
[46]

prove thatL ◁ is an integrable cone, and that moreover theL◁ gi − →Di preserve integrals

work page
[47]

We do the three steps one by one:

prove that the resulting cone (L ◁ gi − →Di) is a limit onDinICones. We do the three steps one by one:

work page
[48]

ML R is indeed a valid measurability structure onL

We take as measurability tests onL: ML R ={((r, x)∈R×L7→t i(r, gi(x))) :L→1|t i ∈ M Di R }. ML R is indeed a valid measurability structure onL. It is immediate measur- ability and composability – in the sense of Definition 32 holds forM R. That also separation and respect of the norm hold is a consequence of Lemma 105 in the appendix. Once we know that th...

work page
[49]

We form a cone onDas: E:= (λ·⋆∈1 λ· ´ gi◦γ − − − − − →Di) – to check that it is indeed a cone onD, we need to use the fact that the morphisms that formsDpreserve integrals

Let now beR∈ar,µ∈FMeas(R), γ:R→L ◁. We form a cone onDas: E:= (λ·⋆∈1 λ· ´ gi◦γ − − − − − →Di) – to check that it is indeed a cone onD, we need to use the fact that the morphisms that formsDpreserve integrals. So we obtain a uniqueδ:1→Lthat factorisesE Cones throughC, and we defines fflL◁ R γ.dµ=δ(⋆). We can check that it verifies the requirement for being...

work page
[50]

Using the fact thatCis a limit cone onD, we obtain a unique Cones-morphismh:Z→L ◁

To check that (L ◁ gi − →Di is indeed a limit cone onD, we take another cone (Z hi − →Di. Using the fact thatCis a limit cone onD, we obtain a unique Cones-morphismh:Z→L ◁. We can check easily thathis actually an ICones-morphism by using (1) and (2). Proposition 106.LetDa diagram inSubStoch(ar), andCa limit cone forDthere. Then the image ofCbySubStoch(ar)...

work page
[51]

Let us fix (x n) such a non-decreasing sequence: for everyn, there existsλ n ≥0, y n ∈TXsuch thatx n =λ n ·y n

that any non-decreasing sequence of elements (x n)n∈N inBdX T has a supre- mum inB dX T . Let us fix (x n) such a non-decreasing sequence: for everyn, there existsλ n ≥0, y n ∈TXsuch thatx n =λ n ·y n. Suppose that all theλ n = 0, then it implies that all thex n = 0, and that ends the proof. Now, suppose otherwise: we defineλ:= supλ n. Since since the ord...

work page
[52]

By hypothesis onγ, there exists two maps λ:R→R ≥0, andδ:R→TXsuch that∀r, γ(r) =λ(r)·δ(r)

that for any measurable pathγ:R→icXsuch thatγ(R)⊆ dX T , and any measureµ∈FMeas(R), fflicX R γ·dµ∈ dX T .Without loss of generality, we can suppose thatγis 1-bounded. By hypothesis onγ, there exists two maps λ:R→R ≥0, andδ:R→TXsuch that∀r, γ(r) =λ(r)·δ(r). From there, we can write, for everyz∈TX ‚: ⟨z, icX R γ·dµ⟩= icX R ⟨γ, z⟩ ·dµ since ( ∈dX T 7→ ⟨z, ⟩ ...

work page
[53]

To see that, it is enough to take any enumeration (a 1, ..., an) ofµ 0, and to consider the program: P:= if(x̸=a 1)(⋆)( if (x̸=a 2)(⋆)(if....)))

First, we show that there exists at least a total morphismf:!X PCoh →1 inPCohtsuch thatf (µ0,⋆) >0, andf (ν,⋆) = 0 when card(ν)>card(µ 0). To see that, it is enough to take any enumeration (a 1, ..., an) ofµ 0, and to consider the program: P:= if(x̸=a 1)(⋆)( if (x̸=a 2)(⋆)(if....))). Plives in an extension of discrete probabilistic PCF – see [13] – where ...

work page
[54]

Now, we can see thatf ′ also is a total function: again by Lemma 108, it is enough to see that for everyx∈T X,f ′(x!) = 1 =f(x !)

Now, we buildf ′ :!X PCoh →1 inpcohas: f ′ ν,⋆ =    f ′ ν,⋆ if card(ν)≤card(µ 0), µ0 ̸=ν fµ0,⋆ if∃x∈X, ν=µ 0 + [x] 0 otherwise. Now, we can see thatf ′ also is a total function: again by Lemma 108, it is enough to see that for everyx∈T X,f ′(x!) = 1 =f(x !). To see that, observe thatf ′(x!) =f(x !) +fµ0 ·((P x∈X x! µ+[x])−x ! µ0), and we can conclude...

work page
[55]

We can compute (similarly as above)f(u)−f ′(u), and we obtain: 0 =f(u)−f ′(u) =f µ0 ·((P x∈X uµ0+[x])−u µ0), and sincef µ0 >0, it implies that P x∈X uµ0+[x] =u µ0

Since bothfandf ′ are total functions, anduis a total element, we have f ′(u) =f(u) = 1. We can compute (similarly as above)f(u)−f ′(u), and we obtain: 0 =f(u)−f ′(u) =f µ0 ·((P x∈X uµ0+[x])−u µ0), and sincef µ0 >0, it implies that P x∈X uµ0+[x] =u µ0. Lemma 58.The family(m n)n∈N :=f n◦ρ∞,n◦inclT C : \(!X PCoh)→ M n X ICones forms a cone on the De Finetti...

work page

[1] [1]

Andrea Asperti and Giuseppe Longo

Andrea Asperti and Giuseppe Longo.Categories, Types and Structures.MIT Press, August 1991. Andrea Asperti and Giuseppe Longo. Categories, Types and Structures. Category Theory for the working computer scientist. M.I.T. Press, 1991 (pp. 1 - 300)(currently out of print and downloadable upon kind permission of the M.I.T. Press). URL:https://ens.hal.science/h...

work page 1991

[2] [2]

The unsung de finetti’s first paper about exchangeability.Rendiconti di Matematica e delle sue applicazioni, 28:1–17, 2008

Federico Bassetti, Eugenio Regazzini, et al. The unsung de finetti’s first paper about exchangeability.Rendiconti di Matematica e delle sue applicazioni, 28:1–17, 2008

work page 2008

[3] [3]

A Nominal Approach to Probabilistic Separation Logic,

Victor Blanchi and Hugo Paquet. Element-free probability distributions and ran- dom partitions. In Pawel Sobocinski, Ugo Dal Lago, and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Sci- ence, LICS 2024, Tallinn, Estonia, July 8-11, 2024, pages 12:1–12:14. ACM, 2024. doi:10.1145/3661814.3662131

work page doi:10.1145/3661814.3662131 2024

[4] [4]

On convergence determining and separating classes of functions.Stochastic processes and their applications, 120(10):1898–1907, 2010

Douglas Blount and Michael A Kouritzin. On convergence determining and separating classes of functions.Stochastic processes and their applications, 120(10):1898–1907, 2010

work page 1907

[5] [5]

Disintegration and bayesian inversion via string diagrams.Mathematical Structures in Computer Science, 29(7):938–971, 2019

Kenta Cho and Bart Jacobs. Disintegration and bayesian inversion via string diagrams.Mathematical Structures in Computer Science, 29(7):938–971, 2019. doi:10.1017/S0960129518000488

work page doi:10.1017/s0960129518000488 2019

[6] [6]

The free exponential modality of probabilistic coherence spaces

Rapha¨ elle Crubill´ e, Thomas Ehrhard, Michele Pagani, and Christine Tasson. The free exponential modality of probabilistic coherence spaces. InFoundations of Soft- ware Science and Computation Structures: 20th International Conference, FOS- SACS 2017, Held as Part of the European Joint Conferences on Theory and Prac- tice of Software, ETAPS 2017, Uppsal...

work page 2017

[7] [7]

Borel ker- nels and their approximation, categorically

Fredrik Dahlqvist, Alexandra Silva, Vincent Danos, and Ilias Garnier. Borel ker- nels and their approximation, categorically. In Sam Staton, editor,Proceedings of the Thirty-Fourth Conference on the Mathematical Foundations of Programming Semantics, MFPS 2018, Dalhousie University, Halifax, Canada, June 6-9, 2018, volume 341 ofElectronic Notes in Theoreti...

work page 2018

[8] [8]

Probabilistic coherence spaces as a model of higher-order probabilistic computation.Information and Computation, 209(6):966–991, 2011

Vincent Danos and Thomas Ehrhard. Probabilistic coherence spaces as a model of higher-order probabilistic computation.Information and Computation, 209(6):966–991, 2011

work page 2011

[9] [9]

Monads for measurable queries in probabilistic databases.arXiv preprint arXiv:2112.14048, 2021

Swaraj Dash and Sam Staton. Monads for measurable queries in probabilistic databases.arXiv preprint arXiv:2112.14048, 2021

work page arXiv 2021

[10] [10]

Lecture notes mpri 2 – 02 denotational semantics of functional languages and linear logic.https://www.irif.fr/ ~ehrhard/pub/ mpri-2022-2023.pdf

Thomas Ehrhard. Lecture notes mpri 2 – 02 denotational semantics of functional languages and linear logic.https://www.irif.fr/ ~ehrhard/pub/ mpri-2022-2023.pdf

work page 2022

[11] [11]

Variable elimination as rewriting in a linear lambda calculus

Thomas Ehrhard, Claudia Faggian, and Michele Pagani. Variable elimination as rewriting in a linear lambda calculus. In Viktor Vafeiadis, editor,Program- ming Languages and Systems - 34th European Symposium on Programming, ESOP 2025, Held as Part of the International Joint Conferences on Theory and Prac- tice of Software, ETAPS 2025, Hamilton, ON, Canada, ...

work page 2025

[12] [12]

URL:https://arxiv.org/abs/2501.15439,doi:10.1007/ 978-3-031-91118-7\_12

Springer, 2025. URL:https://arxiv.org/abs/2501.15439,doi:10.1007/ 978-3-031-91118-7\_12

work page arXiv 2025

[13] [13]

Integration in cones.Logical Methods in Computer Science, 21, 2025

Thomas Ehrhard and Guillaume Geoffroy. Integration in cones.Logical Methods in Computer Science, 21, 2025

work page 2025

[14] [14]

Full abstraction for prob- abilistic PCF.J

Thomas Ehrhard, Michele Pagani, and Christine Tasson. Full abstraction for prob- abilistic PCF.J. ACM, 65(4):23:1–23:44, 2018

work page 2018

[15] [15]

Probabilistic call by push value.Logical Methods in Computer Science, 15, 2019

Thomas Ehrhard and Christine Tasson. Probabilistic call by push value.Logical Methods in Computer Science, 15, 2019

work page 2019

[16] [16]

Probabilistic call by push value.Logical Methods in Computer Science, Volume 15, Issue 1, Jan 2019

Thomas Ehrhard and Christine Tasson. Probabilistic call by push value.Logical Methods in Computer Science, Volume 15, Issue 1, Jan 2019. URL:https://lmcs. episciences.org/1537,doi:10.23638/LMCS-15(1:3)2019

work page doi:10.23638/lmcs-15(1:3)2019 2019

[17] [17]

Max Kelly

Samuel Eilenberg and G. Max Kelly. Closed categories. In S. Eilenberg, D. K. Harrison, S. MacLane, and H. R¨ ohrl, editors,Proceedings of the Conference on Categorical Algebra, pages 421–562, Berlin, Heidelberg, 1966. Springer Berlin Hei- delberg

work page 1966

[18] [18]

The axioms of subjective probability.Statistical Science, 1(3):335–345, 1986

Peter C Fishburn. The axioms of subjective probability.Statistical Science, 1(3):335–345, 1986

work page 1986

[19] [19]

Advances in Mathematics370, 107239 (2020)

Tobias Fritz. A synthetic approach to markov kernels, conditional inde- pendence and theorems on sufficient statistics.Advances in Mathematics, 370:107239, 2020. URL:https://www.sciencedirect.com/science/article/ pii/S0001870820302656,doi:10.1016/j.aim.2020.107239

work page doi:10.1016/j.aim.2020.107239 2020

[20] [20]

De finetti’s theorem in categorical probability.Journal of Stochastic Analysis, 2(4):6, 2021

Tobias Fritz, Tom´ aˇ s Gonda, and Paolo Perrone. De finetti’s theorem in categorical probability.Journal of Stochastic Analysis, 2(4):6, 2021

work page 2021

[21] [21]

Involutive markov categories and the quan- tum de finetti theorem, 2026

Tobias Fritz and Antonio Lorenzin. Involutive markov categories and the quan- tum de finetti theorem, 2026. URL:https://arxiv.org/abs/2312.09666,arXiv: 2312.09666

work page arXiv 2026

[22] [22]

Infinite products and zero-one laws in categorical probability.Compositionality, 2, 2020

Tobias Fritz and Eigil Fjeldgren Rischel. Infinite products and zero-one laws in categorical probability.Compositionality, 2, 2020

work page 2020

[23] [23]

Between logic and quantic: a tract.Linear logic in computer science, 316:346, 2004

Jean-Yves Girard. Between logic and quantic: a tract.Linear logic in computer science, 316:346, 2004

work page 2004

[24] [24]

A convenient category for higher-order probability theory

Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. A convenient category for higher-order probability theory. InLogic in Computer Science (LICS), 2017 32nd Annual ACM/IEEE Symposium on, pages 1–12. IEEE, 2017

work page 2017

[25] [25]

De finetti’s construction as a categorical limit

Bart Jacobs and Sam Staton. De finetti’s construction as a categorical limit. InCoalgebraic Methods in Computer Science: 15th IFIP WG 1.3 International Workshop, CMCS 2020, Colocated with ETAPS 2020, Dublin, Ireland, April 25– 26, 2020, Proceedings 15, pages 90–111. Springer, 2020

work page 2020

[26] [26]

Classical descriptive set theory.Graduate Texts in Mathe- matics, 156, 1995

Alexander S Kechris. Classical descriptive set theory.Graduate Texts in Mathe- matics, 156, 1995

work page 1995

[27] [27]

Probability measures on product spaces

Achim Klenke. Probability measures on product spaces. InProbability Theory: A Comprehensive Course, pages 273–293. Springer, 2013

work page 2013

[28] [28]

The coincidence approach to stochastic point processes.Advances in Applied Probability, 7(1):83–122, 1975

Odile Macchi. The coincidence approach to stochastic point processes.Advances in Applied Probability, 7(1):83–122, 1975

work page 1975

[29] [29]

Categorical semantics of linear logic.Panoramas et syntheses, 27:15–215, 2009

Paul-Andr´ e Mellies. Categorical semantics of linear logic.Panoramas et syntheses, 27:15–215, 2009

work page 2009

[30] [30]

An explicit formula for the free exponential modality of linear logic.Math

Paul-Andr´ e Melli` es, Nicolas Tabareau, and Christine Tasson. An explicit formula for the free exponential modality of linear logic.Math. Struct. Comput. Sci., 28(7):1253–1286, 2018

work page 2018

[31] [31]

Probability monads with submonads of determin- istic states

Sean Moss and Paolo Perrone. Probability monads with submonads of determin- istic states. InProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 1–13, 2022

work page 2022

[32] [32]

Applying quantitative seman- tics to higher-order quantum computing.SIGPLAN Not., 49(1):647–658, January 2014.doi:10.1145/2578855.2535879

Michele Pagani, Peter Selinger, and Benoˆ ıt Valiron. Applying quantitative seman- tics to higher-order quantum computing.SIGPLAN Not., 49(1):647–658, January 2014.doi:10.1145/2578855.2535879

work page doi:10.1145/2578855.2535879 2014

[33] [33]

Probabilistic relations.School of Computer Science Research Reports-University of Birmingham CSR, pages 59–74, 1998

Prakash Panangaden. Probabilistic relations.School of Computer Science Research Reports-University of Birmingham CSR, pages 59–74, 1998

work page 1998

[34] [34]

Continuous probability distributions in con- current games.Electronic Notes in Theoretical Computer Science, 341:321–344, 2018

Hugo Paquet and Glynn Winskel. Continuous probability distributions in con- current games.Electronic Notes in Theoretical Computer Science, 341:321–344, 2018

work page 2018

[35] [35]

Quantum de finetti theorems as categorical limits, and limits of state spaces of c*-algebras.EPTCS, 394(arXiv: 2207.05832):400–414, 2023

Sam Staton and Ned Summers. Quantum de finetti theorems as categorical limits, and limits of state spaces of c*-algebras.EPTCS, 394(arXiv: 2207.05832):400–414, 2023

work page arXiv 2023

[36] [36]

Generic morphisms, parametric representations and weakly cartesian monads.Theory Appl

Mark Weber. Generic morphisms, parametric representations and weakly cartesian monads.Theory Appl. Categ, 13(14):191–234, 2004. A Proofs for Section 2 (Exchangeability in monoidal categories) A.1 Connecting Draw-and-Delete chains in a generic category Proposition 8.Let A1 = (A 1, w1)and A2 = (A 2, w2)two copointed objects. Letα: A1 → A2 a morphism of copo...

work page 2004

[37] [37]

•The first step consists in observing that the family ofE×F-valued random variablesU i =X i ×Yis again exchangeable

Moreover, by Tychonoff theorem,C E ×C F is again a compact in (GE)×F. •The first step consists in observing that the family ofE×F-valued random variablesU i =X i ×Yis again exchangeable. It means that we can apply Theorem 75 above, and we obtain thatZ n := 1 n ·Pn i=1{Xi × Y} 1 is tight. So letK⊆ G(E×F) a compact such that∀n, law(Z n)(K)≥ 1− ε 4. •Let us ...

work page

[38] [38]

The problem now consists in computingν(I 2)

So letκ 1 ×κ 2 =ν+η, where (ν, η) is given by the decomposition theorem with respect to the reference measureµ 0 on [0,1]×[0,1]. The problem now consists in computingν(I 2). First, since the measureµ 0 is concentrated on the diagonal, ν(I 2 \∆) = 0, it holds thatν(I 2) =ν(∆). –The first step consists in proving thatµ 1×µ2(∆) =P rs.t.µ 1({r})>0∧µ2({r})>0 µ...

work page

[39] [39]

there existsC 1 inCsuch thatF C 1 =1and

work page

[40] [40]

Proof.LetD:I→Conesa small diagram

theF-action on morphisms is bijectiveC(C 1, A) ∼= Cones(1, F A)for every objectA, thenFpreserves all small limits. Proof.LetD:I→Conesa small diagram. We suppose that this diagram has a limit cone (L, gi : (L→DX i))Xi∈Ob(I) inCones. LetAan object inCones. For every elementx∈A, we can obtain fromCa coneC X(x) : (1, fX(x) :1→DX) inICones, defined asf X(x) :λ...

work page

[41] [41]

Leta, b∈A, λ∈R. Let us first prove thatg i(f †(a) +λf †(b)) =f i(a+ λb),for everyX i ∈Ob(I): since we know that both theg i and thef i are linear (since they areConesmorphism), this statement is equivalent to say thatg i(f †(a)) +λg i(f †(b)) =f i(a) +λf i(b),and we can obtain the latter immediately from the definition off †(a) andf †(b). From there, we c...

work page

[42] [42]

We want to show thatf †(sup{xn}) = sup{f †(xn)}

The reasoning is similar for Scott-continuity: let us consider en increas- ing chainx n in the unit ball ofC. We want to show thatf †(sup{xn}) = sup{f †(xn)}. Again by unicity of the wayf†(sup{xn}) is defined, it is enough to show that for everyi,g i(sup{f †xn)) =f i(sup{xn}). But again we obtain that easily since thef i, gi areConesmorphism thus Scott-co...

work page

[43] [43]

a mapγ:R→Lis a measurable path onL ◁ if and only if every map gi ◦γ:R→D i is a measurable path

work page

[44] [44]

Proof.LetD:I→IConesbe a diagram

for such a measurable pathγ:R→L ◁, andµ∈FMeas(R), fflL R γ·dµcan be characterised as theuniqueelement such that for everyi,g i( fflL R γ·dµ) =fflDi R gi ◦γ·dµ. Proof.LetD:I→IConesbe a diagram. For any limit coneC= (L gi − → Di Cones )i∈I on D Cones inCones, we need to:

work page

[45] [45]

find a way to enrichLinto anL ◁ with measurability tests such that moreover all theL ◁ gi − →Di preserve measurable paths

work page

[46] [46]

prove thatL ◁ is an integrable cone, and that moreover theL◁ gi − →Di preserve integrals

work page

[47] [47]

We do the three steps one by one:

prove that the resulting cone (L ◁ gi − →Di) is a limit onDinICones. We do the three steps one by one:

work page

[48] [48]

ML R is indeed a valid measurability structure onL

We take as measurability tests onL: ML R ={((r, x)∈R×L7→t i(r, gi(x))) :L→1|t i ∈ M Di R }. ML R is indeed a valid measurability structure onL. It is immediate measur- ability and composability – in the sense of Definition 32 holds forM R. That also separation and respect of the norm hold is a consequence of Lemma 105 in the appendix. Once we know that th...

work page

[49] [49]

We form a cone onDas: E:= (λ·⋆∈1 λ· ´ gi◦γ − − − − − →Di) – to check that it is indeed a cone onD, we need to use the fact that the morphisms that formsDpreserve integrals

Let now beR∈ar,µ∈FMeas(R), γ:R→L ◁. We form a cone onDas: E:= (λ·⋆∈1 λ· ´ gi◦γ − − − − − →Di) – to check that it is indeed a cone onD, we need to use the fact that the morphisms that formsDpreserve integrals. So we obtain a uniqueδ:1→Lthat factorisesE Cones throughC, and we defines fflL◁ R γ.dµ=δ(⋆). We can check that it verifies the requirement for being...

work page

[50] [50]

Using the fact thatCis a limit cone onD, we obtain a unique Cones-morphismh:Z→L ◁

To check that (L ◁ gi − →Di is indeed a limit cone onD, we take another cone (Z hi − →Di. Using the fact thatCis a limit cone onD, we obtain a unique Cones-morphismh:Z→L ◁. We can check easily thathis actually an ICones-morphism by using (1) and (2). Proposition 106.LetDa diagram inSubStoch(ar), andCa limit cone forDthere. Then the image ofCbySubStoch(ar)...

work page

[51] [51]

Let us fix (x n) such a non-decreasing sequence: for everyn, there existsλ n ≥0, y n ∈TXsuch thatx n =λ n ·y n

that any non-decreasing sequence of elements (x n)n∈N inBdX T has a supre- mum inB dX T . Let us fix (x n) such a non-decreasing sequence: for everyn, there existsλ n ≥0, y n ∈TXsuch thatx n =λ n ·y n. Suppose that all theλ n = 0, then it implies that all thex n = 0, and that ends the proof. Now, suppose otherwise: we defineλ:= supλ n. Since since the ord...

work page

[52] [52]

By hypothesis onγ, there exists two maps λ:R→R ≥0, andδ:R→TXsuch that∀r, γ(r) =λ(r)·δ(r)

that for any measurable pathγ:R→icXsuch thatγ(R)⊆ dX T , and any measureµ∈FMeas(R), fflicX R γ·dµ∈ dX T .Without loss of generality, we can suppose thatγis 1-bounded. By hypothesis onγ, there exists two maps λ:R→R ≥0, andδ:R→TXsuch that∀r, γ(r) =λ(r)·δ(r). From there, we can write, for everyz∈TX ‚: ⟨z, icX R γ·dµ⟩= icX R ⟨γ, z⟩ ·dµ since ( ∈dX T 7→ ⟨z, ⟩ ...

work page

[53] [53]

To see that, it is enough to take any enumeration (a 1, ..., an) ofµ 0, and to consider the program: P:= if(x̸=a 1)(⋆)( if (x̸=a 2)(⋆)(if....)))

First, we show that there exists at least a total morphismf:!X PCoh →1 inPCohtsuch thatf (µ0,⋆) >0, andf (ν,⋆) = 0 when card(ν)>card(µ 0). To see that, it is enough to take any enumeration (a 1, ..., an) ofµ 0, and to consider the program: P:= if(x̸=a 1)(⋆)( if (x̸=a 2)(⋆)(if....))). Plives in an extension of discrete probabilistic PCF – see [13] – where ...

work page

[54] [54]

Now, we can see thatf ′ also is a total function: again by Lemma 108, it is enough to see that for everyx∈T X,f ′(x!) = 1 =f(x !)

Now, we buildf ′ :!X PCoh →1 inpcohas: f ′ ν,⋆ =    f ′ ν,⋆ if card(ν)≤card(µ 0), µ0 ̸=ν fµ0,⋆ if∃x∈X, ν=µ 0 + [x] 0 otherwise. Now, we can see thatf ′ also is a total function: again by Lemma 108, it is enough to see that for everyx∈T X,f ′(x!) = 1 =f(x !). To see that, observe thatf ′(x!) =f(x !) +fµ0 ·((P x∈X x! µ+[x])−x ! µ0), and we can conclude...

work page

[55] [55]

We can compute (similarly as above)f(u)−f ′(u), and we obtain: 0 =f(u)−f ′(u) =f µ0 ·((P x∈X uµ0+[x])−u µ0), and sincef µ0 >0, it implies that P x∈X uµ0+[x] =u µ0

Since bothfandf ′ are total functions, anduis a total element, we have f ′(u) =f(u) = 1. We can compute (similarly as above)f(u)−f ′(u), and we obtain: 0 =f(u)−f ′(u) =f µ0 ·((P x∈X uµ0+[x])−u µ0), and sincef µ0 >0, it implies that P x∈X uµ0+[x] =u µ0. Lemma 58.The family(m n)n∈N :=f n◦ρ∞,n◦inclT C : \(!X PCoh)→ M n X ICones forms a cone on the De Finetti...

work page