Library ALEA.Choice
Definition of a probabilistic choice
We interpret the probabilistic program p which executes two probabilistic programs p1 and p2 and then make a choice between the two computed results.let rec p () = let x = p1 () in let y = p2 () in choice x y
Section CHOICE.
Variable A : Type.
Variables p1 p2 : distr A.
Variable choice : A -> A -> A.
Definition p : distr A := Mlet p1 (fun x => Mlet p2 (fun y => Munit (choice x y))).
Variable A : Type.
Variables p1 p2 : distr A.
Variable choice : A -> A -> A.
Definition p : distr A := Mlet p1 (fun x => Mlet p2 (fun y => Munit (choice x y))).
Main result
We estimate the probability for p to satisfy Q given estimations for both p1 and p2.Assumptions
We need extra properties on p1, p2 and choice.- p1 and p2 terminate with probability 1
- Q value on choice is not less than the sum of values of Q on separate elements.