Finite probability spaces implementations

Stream: new members

[Michael Fishman]

What implementations are there for finite probability spaces?

I'm looking for an implementation where:

1. The event/condition variables of a distribution are part of its type. For example, a conditional distribution $P(Color \mid Species)$ would have a type like Distribution Color Species
2. Computing joint/product/marginal/conditional distributions verifies that the input distributions are compatible, and the result distribution has the correct type. For example, something like

probability_of_color_conditioned_on_species : Distribution Color Species
probability_of_species : Distribution Species unit

probability_of_color_and_species : Distribution (Color \times Species) Unit := probability_of_color_conditioned_on_species * probability_of_species

1. The functions are computible, so that I could use it with real data. Hopefully, given a non-computible implementation, I would be able to modify it to be computible myself.

So far I'm aware of @Daniel Weber's implementation here. I'm wondering what else exists.

Context: I needed to manipulate discrete distributions in python in the past. I built a library for this. It tracked event and condition variables, and enforced compatibility when combining distributions. But none of that tracking/enforcement was at the type level, because python makes that impossible AFAIK. Since then I've been itching to make/see a library like that, with type-level tracking/enforcement of event/condition variables.

[Daniel Weber]

$\mathbb{R}$ isn't computable, so if you want to make the functions computable you have to restrict the possible probabilities

[Michael Fishman]

R isn't computable

Yea, I ran into that on my first crack at this last week. I got around it so far by using NNRat.

[Michael Fishman]

@Daniel Weber Does your implementation deal with conditional distributions? I see instMulFinPMF takes product distributions, but haven't found conditionals yet.

[Daniel Weber]

Michael Fishman said:

Daniel Weber Does your implementation deal with conditional distributions? I see instMulFinPMF takes product distributions, but haven't found conditionals yet.

No, it doesn't

[Daniel Weber]

Michael Fishman said:

R isn't computable

Yea, I ran into that on my first crack at this last week. I got around it so far by using NNRat.

Perhaps it's better to just use docs#LinearOrderedField (or maybe just docs#LinearOrderedRing is enough) and let the user worry about computability

[Michael Fishman]

I like that idea!

[Michael Fishman]

@Daniel Weber Why did you use Real numbers, and add a condition that they are $>= 0$, instead of using NNReal?

[Daniel Weber]

I needed to subtract probabilities for statistical distance, and it was really inconvenient with NNReal. In retrospect it might've been better to just use dist, I'm not sure

[Michael Fishman]

Thanks!