Email Gateway (Aug 19 2022 at 17:04): Email Gateway (Aug 19 2022 at 17:04):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear probability experts,
I have a possibly infinite nesting of discrete probability distributions, i.e., a
codatatype of the form
codatatype foo = Foo "(nat * foo) pmf"
where pmf is the type of discrete probability distributions (probability mass functions,
PMF). Now, I would like to measure unrollings of some "foo :: foo", which are infinite
streams of naturals. The streams are generated by picking a element (n, foo') from the
support of foo's PMF, use n as the head of the stream and continue corecursively with
foo'. The probability of a single stream should intuitively be the product of all the
probabilities of the random choices according to the PMFs. This is only the intuition, as
the stream is infinite and the resulting distribution is continuous, so the density given
by the product does not exist.
I now want to construct the measure space with the associated measure on the sigma algebra
generated by the usual cylinders on streams. I tried to define the measure on the
cylinders (which can be indexed all finite lists of naturals) and found the function
extend_measure for that. Unfortunately, I have not found many usable theorems about
extend_measure. In the theorem emeasure_extend_measure, e.g., I have to provide a positive
and countably-additive function mu' on the sigma algebra of the cylinders, which is just
what I want to construct. Am I overlooking the obvious? Are there better ways to construct
the measure function I want? The sigma algebra is isomorphic to the infinite indexed
product. My problem is just assigning the right probability to the sets of streams.
Thanks in advance for any pointers and suggestions,
Andreas
PS: I am hooked in a recent snapshot of the development version, so I am happy to use all
the new stuff that will be only available in Isabelle2015. I still post on isabelle-users
as this is a general question about measures in Isabelle which will still be relevant
after the next release.
Email Gateway (Aug 19 2022 at 17:05):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Andreas,
I think you can use the formalization of Markov chains in the locale
MC_syntax in $AFP/Markov_Models/Discrete_Time_Markov_Chain. Here a
Markov chain K is given as the Markov kernel (i.e. transition system)
K :: 's => 's pmf.
In your case the state space is nat * foo, so MC_syntax can be
instantiated with
K == un_Foo o snd
then you get a trace space "T s :: (nat * foo) stream measure". With
T' s == distr (T s) (stream_space (count_space UNIV)) (smap fst)
you construct a "nat stream space". But be aware: you lost some
information, so T' is not the trace space of a Markov chain anymore!
Does this answer your question?
PS: If you want to construct the trace space yourself you want to use
Caratheodories extension theorem in the form of
extend_measure_caratheodory.
But generally I would suggest to avoid this and use the product measure
or the trace space of Markov chains.
Email Gateway (Aug 19 2022 at 17:05):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Johannes,
Thanks for the quick answer. Building on your work seems easier than redoing everything
from scratch. I still have some trouble to define the distribution T', because T' should
have type "foo => ..." rather than "nat * foo => ...". I tried to define T' as
T' s = distr (T (undefined, s)) (stream_space (count_space UNIV)) (smap fst)
but then I have trouble to get a nice recursion equation in the style of
MC_Syntax.nn_integral_T, because I don't know how to show "MC_syntax.walk K (n, foo) =
MC_syntax.walk K (undefined, foo)" for K = "un_Foo o snd". Can you give me a hint?
I also looked at your theory on Markov Decision Processes, which look very interesting.
Unfortunately, I have not been able to really understand them. Can you give me a reference
where I can read up on that? The paper linked from the AFP entry's abstract does not cover
MDPs.
Best,
Andreas
Email Gateway (Aug 19 2022 at 17:05):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Johannes,
Meanwhile, I found a way to prove this using MC_syntax.T_eq_T'.
Sorry for the noise,
Andreas
Last updated: Apr 24 2024 at 16:18 UTC