The Coq mailing list

[Fontaine Allyx <fontaine AT labri.fr>]

Le 23/05/2011 11:18, AUGER Cedric a écrit :
> Le Sun, 22 May 2011 17:41:50 +0200,
> David 
> Baelde<david.baelde AT gmail.com>
>   a écrit :
>
> > Hi Allyx,
> >
> > If you haven't already, you should have a look at the paper by
> > Audebaud&  Paulin (http://dx.doi.org/10.1016/j.scico.2007.09.002)
> > about the ALEA library. It starts with a gentle introduction to the
> > monad that is used, detailing its advantages and drawbacks.
> >
> > There are mainly two ways of representing probabilistic algorithms. A
> > computation returning objects of type 'a can be represented either as
> > (unit ->  'a) or ('a ->  [0,1]). The first approach is suitable for
> > simulations: it gives you a function that you can re-run as many times
> > as you wish, possibly getting different results each time, because the
> > function relies on some random generator. The second approach, used in
> > ALEA, models the computation as a probability distribution. It is an
> > exact approach: for a given x of type 'a it should return the
> > probability that this x is obtained. But this will be unusable for
> > testing.
> >
> > Long story short, Pierre Corbineau's solution will work. However, I
> > wouldn't bother to make extraction work for such small examples: just
> > rewrite the code in ML yourself.
> >
> > Have fun,
>
> I also guess that if "'a" is a type which cardinality is quite small,
> and you can extract [0,1] to float, then you can write a short ML code:
>
> let dice_throw =
>    let sieve = Random.float 1. in
>    let rec get_rand acc l =
>      match l with
>      | v::l ->  let acc = acc + μ v in
>                if acc>  sieve then v else get_rand acc l
>      | [] ->  failwith "Hmm, this is unexpected!"
>    in get_rand 0 [list of all the elements of your type]
>
> of course if you have big types for 'a such as int it can be too long
> and even false due to rounding errors (the failwith case can even
> occur).
> You also have to identify the "μ" function (if it is the one I think
> of, it is also called μ in Alea, so it should be extracted to its
> Unicode code, as unicode is not supported by OCaml, leading to some
> awfull identifier).
> Even in this case, I am not sure it can be very usefull, but if it is,
> then you won't have to rewrite all the ML code, and won't have to play
> with the Extraction mechanism too much (and using P. Corbineau
> solution seems also hazardous, as you change the extracted objects to
> objects which are semantically very different; furthermore, using
> side effects can mess a lot with extraction if some optimizations are
> performed ("let x = side_effect () in let y = side_effect () in ..."
> could be extracted to "let x = side_effect () in let y = x in ..." as
> well as identity due to Coq semantics, but the two functions are
> clearly different with OCaml)).

Thanks for your answers!

Actually, as I have several examples more or less simple, I would like 
to have an automatic way which ensures that Ocaml functions really 
corresponds to Coq functions. But as I don't know well all those 
mechanisms, I indeed begin with writting ML code by myself and having a 
look at extraction.

I am not sure of my understanding of the role of the accumulator in 
dice_throw. Is it needed to return an element of my type uniformly at 
random thanks to the μ function? Does the failwith case not be reached 
because the sum of the probabilities is supposed to be greater than 1?

Allyx