Library ALEA.Choice

Choice.v: An example of probabilistic choice

Require Export Prog.
Set Implicit Arguments.

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))).

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.
If Q is a boolean function it means than if one of x or y satisfies Q then (choice~x~y) will also satisfy Q
Hypothesis p1_terminates : (mu p1 (fone A))==1.
Hypothesis p2_terminates : (mu p2 (fone A))==1.

Variable Q : MF A.
Hypothesis choiceok : forall x y, Q x + Q y <= Q (choice x y).

Proof of estimation:

ok k1 p1 Q and ok k2 p2 Q implies ok (k1(1-k2)+k2) p Q

Lemma choicerule : forall k1 k2,
  k1 <= mu p1 Q -> k2 <= mu p2 Q -> (k1 * ([1-] k2) + k2) <= mu p Q.

End CHOICE.