Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: event: Categorical Probability and Statistics 2020 workshop

Topic: Tutorial: Probabilistic programming and semantics

Paolo Perrone (Jun 02 2020 at 23:52):

Hello all, here's Christine Tasson's video, about semantics in the context of probablistic programming.
https://youtu.be/3P0RJcfynNc
Any questions go here :)

Tobias Fritz (Jun 03 2020 at 16:33):

Thank you, Christine, for the very nice tutorial! Among other things, I finally understand why semantics is important. Here are a few questions if you don't mind.

• The typed lambda calculus has very nice categorical semantics given by CCCs. Could there be a similarly general categorical semantics for a probabilistic version of the simply typed lambda calculus with "coin"?
• The stochastic kernels Proba that you introduced are subnormalized, but not necessarily normalized, right?
• Is the problem of finding a CCC of continuous domains that is stable under the probabilistic powerdomain functor still open?
• I haven't quite understood the relevance of linear logic to the semantics, and in particular of the analytic morphisms, since a stochastic kernel clearly operates in a linear way on probability distributions. So is this mainly a way to construct CCCs of the desired kind, but the probabilistic program interpretation doesn't use all the structure of linear logic? Or are there languages with syntactical constructions which result semantically in non-linear maps between spaces of distributions?
• There's another CCC which is closely related to measure-theoretic probability and quantum probability, namely the opposite of the category of $W^*$-algebras. It's quite remarkable that the category of $W^*$-algebras is cocartesian coclosed, making its opposite into a CCC. I think that this still holds (for purely formal reasons) if one restricts to commutative $W^*$-algebras. This results in a category equivalent to a category of measurable spaces. So it's natural to suspect that this also carries a version of the Giry monad. Has this category been studied as a potential nice CCC for probabilistic program semantics? Perhaps it's related to your category of measurable cones?

Sam Staton (Jun 03 2020 at 21:09):

Tobias Fritz said:

It's quite remarkable that the category of $W^*$-algebras is cocartesian coclosed, making its opposite into a CCC.

Hi -- I thought that paper was about a monoidal coclosed structure, did I misunderstand? although this would still be relevant for linear logic, of course.

John Baez (Jun 03 2020 at 21:10):

I can't believe it's cocartesian coclosed. For commutative W*-algebras I can believe it.

John Baez (Jun 03 2020 at 21:11):

The category of commutative W*-algebras is sorta kinda like the opposite of the category of measurable spaces...

Tobias Fritz (Jun 03 2020 at 21:21):

I have to admit that I haven't studied the paper in detail, but on p.8/9 it says that the monoidal product $\mathcal{M} \bar{\otimes} \mathcal{N}$ is defined as the quotient of the free product $\mathcal{M} \ast \mathcal{N}$ by the commutators. So this seems to be saying that in the category of commutative $W^*$-algebras, the relevant monoidal structure is exactly the coproduct. Although of course I may well be missing or misunderstanding something. In any case, you're both right, in the statement above I indeed meant to say that the category of commutative $W^*$-algebras is apparently cocartesian coclosed.

There's also the MSc thesis of Sander Uijlen that talks about the category of $W^*$-algebras and the free exponential. It was written in Nijmegen around the time (I think) that Sam was there, so Sam will probably know this stuff much better :)

BTW @John Baez, great to have you chime in!

Tobias Fritz (Jun 03 2020 at 21:24):

Everyone: please feel free to ask more "basic" questions as well! We will have several communities interacting here, so nothing is too basic to be asked about.

Christine Tasson (Jun 05 2020 at 14:25):

Tobias Fritz said:

Thank you, Christine, for the very nice tutorial! Among other things, I finally understand why semantics is important. Here are a few questions if you don't mind.

Sorry for my late answer to your points and thanks for asking questions !

Christine Tasson (Jun 05 2020 at 14:48):

Tobias Fritz said:

• The stochastic kernels Proba that you introduced are subnormalized, but not necessarily normalized, right?

They are subnormalized indeed. To understand why, consider a probabilistic program with a while loop that can diverge. As the semantics of a probabilistic program of type nat coincides to the distribution of its output values, you have to keep some probability for this divergence that can be seen as one specific output value.

Christine Tasson (Jun 05 2020 at 14:50):

Tobias Fritz said:

• Is the problem of finding a CCC of continuous domains that is stable under the probabilistic powerdomain functor still open?

I think so. There have been some work by Goubault-Larrecq http://www.lsv.fr/Publis/PAPERS/PDF/JGL-lmcs12.pdf, who defines a suitable notion of domains, but it does not give rise to a CCC.

Christine Tasson (Jun 05 2020 at 15:03):

Tobias Fritz said:

• I haven't quite understood the relevance of linear logic to the semantics, and in particular of the analytic morphisms, since a stochastic kernel clearly operates in a linear way on probability distributions. So is this mainly a way to construct CCCs of the desired kind, but the probabilistic program interpretation doesn't use all the structure of linear logic? Or are there languages with syntactical constructions which result semantically in non-linear maps between spaces of distributions?

I am not sure to understand quite well your question. But I think you refer to the fact that we are used to probabilistic programs or constructions that use linearly their input. It is the case in the monadic lambda-calculus, in probabilistic automata and in Bayesian networks and in Call-By-Value languages in general.

In general, if you have a probabilistic program M that you want to compose with another one N, you use the let construction:
let x=M in N
This means that you first sample M and then pass it to N. In this way, each time you use the variable x in N, you will substitute it with the same value.

But there are situations where you want to sample M many times and you really want to take into consideration the possibly different outcomes. For instance, you want to approximate a gaussian distribution using the Gatson board. If M is the program Plinko in the slides, you are not interested in one sample but with all the outcomes and their multiplicities.
A program P that do this approximation will use infinitely many copies of M. You may think of this copies as i.i.d. random variables x. Now P is non linear and its semantics in the linear logic framework will be a formal series depending on x.

This corresponds to a Call-By-Name language: in the beta reduction (\lambda x. P) M -> P[x\M], you first duplicate M as many times as needed and substitute all the occurrences of x in P. That means that you have duplicated the random variables corresponding to M into as many random variables all independent and following the same law.

Manuel Bärenz (Jun 05 2020 at 15:49):

That's surprising to me. For example in Haskell, I'd expect that x is sampled coherently the same way in all occurrences. There, the difference would be whether you pass around a value in a probability monad, or whether you use Kleisli composition.

Tobias Fritz (Jun 05 2020 at 23:05):

Thanks, @Christine Tasson , for the elaborate answer :)

I'll have to let this sink in for some time, but if I understand correctly the use of the exponential modality is closely related to the de Finetti theorem. Or let me perhaps ask like this: can I intuitively think of the function type $A \multimap B$ as the type of Kleisli morphisms $A \to PB$ where $P$ is a probability monad, and $!A \multimap B$ instead is the type of all (or all analytic) functions $PA \to PB$? (Maybe not completely precisely, but at least at an intuitive level?)

Christine Tasson (Jun 09 2020 at 07:10):

Kind of:

In the LL setting, $A\multimap B$ can be thought as stochastic matrices or linear operators that preserve probability distributions
And $A\to B=!A\multimap B$ can be thought as analytic operators that also preserve probability distributions

In the CBV/Monadic approach, $A\to B$ will be interpreted in the Kleisli category taking as input an element of $A$ and producing a probability distribution.

Do note hesitate to ask for more details !

eric brunner (Jun 22 2020 at 02:44):

john, could i persuade you to expand on that by a para or two? genuinely curious. -e

John Baez (Jun 22 2020 at 04:59):

Me? Expand on what, exactly?

eric brunner (Jun 22 2020 at 06:13):

Rongmin Lu said:

eric brunner-williams (uoregon) said:

john, could i persuade you to expand on that by a para or two? genuinely curious. -e

It may help if you could do a Quote and Reply on the message you're interested in commenting on next time. If you're unfamiliar with the Zulip mechanism, there are instructions here.

thank you. got it.