Zulip Chat Archive

Stream: new members

Topic: Giry monad


view this post on Zulip Patrick Massot (Oct 11 2019 at 12:53):

Hi @Vincent Beffara, welcome! You'll eligible for the Giry test: do you know what is the Giry monad?

view this post on Zulip Patrick Massot (Oct 11 2019 at 13:21):

Oh crap: he left. I hope it's not because of the Giry joke. @Vincent Beffara this was a joke about computer scientists who like to pretend they think probability theory is the study of the Giry monad, an arcane part of category theory. But you're very welcome to formalize actual probability theory!

view this post on Zulip Kevin Buzzard (Oct 11 2019 at 17:19):

I was emailed by a computer scientist from Harvard earlier this week, who sent me a preprint in statistical learning theory where they have formalised some basic results from this area in Lean. I took a look through the paper and the first thing I noticed was that @Koundinya Vajjha was a co-author (which probably explained the Lean) but also that they talk extensively about the Giry monad. So there really are people out there who know what it is (but I think none of the authors were mathematicians...)

view this post on Zulip Koundinya Vajjha (Oct 11 2019 at 17:29):

Yeah that preprint was an outgrowth of my internship at Oracle Labs. The computer scientist who emailed you was probably Jean-Baptiste Tristan?

view this post on Zulip Kevin Buzzard (Oct 11 2019 at 17:31):

Indeed! Is it posted online anywhere? I was pleasantly surprised to see Giry monads in there, for me and Patrick they are becoming a running joke, I have asked several mathematicians about them (including a Fields Medallist and another highly prestigious person) and none of them have ever heard of them!

view this post on Zulip Koundinya Vajjha (Oct 11 2019 at 17:32):

No it's not posted online yet! And the Giry monad is really quite pleasant. It's a pity they haven't heard of it.

view this post on Zulip Kevin Buzzard (Oct 11 2019 at 17:33):

I guess many mathematicians haven't even heard of filters ;-)

view this post on Zulip Kevin Buzzard (Oct 11 2019 at 17:33):

but a lot more of them haven't heard of monads.

view this post on Zulip Patrick Massot (Oct 11 2019 at 17:33):

At least we hear the word

view this post on Zulip Koundinya Vajjha (Oct 11 2019 at 17:35):

Yeah I consider myself a mathematician (who formalizes) and it's really when you see the Giry monad in action to construct product measures, say, you realize how cool it is. :-)

view this post on Zulip Kevin Buzzard (Oct 11 2019 at 17:35):

Maybe I'm saying it wrong. How do you pronounce "Giry"?

view this post on Zulip Sebastien Gouezel (Oct 11 2019 at 17:52):

I don't think the Giry monad is relevant to mainstream mathematicians in probability theory, as we most often work with infinite sequences of random variables. For instance, the first theorem in a probability course is the law of large numbers, saying that if X_n is a sequence of integrable independent identically distributed random variables, then (X_0+...+X_{n-1})/n converges almost surely to the average of X_0. I was under the impression that this can not be conveniently expressed with the Giry monad, but I would be happy to be corrected if I am wrong!

view this post on Zulip Johan Commelin (Oct 11 2019 at 17:54):

Note that the law of large numbers is one of the 5 remaining theorems on Freek100.

view this post on Zulip Koundinya Vajjha (Oct 11 2019 at 17:55):

Johannes used to talk about the Ionescu-Tulcea theorem which allows one to construct Markov processes using the Giry monad for probability measures.

view this post on Zulip Sebastien Gouezel (Oct 11 2019 at 18:59):

Note that the law of large numbers is one of the 5 remaining theorems on Freek100.

Well, I have proved in Isabelle the Birkhoff theorem, which is a far reaching generalization of the law of large numbers...

view this post on Zulip Sebastien Gouezel (Oct 11 2019 at 19:01):

Johannes used to talk about the Ionescu-Tulcea theorem which allows one to construct Markov processes using the Giry monad for probability measures.

If you want to look at a Markov process in finite time, the Giry monad is perfect (and essentially designed for this, I would say). But if you want a theorem talking about the process over all times, I don't think it is the right tool.

view this post on Zulip Floris van Doorn (Oct 11 2019 at 19:04):

How much work would it be to specialize the Birkhoff theorem to the law of large numbers?

view this post on Zulip Sebastien Gouezel (Oct 11 2019 at 19:42):

Not that much. But given all the theory that Johannes and Jeremy have already developed to prove the (much harder) central limit theorem, it would probably be even quicker to formalize one of the classical proofs of the law of large numbers -- and this would just be an exercise, really.

view this post on Zulip Vincent Beffara (Oct 11 2019 at 20:44):

I had never heard of the Giri monad. And now that I had a quick look at the page, I am not really less perplexed than before

view this post on Zulip Vincent Beffara (Oct 11 2019 at 20:45):

To me randomness feels more like the IO monad from Haskell, an unknowable process that ends up producing a real number at the end ...

view this post on Zulip Patrick Massot (Oct 11 2019 at 20:50):

If you know monads from Haskell you're half way through understanding that Giry stuff.

view this post on Zulip Patrick Massot (Oct 11 2019 at 20:50):

And soon you'll be able to do probability theory the right way :lol:

view this post on Zulip Mario Carneiro (Oct 12 2019 at 04:56):

I think that the Giry monad is essentially the formalization of your intuition, @Vincent Beffara

view this post on Zulip Mario Carneiro (Oct 12 2019 at 04:58):

I'm not sure the definition itself provides much knowledge, but the idea that you can view random variables as a monad makes it really clear how to use them in diverse ways

view this post on Zulip Floris van Doorn (Oct 14 2019 at 19:23):

Not that much. But given all the theory that Johannes and Jeremy have already developed to prove the (much harder) central limit theorem, it would probably be even quicker to formalize one of the classical proofs of the law of large numbers -- and this would just be an exercise, really.

Is it really that easy? If we're talking about the strong law of large numbers, I believe the proof is quite tricky. According to Terry Tao:

The weak law is easy to prove, but the strong law (which of course implies the weak law, by Egoroff’s theorem) is more subtle, and in fact the proof of this law (assuming just finiteness of the first moment) usually only appears in advanced graduate texts.

https://terrytao.wordpress.com/2008/06/18/the-strong-law-of-large-numbers/

view this post on Zulip Sebastien Gouezel (Oct 14 2019 at 19:36):

No, the strong law of large numbers is not easy, but it is not hard either. The proof takes less than two pages in standard textbooks (for instance Billingsley, probability and measure), and all the supporting material is already formalized, so I am pretty sure I could do it in a few hours, say.


Last updated: May 14 2021 at 06:16 UTC