Giry monad

Stream: new members

[Patrick Massot]

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

[Patrick Massot]

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!

[Kevin Buzzard]

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...)

[Koundinya Vajjha]

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

[Kevin Buzzard]

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!

[Koundinya Vajjha]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Patrick Massot]

At least we hear the word

[Koundinya Vajjha]

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. :-)

[Kevin Buzzard]

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

[Sebastien Gouezel]

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!

[Johan Commelin]

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

[Koundinya Vajjha]

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

[Sebastien Gouezel]

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...

[Sebastien Gouezel]

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.

[Floris van Doorn]

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

[Sebastien Gouezel]

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.

[Vincent Beffara]

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

[Vincent Beffara]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Floris van Doorn]

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/

[Sebastien Gouezel]

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.