The Coq mailing list

[Pierre Corbineau <Pierre.Corbineau AT imag.fr>]

Dear Allyx,

Within Coq, all you can do with Alea distrs is evaluate the probability 
of a certain (computable) event to happen by using the mu function 
(which is actually a projection). This probably isn't what you want.

I think you might try to extract Alea Functions to a randomized Ocaml 
program using the following translation:


Distr A => 'a distr == unit -> 'a (random function)

let draw d = d ();;

Flip => (Random.bool: bool distr)

Munit => fun x => fun () => x :'a -> 'a distr

Mlet => fun d f => f (draw d) : 'a distr -> (a' -> 'b distr) -> 'b distr


Maybe another Pierre can help you there...

Pierre Corbineau



Le 20/05/2011 17:24, Allyx FONTAINE a écrit :
> Hello,
>
> Is there a way to test (complex) functions based on monads used in the
> alea library for randomized algorithm ? I want to know if the functions
> I make really corresponds to what I expect them to do before starting to
> analyze them.
>
> For example, I want to produce a list of bits generated by a coin flip.
> I want to stop it as soon as true is flipped. I made this function below :
>
> Add LoadPath "../alea-v5".
> Require Export Prog.
> Require Import List.
>
> Instance Test_mon :
> monotonic (fun (f: (list nat) -> distr (list nat)) (x: (list nat)) =>
> (Mif Flip (f (1%nat::x)) (Munit (0%nat::x)))).
> red;intros;intro p;apply Mif_le_compat;auto.
> Qed.
>
> Definition Test : ((list nat) -> distr (list nat)) -m> ((list nat) ->
> distr (list nat)) :=
> mon (fun (f: (list nat) -> distr (list nat)) (x: (list nat)) =>
> (Mif Flip (f (1%nat:: x)) (Munit (0%nat::x)))).
>
> This function stops when a false is flipped (and not true as I wanted).
> Is there a means to detect this error ? Are some possible outputs be
> computed ?
>
> Thanks in advance,
> Allyx

--
Pierre Corbineau          | 
Pierre.Corbineau AT imag.fr
VERIMAG - Centre Équation | Tel: (+33 / 0) 4 56 52 04 42
2, avenue de Vignate      | Office nr B18
38610 GIÈRES - FRANCE     | http://www-verimag.imag.fr/~corbinea/
begin:vcard
fn:Pierre Corbineau
n:Corbineau;Pierre
org;quoted-printable:Universit=C3=A9 Joseph Fourier - Grenoble 1;Laboratoire VERIMAG - Polytech' Grenoble
adr;quoted-printable;quoted-printable:2, avenue de Vignate;;VERIMAG - Centre =C3=89QUATION ;GI=C3=88RES ;;38610;France
email;internet:Pierre.Corbineau AT imag.fr
title;quoted-printable:Ma=C3=AEtre de Conf=C3=A9rences
tel;work:+33 (0) 4 56 52 04 42
tel;fax:+33 (0) 4 56 52 03 44
x-mozilla-html:FALSE
url:http://www-verimag.imag.fr/~corbinea
version:2.1
end:vcard