*To*: Johannes HÃlzl <hoelzl at in.tum.de>, <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Measure definition on streams*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Wed, 25 Feb 2015 12:33:10 +0100*In-reply-to*: <54EDA844.5070604@inf.ethz.ch>*References*: <54ECA47B.5050707@inf.ethz.ch> <1424816504.24000.23.camel@lapnipkow5> <54EDA844.5070604@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.4.0

Dear Johannes, Meanwhile, I found a way to prove this using MC_syntax.T_eq_T'. Sorry for the noise, Andreas On 25/02/15 11:47, Andreas Lochbihler wrote:

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 On 24/02/15 23:21, Johannes HÃlzl wrote: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? - Johannes 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. Am Dienstag, den 24.02.2015, 17:19 +0100 schrieb Andreas Lochbihler: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.

**References**:**[isabelle] Measure definition on streams***From:*Andreas Lochbihler

**Re: [isabelle] Measure definition on streams***From:*Johannes Hölzl

**Re: [isabelle] Measure definition on streams***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Measure definition on streams
- Next by Date: Re: [isabelle] Typo in Tutorial?
- Previous by Thread: Re: [isabelle] Measure definition on streams
- Next by Thread: [isabelle] Typo in Tutorial?
- Cl-isabelle-users February 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list