# 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 http://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.