Double Glueing over Free Exponential: with Measure Theoretic Applications

Masahiro Hamano

arxiv: 2107.07726 · v7 · submitted 2021-07-16 · 💻 cs.LO · math.CT

Double Glueing over Free Exponential: with Measure Theoretic Applications

Masahiro Hamano This is my paper

Pith reviewed 2026-05-24 13:33 UTC · model grok-4.3

classification 💻 cs.LO math.CT

keywords double glueingfree exponentialorthogonalitys-finite transition kernelsprobabilistic coherent spaceslinear logicLebesgue integralmeasure theory

0 comments

The pith

Reciprocity of orthogonality lifts the free exponential over Hyland-Schalk double glueing in s-finite kernel categories.

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

The paper introduces a reciprocity condition on orthogonality that suffices to lift the free exponential construction of Mellies-Tabareau-Tasson over the double glueing of Hyland and Schalk. The method is instantiated on the monoidal category TsK of s-finite transition kernels with countable biproducts, where the opposite category admits a free exponential that admits a direct description in measure theory. An orthogonality relation between measures and measurable functions is defined via Lebesgue integrals and shown to be reciprocal, so the free exponential lifts to the orthogonality category O_I(TsK^op). This lifted structure contains Ehrhard et al.'s probabilistic coherent spaces as a full subcategory on countable measurable spaces. The lifting step relies on the uniform convergence theorem commuting integrals and limits together with the Fubini-Tonelli theorem for double integrals under s-finiteness.

Core claim

The reciprocity of orthogonality allows lifting the free exponential over the double glueing in terms of the orthogonality. In TsK the opposite category TsK^op possesses the free exponential, which is describable in terms of measure theory. The orthogonality between measures and measurable functions defined via Lebesgue integrals is reciprocal; therefore the free exponential lifts to O_I(TsK^op), which subsumes probabilistic coherent spaces as a full subcategory of countable measurable spaces. The measure-theoretic uniform convergence theorem and Fubini-Tonelli theorem are used to establish the lifting.

What carries the argument

The reciprocity of orthogonality condition, defined so that it directly lifts the free exponential over double glueing in terms of the orthogonality relation.

If this is right

TsK^op admits a free exponential that is expressible directly in measure-theoretic language.
The Lebesgue-integral orthogonality on s-finite kernels is reciprocal and therefore lifts.
The lifted free exponential in O_I(TsK^op) contains probabilistic coherent spaces on countable spaces as a full subcategory.
The two-layer decomposition of the direct free exponential of Crubille et al. follows from the lifted construction.

Where Pith is reading between the lines

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

The same reciprocity test may be checked in other integral-based orthogonality relations to obtain lifted exponentials without redoing the categorical construction.
The continuous version of orthogonality supplies a bridge between discrete probabilistic coherent spaces and general measurable-space models of linear logic.
The measure-theoretic description may allow direct transfer of analytic tools such as dominated convergence into the syntax of linear logic.

Load-bearing premise

The orthogonality defined via Lebesgue integrals on s-finite transition kernels satisfies the reciprocity condition.

What would settle it

An explicit pair of measures and measurable functions in TsK for which the Lebesgue integral fails to commute with the pointwise limit under uniform convergence would prevent the reciprocity condition from holding and block the lifting.

read the original abstract

This paper provides a compact method to lift the free exponential construction of Mellies-Tabareau-Tasson over the Hyland-Schalk double glueing for orthogonality categories. A condition ``reciprocity of orthogonality'' is presented simply enough to lift the free exponential over the double glueing in terms of the orthogonality. Our general method applies to the monoidal category TsK of the s-finite transition kernels with countable biproducts. We show (i) TsK^op has the free exponential, which is shown to be describable in terms of measure theory. (ii) The s-finite transition kernels have an orthogonality between measures and measurable functions in terms of Lebesgue integrals. The orthogonality is reciprocal, hence the free exponential of (i) lifts to the orthogonality category O_I(TsK^op), which subsumes Ehrhard et al's probabilistic coherent spaces as a full subcategory of countable measurable spaces. To lift the free exponential, the measure-theoretic uniform convergence theorem commuting Lebesgue integral and limit plays a crucial role as well as Fubini-Tonelli theorem for double integral in s-finiteness. Our measure-theoretic orthogonality is considered as a continuous version of the orthogonality of the probabilistic coherent spaces for linear logic, and in particular provides a two layered decomposition of Crubille et al's direct free exponential for these spaces.

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

The paper gives a compact reciprocity condition to lift the MTT free exponential over HS double glueing and verifies it for s-finite kernels to get a measure-theoretic model containing probabilistic coherent spaces.

read the letter

The main takeaway is that reciprocity of orthogonality is enough to lift the Mellies-Tabareau-Tasson free exponential over Hyland-Schalk double glueing, and the authors carry this out explicitly for the opposite of the s-finite transition kernel category. They describe the free exponential in measure-theoretic terms and define an orthogonality via Lebesgue integrals that satisfies the reciprocity condition, using uniform convergence to move limits inside integrals and Fubini-Tonelli for the s-finiteness double integrals. The lifted structure subsumes probabilistic coherent spaces on countable spaces as a full subcategory and gives a layered view of Crubille et al's direct construction. This is the actual new piece: a general lifting method plus its concrete verification in the measure setting. The paper does this cleanly and cites the right prior results without overclaiming. The soft spots are limited. The argument depends on the standard measure theorems applying directly to s-finite kernels, and the stress-test confirms there are no extra hidden restrictions, so the central claim holds. Edge cases on non-standard measurable spaces might still need checking in a revision, but nothing load-bearing appears broken. This is for people working on categorical models of probabilistic computation and linear logic semantics. A reader who wants to see how discrete and continuous models can be unified through orthogonality categories will get something concrete from it. The work is formally grounded enough and the application is sharp enough to deserve referee time.

Referee Report

0 major / 3 minor

Summary. The paper presents a compact method to lift the free exponential construction of Mellies-Tabareau-Tasson over the Hyland-Schalk double glueing using a reciprocity condition on orthogonality. It applies the method to the opposite of the category TsK of s-finite transition kernels (with countable biproducts), showing that TsK^op admits a free exponential describable via measure theory, that the Lebesgue-integral orthogonality between measures and measurable functions is reciprocal, and that the lifted free exponential in the orthogonality category O_I(TsK^op) subsumes probabilistic coherent spaces as a full subcategory. The lifting relies on the uniform convergence theorem and Fubini-Tonelli theorem to handle limits and double integrals in the s-finite setting.

Significance. If the reciprocity verification and lifting hold, the work supplies a general, condition-based technique for combining free exponentials with double glueing in orthogonality categories and yields an explicit measure-theoretic model that generalizes probabilistic coherent spaces while decomposing Crubille et al.'s direct construction into two layers. The direct use of standard measure-theoretic results (uniform convergence, Fubini-Tonelli) in the s-finite kernel setting is a concrete strength that makes the construction falsifiable and reproducible.

minor comments (3)

The abstract and introduction should explicitly state the precise statement of the reciprocity condition (including the two directions of the orthogonality) before claiming it suffices for the lift; this would make the central argument easier to follow without consulting the full definitions in §3.
In the description of the free exponential on TsK^op, clarify whether the countable biproducts are used only for the monoidal structure or also in the explicit measure-theoretic formula; a short remark or diagram would resolve potential ambiguity for readers familiar with MTT but not with s-finite kernels.
The claim that O_I(TsK^op) subsumes probabilistic coherent spaces should include a brief, self-contained verification that the countable measurable spaces embed fully faithfully, citing the relevant functor or restriction of the orthogonality.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary and recommendation of minor revision. No major comments were listed in the report, so we have no specific points requiring point-by-point response or revision at this stage.

Circularity Check

0 steps flagged

No significant circularity; derivation is self-contained

full rationale

The paper defines a reciprocity condition on orthogonality and verifies it directly for the Lebesgue-integral orthogonality on s-finite kernels using the uniform convergence theorem and Fubini-Tonelli theorem. The free exponential on TsK^op is constructed explicitly via measure theory, then lifted via the double-glueing construction of Hyland-Schalk once reciprocity holds. All load-bearing steps (explicit description of the exponential, verification of reciprocity, application of the lift) are carried out in the paper itself with external measure-theoretic results that do not presuppose the target lifting. Cited prior works (Mellies-Tabareau-Tasson, Hyland-Schalk, Ehrhard et al., Crubille et al.) supply independent background constructions and are not self-citations whose content is required to close the argument. No fitted parameters, self-definitional reductions, or imported uniqueness theorems appear.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the reciprocity condition as a key assumption and standard measure theory results as background axioms.

axioms (2)

domain assumption The orthogonality relation defined by Lebesgue integrals is reciprocal.
This condition is presented as sufficient to lift the free exponential over the double glueing.
domain assumption The uniform convergence theorem and Fubini-Tonelli theorem apply to the s-finite transition kernels setting.
These are invoked to establish the measure-theoretic properties.

pith-pipeline@v0.9.0 · 5774 in / 1224 out tokens · 24469 ms · 2026-05-24T13:33:17.300649+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Cost/FunctionalEquation.lean washburn_uniqueness_aczel echoes

?

echoes
ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

An orthogonality is reciprocal when for every u : I → R, x : S → J, and f : R → S, u ⊥_R x ∘ f if and only if f ∘ u ⊥_S x (Def 1.4). ... reciprocity derives the three conditions (isomorphism), (tensor) and (identity) ... (precise tensor) is derived (Prop 1.6)
IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean absolute_floor_iff_bare_distinguishability echoes

?

echoes
ECHOES: this paper passage has the same mathematical shape or conceptual pattern as the Recognition theorem, but is not a direct formal dependency.

The orthogonality is reciprocal, hence the free exponential of (i) lifts to the orthogonality category O_I(TsK^op) (abstract). ... reciprocity of orthogonality between measures and measurable functions in terms of Lebesgue integrals (Prop 4.2, 4.3)

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

29 extracted references · 29 canonical work pages

[1]

Bauer, Probability Theory, De Gruyter Studies in Mathematics 23 , Berlin (1996)

H. Bauer, Probability Theory, De Gruyter Studies in Mathematics 23 , Berlin (1996)

work page 1996
[2]

Blute, M

R. Blute, M. Hamano, P. Scott, Softness of Hypercoherences and MALL Full Completeness, Ann. Pure and Applied Logic, 131 (2005), pp. 1-63

work page 2005
[3]

Blute, P

R. Blute, P. Scott, Category Theory for Linear Logicians, in [11], 1–52 (2004)

work page 2004
[4]

Borgstr¨ om, A.D

J. Borgstr¨ om, A.D. Gordon, M. Greenberg, J. Margetson, J. Van Gael, Measure Transformer Semantics for Bayesian Machine Learning, Logical Methods in Computer Science , Vol. 9, No. 3, 2013

work page 2013
[5]

Crubill´ e, Probabilistic Stable Functions on Discrete Cones are Power Series, In 33rd Annual ACM/IEEE Symposium on LICS, 275-284 (2018)

R. Crubill´ e, Probabilistic Stable Functions on Discrete Cones are Power Series, In 33rd Annual ACM/IEEE Symposium on LICS, 275-284 (2018)

work page 2018
[6]

Crubill´ e, T

R. Crubill´ e, T. Ehrhard, M. Pagani, C. Tasson, The Free Exponential Modality of Probabilistic Coherence Spaces, In20th International Conference, Foundations of Software Science and Computation Structures , LNCS (10203). 20-35 (2017)

work page 2017
[7]

Dal Lago, N

U. Dal Lago, N. Hoshino, The Geometry of Bayesian Programming, in 34th Annual ACM/IEEE Symposium of Logic in Computer Science, (2019). Long version arXiv:1904.07425 (2019)

work page arXiv 2019
[8]

Danos, T

V. Danos, T. Ehrhard, Probabilistic Coherence Spaces as a Model of Higher-order Probabilistic Computation, Information and Computation, 209(6), 966-991 (2011)

work page 2011
[9]

Devarajan, D

H. Devarajan, D. Hughes, G. Plotkin, and V. Pratt, Full completeness of the multiplicative linear logic of Chu spaces, in 14th Annual IEEE Symposium on Logic in Computer Science , pp. 234-243 (1999)

work page 1999
[10]

Ehrhard, On K¨ othe Sequence Spaces and Linear Logic, Mathematical Structures in Computer Science 12(5): 579-623 (2002)

T. Ehrhard, On K¨ othe Sequence Spaces and Linear Logic, Mathematical Structures in Computer Science 12(5): 579-623 (2002)

work page 2002
[11]

Ehrhard, J-Y

T. Ehrhard, J-Y. Girard, P. Ruet, P. Scott, (eds). Linear Logic in Computer Science, (London Mathematical Society Lecture Note Series 316) , (2004)

work page 2004
[12]

Pagani, C

T, Ehrhard, M. Pagani, C. Tasson, The computational meaning of probabilistic coherent spaces, in Twenty-Sixth Annual IEEE Symposium on Logic in Computer Science , 87-96 (2011) 28

work page 2011
[13]

Pagani, C

T, Ehrhard, M. Pagani, C. Tasson, Making Full Abstraction for Probabilistic PCF, Journal of the ACM , 65(4): 23:1-23:44 (2018)

work page 2018
[14]

Ehrhard, M

T. Ehrhard, M. Pagani, C. Tasson, Measurable cones and stable, measurable functions: a model for probabilistic higher- order programming. In Proceedings of the ACM on Programming Languages , No. 59 (2018)

work page 2018
[15]

Girard, Linear Logic

J-Y. Girard, Linear Logic. Theor. Comput. Sci. 50: 1-102 (1987)

work page 1987
[16]

J-Y Girard, Between logic and quantic : a tract, in [11], 316-346. (2004)

work page 2004
[17]

Giry, A categorical approach to probability theory, Categorical aspects of topology and analysis, 68-85, Lecture Notes in Math

M. Giry, A categorical approach to probability theory, Categorical aspects of topology and analysis, 68-85, Lecture Notes in Math. 915 Springer (1982)

work page 1982
[18]

Hamano, A linear Exponential Comonad in s-ﬁnite Transition Kernels and Probabilistic Coherent Spaces, submitted, arXiv:1909.07589 (2019)

M. Hamano, A linear Exponential Comonad in s-ﬁnite Transition Kernels and Probabilistic Coherent Spaces, submitted, arXiv:1909.07589 (2019)

work page arXiv 1909
[19]

Hyland, A

M. Hyland, A. Schalk, Glueing and Orthogonality for Models of Linear Logic, Theoretical Computer Science 294 (1-2), 183-231 (2003)

work page 2003
[20]

Kozen, Semantics of Probabilistic Programs

D. Kozen, Semantics of Probabilistic Programs. J. Comput. Syst. Sci. 22(3): 328-350 (1981)

work page 1981
[21]

Melli` es, Categorical semantics of linear logic, Panoramas et Synth` eses 27, Soci´ et´ e Math´ ematique de France 1-196 (2009)

P-A. Melli` es, Categorical semantics of linear logic, Panoramas et Synth` eses 27, Soci´ et´ e Math´ ematique de France 1-196 (2009)

work page 2009
[22]

Melli` es, N

P-A. Melli` es, N. Tabareau and C. Tasson, An explicit formula for the free exponential modality of linear logic,Mathematical Structures in Computer Science, 28 (7), 1253-1286 (2018). The conference version of the same titled paper, in36th ICALP, LNCS (5556), 247-260 (2009)

work page 2018
[23]

Panangaden, The Category of Markov Kernels, in First International Workshop on Probabilistic Methods in Veriﬁca- tion, Electr

P. Panangaden, The Category of Markov Kernels, in First International Workshop on Probabilistic Methods in Veriﬁca- tion, Electr. Notes Theor. Comput. Sci. 22: 171-187 (1999)

work page 1999
[24]

Panangaden, Labelled Markov Processes, World Scientiﬁc (2009)

P. Panangaden, Labelled Markov Processes, World Scientiﬁc (2009)

work page 2009
[25]

Seely, Linear logic, *-autonomous categories and cofree coalgebras, AMS Contemporary Mathematics , 92: 371-382, (1989)

R. Seely, Linear logic, *-autonomous categories and cofree coalgebras, AMS Contemporary Mathematics , 92: 371-382, (1989)

work page 1989
[26]

Sharpe, General Theory of Markov Processes, Pure and Applied Mathematics Volume 133, Academic Press, 1988

M. Sharpe, General Theory of Markov Processes, Pure and Applied Mathematics Volume 133, Academic Press, 1988

work page 1988
[27]

Staton, Commutative Semantics for Probabilistic Programming, In 26th European Symposium on Programming, LNCS (10201) 855-879 (2017)

S. Staton, Commutative Semantics for Probabilistic Programming, In 26th European Symposium on Programming, LNCS (10201) 855-879 (2017)

work page 2017
[28]

Staton, H

S. Staton, H. Yang, C. Heunen, O. Kammar and F. Wood, Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In 31st Annual ACM/IEEE Symposium on LICS 525–534, (2016)

work page 2016
[29]

Omitted Proofs A.1.1

Appendix A.1. Omitted Proofs A.1.1. Proof of Propsotion 1.14 Proof. First, to check the double orthogonality, it suﬃces to show that A p&B p = U◦ for certain subset U⊆C (A&B, J). The U is given by (A p)◦pl∪ (B p)◦pr. In the following the reciprocity of ⊥ is used wrt the left and right projections pl and pr, respectively. (⊆) Take any u&v from (LHS) with u...

work page

[1] [1]

Bauer, Probability Theory, De Gruyter Studies in Mathematics 23 , Berlin (1996)

H. Bauer, Probability Theory, De Gruyter Studies in Mathematics 23 , Berlin (1996)

work page 1996

[2] [2]

Blute, M

R. Blute, M. Hamano, P. Scott, Softness of Hypercoherences and MALL Full Completeness, Ann. Pure and Applied Logic, 131 (2005), pp. 1-63

work page 2005

[3] [3]

Blute, P

R. Blute, P. Scott, Category Theory for Linear Logicians, in [11], 1–52 (2004)

work page 2004

[4] [4]

Borgstr¨ om, A.D

J. Borgstr¨ om, A.D. Gordon, M. Greenberg, J. Margetson, J. Van Gael, Measure Transformer Semantics for Bayesian Machine Learning, Logical Methods in Computer Science , Vol. 9, No. 3, 2013

work page 2013

[5] [5]

Crubill´ e, Probabilistic Stable Functions on Discrete Cones are Power Series, In 33rd Annual ACM/IEEE Symposium on LICS, 275-284 (2018)

R. Crubill´ e, Probabilistic Stable Functions on Discrete Cones are Power Series, In 33rd Annual ACM/IEEE Symposium on LICS, 275-284 (2018)

work page 2018

[6] [6]

Crubill´ e, T

R. Crubill´ e, T. Ehrhard, M. Pagani, C. Tasson, The Free Exponential Modality of Probabilistic Coherence Spaces, In20th International Conference, Foundations of Software Science and Computation Structures , LNCS (10203). 20-35 (2017)

work page 2017

[7] [7]

Dal Lago, N

U. Dal Lago, N. Hoshino, The Geometry of Bayesian Programming, in 34th Annual ACM/IEEE Symposium of Logic in Computer Science, (2019). Long version arXiv:1904.07425 (2019)

work page arXiv 2019

[8] [8]

Danos, T

V. Danos, T. 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]

Devarajan, D

H. Devarajan, D. Hughes, G. Plotkin, and V. Pratt, Full completeness of the multiplicative linear logic of Chu spaces, in 14th Annual IEEE Symposium on Logic in Computer Science , pp. 234-243 (1999)

work page 1999

[10] [10]

Ehrhard, On K¨ othe Sequence Spaces and Linear Logic, Mathematical Structures in Computer Science 12(5): 579-623 (2002)

T. Ehrhard, On K¨ othe Sequence Spaces and Linear Logic, Mathematical Structures in Computer Science 12(5): 579-623 (2002)

work page 2002

[11] [11]

Ehrhard, J-Y

T. Ehrhard, J-Y. Girard, P. Ruet, P. Scott, (eds). Linear Logic in Computer Science, (London Mathematical Society Lecture Note Series 316) , (2004)

work page 2004

[12] [12]

Pagani, C

T, Ehrhard, M. Pagani, C. Tasson, The computational meaning of probabilistic coherent spaces, in Twenty-Sixth Annual IEEE Symposium on Logic in Computer Science , 87-96 (2011) 28

work page 2011

[13] [13]

Pagani, C

T, Ehrhard, M. Pagani, C. Tasson, Making Full Abstraction for Probabilistic PCF, Journal of the ACM , 65(4): 23:1-23:44 (2018)

work page 2018

[14] [14]

Ehrhard, M

T. Ehrhard, M. Pagani, C. Tasson, Measurable cones and stable, measurable functions: a model for probabilistic higher- order programming. In Proceedings of the ACM on Programming Languages , No. 59 (2018)

work page 2018

[15] [15]

Girard, Linear Logic

J-Y. Girard, Linear Logic. Theor. Comput. Sci. 50: 1-102 (1987)

work page 1987

[16] [16]

J-Y Girard, Between logic and quantic : a tract, in [11], 316-346. (2004)

work page 2004

[17] [17]

Giry, A categorical approach to probability theory, Categorical aspects of topology and analysis, 68-85, Lecture Notes in Math

M. Giry, A categorical approach to probability theory, Categorical aspects of topology and analysis, 68-85, Lecture Notes in Math. 915 Springer (1982)

work page 1982

[18] [18]

Hamano, A linear Exponential Comonad in s-ﬁnite Transition Kernels and Probabilistic Coherent Spaces, submitted, arXiv:1909.07589 (2019)

M. Hamano, A linear Exponential Comonad in s-ﬁnite Transition Kernels and Probabilistic Coherent Spaces, submitted, arXiv:1909.07589 (2019)

work page arXiv 1909

[19] [19]

Hyland, A

M. Hyland, A. Schalk, Glueing and Orthogonality for Models of Linear Logic, Theoretical Computer Science 294 (1-2), 183-231 (2003)

work page 2003

[20] [20]

Kozen, Semantics of Probabilistic Programs

D. Kozen, Semantics of Probabilistic Programs. J. Comput. Syst. Sci. 22(3): 328-350 (1981)

work page 1981

[21] [21]

Melli` es, Categorical semantics of linear logic, Panoramas et Synth` eses 27, Soci´ et´ e Math´ ematique de France 1-196 (2009)

P-A. Melli` es, Categorical semantics of linear logic, Panoramas et Synth` eses 27, Soci´ et´ e Math´ ematique de France 1-196 (2009)

work page 2009

[22] [22]

Melli` es, N

P-A. Melli` es, N. Tabareau and C. Tasson, An explicit formula for the free exponential modality of linear logic,Mathematical Structures in Computer Science, 28 (7), 1253-1286 (2018). The conference version of the same titled paper, in36th ICALP, LNCS (5556), 247-260 (2009)

work page 2018

[23] [23]

Panangaden, The Category of Markov Kernels, in First International Workshop on Probabilistic Methods in Veriﬁca- tion, Electr

P. Panangaden, The Category of Markov Kernels, in First International Workshop on Probabilistic Methods in Veriﬁca- tion, Electr. Notes Theor. Comput. Sci. 22: 171-187 (1999)

work page 1999

[24] [24]

Panangaden, Labelled Markov Processes, World Scientiﬁc (2009)

P. Panangaden, Labelled Markov Processes, World Scientiﬁc (2009)

work page 2009

[25] [25]

Seely, Linear logic, *-autonomous categories and cofree coalgebras, AMS Contemporary Mathematics , 92: 371-382, (1989)

R. Seely, Linear logic, *-autonomous categories and cofree coalgebras, AMS Contemporary Mathematics , 92: 371-382, (1989)

work page 1989

[26] [26]

Sharpe, General Theory of Markov Processes, Pure and Applied Mathematics Volume 133, Academic Press, 1988

M. Sharpe, General Theory of Markov Processes, Pure and Applied Mathematics Volume 133, Academic Press, 1988

work page 1988

[27] [27]

Staton, Commutative Semantics for Probabilistic Programming, In 26th European Symposium on Programming, LNCS (10201) 855-879 (2017)

S. Staton, Commutative Semantics for Probabilistic Programming, In 26th European Symposium on Programming, LNCS (10201) 855-879 (2017)

work page 2017

[28] [28]

Staton, H

S. Staton, H. Yang, C. Heunen, O. Kammar and F. Wood, Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In 31st Annual ACM/IEEE Symposium on LICS 525–534, (2016)

work page 2016

[29] [29]

Omitted Proofs A.1.1

Appendix A.1. Omitted Proofs A.1.1. Proof of Propsotion 1.14 Proof. First, to check the double orthogonality, it suﬃces to show that A p&B p = U◦ for certain subset U⊆C (A&B, J). The U is given by (A p)◦pl∪ (B p)◦pr. In the following the reciprocity of ⊥ is used wrt the left and right projections pl and pr, respectively. (⊆) Take any u&v from (LHS) with u...

work page