Giry monad for product measures

Stream: general

[Koundinya Vajjha]

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]

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]

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]

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

[Koundinya Vajjha]

Oh you can use do?

[Johannes Hölzl]

argh sorry, fixed my message

[Koundinya Vajjha]

Oh I see. Thanks!

[Koundinya Vajjha]

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

[Jason Rute]

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]

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]

Yes, I think I spoke too quickly...

[Johannes Hölzl]

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]

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]

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

[Jason Rute]

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]

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

[Mario Carneiro]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

and also fancy tactic/parser footwork

[Johan Commelin]

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

[Johannes Hölzl]

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

[Jason Rute]

@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]

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

[Joseph Tassarotti]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Reid Barton]

It's not automatic in general

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

terms have free variables

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

hence do notation exists

[Mario Carneiro]

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

[Joseph Tassarotti]

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]

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]

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]

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]

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

[Mario Carneiro]

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]

@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]

The state is

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

[Koundinya Vajjha]

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