Example 3: Loopy Probabilistic Program
Example 3: Loopy Probabilistic Program
Example 3: 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
"We note that the statement observe(x) is very related to the statement assume(x) used in program verification literature [2, 15, 42]. Also, we note that observe(x) is equivalent to the while-loop while(!x) skip since the semantics of probabilistic programs is concerned about the normalized distribution of outputs over terminating runs of the program, and ignores non-terminating runs. However, we use the terminology observe(x) because of its common use in probabilistic programming systems [5, 22]." (Gordon et al., 2014)
Loopy PROB-Code for E(Count | C1=1 v C2=1) = 4/3
"The program ... Example 3, is equivalent to the program in Example 2, in which the observe statement has been equivalently encoded using a while loop. The observe statement in line 9 of Example 2 admits only executions that satisfy the condition (c1||c2). The while loop in lines 9-17 has equivalent functionality to the observe statement. If (c1||c2) holds, then the loop exits. If not, it merely re-samples c1 and c2, re-calculates count and checks the condition (c1||c2) again.
In general, observe statements can be encoded using loops. However, the converse is difficult to do without computing loop invariants." (Gordon et al., 2014)
Recursive CHURCH-Code for P(Count | C1=1 v C2=1) and E(Count | C1=1 v C2=1) = 4/3
The PROB-code snippet from Gordon et al. is translated by us to a functional CHURCH program to clarify its semantics. 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 'rejection sampling'. The screen-shot presented was generated by using the PlaySpace environment of WebCHURCH.
