Zulip Chat Archive

Stream: general

Topic: Giry monad for product measures


Koundinya Vajjha (May 09 2019 at 21:01):

I want to construct the k-fold product measure from a measure m. I looked through the old chats and @Johannes Hölzl had a slick way to do this using the Giry Monad. Does anyone else understand how to do this?

Does mathlib even have product measures?

Koundinya Vajjha (May 09 2019 at 21:01):

If I understand correctly, I can't directly use do notation to construct this as measure isn't a monad instance. So this won't work:

prod M1 M2 := do { x <- M1, y <- M2, return (x, y) }

Johannes Hölzl (May 09 2019 at 23:01):

You can't write do, but you can still use bind and dirac (otherwise called pure or return). The interesting part is to prove commutativity, i.e. Fubini's theorem

Johannes Hölzl (May 09 2019 at 23:02):

prod m1 m2 := m1.bind (fun x, m2.bind (fun y, dirac (x, y)))

Koundinya Vajjha (May 09 2019 at 23:02):

Oh you can use do?

Johannes Hölzl (May 09 2019 at 23:03):

argh sorry, fixed my message

Koundinya Vajjha (May 09 2019 at 23:05):

Oh I see. Thanks!

Koundinya Vajjha (May 09 2019 at 23:05):

I'll try this once I'm at my machine again.

Jason Rute (May 09 2019 at 23:08):

While the Giry Monad is a slick idea, it won’t ever work in Lean. Here is why. For a measure to be a monad, one needs to make sense of the type measure A where A is a type. But that is not how measures work, m is not a measure on a type A, it is a measure on a space A. (Either a measurable space, or for some types of measure theory, a Polish space or a locally compact Hausdorff space.) Moreover, even if we could restrict to a set of types, we still need to restrict to only certain functions in our map operator. For if m is a measure on the reals, and implicitly we are using the canonical Borel measurable structure of the reals, we still can’t expect map f m to be meaningful for every function from the reals to the reals. Consider the indicator function of a non-measurable set. There is no push-forward measure to be had. The Giry monad is only a monad on a restricted type system. (Such as where types are Polish spaces and functions are continuous maps.) (Alternately, if by “measure”, you mean a probability measure on the full power set sigma algebra, then yes it is a monad, but unless you only care about the discrete setting, this is not what you want...)

Johannes Hölzl (May 09 2019 at 23:30):

Uh, that's a bold claim for something which is already in mathlib: https://github.com/leanprover-community/mathlib/blob/master/src/measure_theory/giry_monad.lean

Jason Rute (May 09 2019 at 23:32):

Yes, I think I spoke too quickly...

Johannes Hölzl (May 09 2019 at 23:32):

The trick is to just set it to 0 (or some null measure etc) if the function is not measurable. Then each equation one proves over the Giry monad requires the necessary measurability assumptions.

Johannes Hölzl (May 09 2019 at 23:33):

Another way to do it would be to setup the category of measurable spaces, and show that there exists a measure-Endofunctor in this category, and prove that it is actually a monad

Johannes Hölzl (May 09 2019 at 23:33):

But to apply it I guess the current approach is the easier one

Jason Rute (May 10 2019 at 00:16):

It is a nice trick (and I should never start a comment with "won't ever"). But doesn't the "set it to 0" trick violate the monadic laws, namely associativity? For example, if m is the Lebesgue measure, f in non measurable, and g x := tt is constant doesn't do { y <- do { x <- m; f x }; g y} give the 0 measure, but do { x <- m; do { y <- f x; g y }} give dirac tt. I think my poorly expressed point is that there isn't a way to actually make measure a monad in Lean which obeys the monadic axioms, but maybe I am mistaken.

Jason Rute (May 10 2019 at 00:19):

Either way, you clearly made the ideas useful (and I again apologize for my brash claims).

Mario Carneiro (May 10 2019 at 00:21):

There is of course category_theory for being able to talk about monads in other categories, but you are probably right that there is no lawful monad from the category of types and functions

Scott Morrison (May 10 2019 at 00:53):

With a PR for monoidal categories open, general monads will be available any day now. :-)

Johan Commelin (May 10 2019 at 03:39):

We won't have the do-notation for those general monads... I'm not sure if that is a bug or a feature :stuck_out_tongue_wink:

Mario Carneiro (May 10 2019 at 04:03):

do notation doesn't really make sense unless you at least have the structure of a CCC, because you need lambda terms

Johan Commelin (May 10 2019 at 04:06):

Sure... but even if we have CCC, we still don't have do

Johan Commelin (May 10 2019 at 04:06):

The category in question (Meas) is a CCC, I think [but I didn't check carefully]

Mario Carneiro (May 10 2019 at 04:10):

and also fancy tactic/parser footwork

Johan Commelin (May 10 2019 at 04:11):

Exactly... that was what I was mostly concerned about

Johannes Hölzl (May 10 2019 at 06:08):

@Jason Rute yes, this is the limitation: the monadic laws only hold conditionally. All functions / sets need to be measurable.

Jason Rute (May 10 2019 at 11:08):

@Johan Commelin I don’t think Meas is CCC. At least Prop 6 in this paper says it is not: https://arxiv.org/pdf/1701.02547.pdf

Johan Commelin (May 10 2019 at 11:09):

Ok... too bad. I've never really done measure theory. So I better don't make bold claims

Joseph Tassarotti (May 10 2019 at 17:48):

do notation doesn't really make sense unless you at least have the structure of a CCC, because you need lambda terms

Why do you say that? Isn't do notation really just sugar for bind's?

Mario Carneiro (May 10 2019 at 19:48):

do a <- f, t is sugar for f >>= \lam a, t, i.e. it is a combination of bind and lambda

Mario Carneiro (May 10 2019 at 19:49):

because term t may have free references to a that was introduced by the do

Mario Carneiro (May 10 2019 at 20:06):

Actually, maybe you don't need exponential objects, if you make sure to uncurry everything. To translate the type theory bind operator to cats, suppose we have G |- do a : A <- f, t : T B where T is the monad. We view this as an arrow G -> T B, where f : G -> T A and t : G x A -> T B. I think it's possible to define this bind in any (category theory) monad with products, Reid and Scott will know

Mario Carneiro (May 10 2019 at 20:21):

At the moment I'm stuck on how to make an arrow G x T A -> T (G x A). This is some tensoring thing?

Reid Barton (May 10 2019 at 20:26):

https://en.wikipedia.org/wiki/Strong_monad

Reid Barton (May 10 2019 at 20:26):

It's not automatic in general

Mario Carneiro (May 10 2019 at 20:30):

Does anything special happen when the monoidal product is just the categorical product there? I see references to things like all functors on Set are strong but that might have to do with the existence of exponentials

Mario Carneiro (May 10 2019 at 20:31):

Also, this paper https://arxiv.org/pdf/1612.05939.pdf suggests that in the case of the Giry monad even this approach won't work because it's not strong

Koundinya Vajjha (May 10 2019 at 20:31):

I still don't quite understand. What's to stop me right now from defining my own do notation for this Giry monad?

Mario Carneiro (May 10 2019 at 20:31):

the problem is that arrows are not the same as terms in type theory

Mario Carneiro (May 10 2019 at 20:31):

terms have free variables

Mario Carneiro (May 10 2019 at 20:32):

and you want to interpret these variables as somehow denoting certain projections from the context object G to make an arrow

Mario Carneiro (May 10 2019 at 20:36):

for example, the type theory term a : A, b : B |- a : A gets turned into pi1 : A x B --> A, and a : A, b : B |- (a, (b, a)) : A x (B x A) becomes (pi1, (pi2, pi1)) : A x B --> A x (B x A)

Mario Carneiro (May 10 2019 at 20:38):

But then the question is how to define the term G |- do a <- f, t, where G |- f : F A and G, a : A |- t : F B? By induction we suppose we can translate f as an arrow G --> F A and t as an arrow G x A --> F B, but then we need an operation in the category to get from this to G --> F B and that needs a strong monadic structure

Mario Carneiro (May 10 2019 at 20:39):

Over the category Type, which is what [monad T] is talking about, all monads are strong monads because tensorial strength is "free"

Mario Carneiro (May 10 2019 at 20:40):

hence do notation exists

Mario Carneiro (May 10 2019 at 20:40):

but over a general category it's not clear how to interpret the term as some arrow in the category

Joseph Tassarotti (May 10 2019 at 20:41):

I think there's two separate issues here: we can define a do notation that desugars into the bind defined here: https://github.com/leanprover-community/mathlib/blob/master/src/measure_theory/giry_monad.lean#L144, but it may very well be the case that the function ends up not being measurable. But that's already a problem with using the bind directly

Reid Barton (May 10 2019 at 20:54):

I think what's special about Set isn't that it's cartesian closed or whatever but rather that it is the base category that we are enriched over.
That is, it is baked into the notion of "functor"

Koundinya Vajjha (May 11 2019 at 14:14):

So the tl;dr is the following:
1. you can't use the existing do notation for the Giry monad because it is not a monad over the Type category.
2. because the way it is implemented currently needs all functions to be measurable.
3. you still can write your own do notation to simply desugar the Giry monad bind.

Mario Carneiro (May 12 2019 at 06:46):

Not quite. You can use the existing do notation, all that needs to be done is that the Giry monad bind be installed as a has_bind instance

Mario Carneiro (May 12 2019 at 06:47):

You could even provide a monad instance for the Giry monad; it just won't be is_lawful_monad

Mario Carneiro (May 12 2019 at 06:49):

You won't even get the wrong result if you use the regular do notation; it fails when the input functions are not measurable but when they are it gets the right result (and in any reasonable application you will use it with measurable functions anyway)

Koundinya Vajjha (May 12 2019 at 12:58):

@Mario Carneiro I tried to do that, but you can only install a has_bind instance over all types α which are instances of [measurable_space α].

instance giry.bind :
has_bind (λ α, measure_theory.measure α) := sorry

Koundinya Vajjha (May 12 2019 at 12:58):

The state is

failed to synthesize type class instance for
α : Type ?
 measurable_space α

Koundinya Vajjha (May 12 2019 at 13:07):

Can I make a subtype of types the elements of which are instances of measurable_space?


Last updated: Dec 20 2023 at 11:08 UTC