Introduction

This post shows how a common problem in Computer Science– Trapper Miner– can be implemented in OCaml as a recursive probabilistic program.

We consider a miner who is trapped in a mine. The miner is sent to the mine for times independently, for each time, with probability he is trapped and with the same probability he is safe. When he is trapped, there are 3 doors in the mine for using. The first door leads to a tunnel that will take him to safety after 3 hours (representing by the variable counter). The second door leads to a tunnel that returns him to the mine after 5 hours. And the third door leads to a tunnel that returns him to the mine after 7 hours. At all times, the miner is equally likely to choose any one of the doors, meaning that he chooses any door with equivalent probability .

This is a common problem in a course of foundation of Computer Science. What we are interested in here is what is the number of hours that the miner needs to take to reach safety in average for independent times.

Manual Method

Let’s consider the manual way to compute expected time the miner reaches safety for n independent times. Let be the random variable representing the miner escape time in the time. And let , we are asking for .

We first need to use the law of total expectation to calculate . Let be the event that the miner is trapped, then we have , which is equal to .

Now use again the law of total expectation to calculate . Let be the event that the miner reaches safety in the first try. Then we have , which is .

Thus, . Finally, by linearity of expectation, we get if , otherwise it is .

As we have shown in the above reasoning process, the manual method involves many heuristic theorems and techniques in probability theory and algebra. As a result, it is very hard or impossible to automate. If we use our automatic analyzer, Absynth, that can infer the tightest upper bound on this expected value, the we get the same tightest bound .

Implementation

let rec reach_safe flag counter = 
   if (flag > 0) then
   begin
      let r = Random.int 100 in 
      (* encode the probability 1/3 *)
      if (r < 34) then
        reach_safe 0 (counter + 3)
      else 
      begin
         let r = Random.int 100 in
         (* encode the probability 1/2 *)
         if (r <= 50) then
            reach_safe 1 (counter + 5)
         else
            reach_safe 1 (counter + 7)
      end
   end
   else counter

let rec trapped_miner n counter = 
   let () = assert (n >= 0) in match n with
   | 0 -> counter
   | _ -> 
     let r = Random.int 100 in
     if (r <= 50) then 
        trapped_miner (n - 1) (reach_safe 1 counter)
     else 
        trapped_miner (n - 1) counter

(* testing function *)
let test nr f n =
   let rt = ref 0 in
   for i = 1 to nr do
      let cost = f n 0 in
      rt := (!rt) + cost
   done; 
   (float_of_int (!rt)) /. (float_of_int nr)

The following are the average values of counter when we run trapped_miner for 10000 times.

# test 10000 trapped_miner 10;;
- : float = 74.7524