Example 4: Loopy Probabilistic Program
Example 4: Loopy Probabilistic Program
Example 4: Loopy Probabilistic Program
Andrew D. Gordon, Thomas A. Henzinger, Aditya V. Nori, and Sriram K. Rajamani. 2014. Probabilistic programming. In Proceedings of the on Future of Software Engineering (FOSE 2014). ACM, New York, NY, USA, 167-181. DOI=10.1145/2593882.2593900 doi.acm.org/10.1145/2593882.2593900
"In general, observe statements can be encoded using loops. However, the converse is difficult to do without computing loop invariants." (Gordon et al., 2014)
PROB-Code of Loopy Probabilistic Program
"To illustrate this, consider Example 4 on the left side. In this program, the return value of b is 1 iff the while loop in lines 3-7 executes an even number of times, and it is 0 if the while loop executes an odd number of times.
Thus, the expected value of b returned by the program, which is the same as the probability that b is 1, is equal to the probability that the while loop executes an even number of times. The probability that the loop executes 0 times is given by 0.5, since this is the same as the probability that c is assigned 1 in line 3. The probability that the loop executes 2 times is equal to the probability that c is assigned 0 in line 3, and that it is assigned 0 the first time line 6 is executed, and that it is assigned 1 the second time line 6 is executed, which is equal to 0.5^3 since the three assignments to c are each independent Bernoulli trials each with probability 0.5. Summing up this for all even number of executions, we get the geometric series 0.5 + 0.5^3 + 0.5^5 + ... which evaluates to 2/3." (Gordon et al., 2014)
CHURCH-Code of Loopy Probabilistic Program
The PROB-code snippet from Gordon et al. is translated by us to a functional CHURCH program to clarify its semantics. In the code the While-loop is substituted by a simple tail-recursion. The generative model is contained in the CHURCH function "take-a-sample". The number of samples taken was set to 10000 in this run. This number can be increased to get a better precision of estimates. The sampling method used is the simple-to-understand 'forward sampling'. The screen-shot presented was generated by using the PlaySpace environment of WebCHURCH.
