Example 1b: Two fair coins with an observational constraint
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
"The program in Example 1(b) is slightly different from Example 1(a)—it executes the observe statement observe(c1||c2) before returning the value of (c1; c2). The observe statement blocks runs which do not satisfy the boolean expression c1||c2 and does not permit those executions to happen. Executions that satisfy c1||c2 are permitted to happen. The semantics of the program is the expected return value, conditioned by permitted executions. Since conditioning by permitted executions yields Pr(c1=false, c2=false) = 0, and Pr(c1=false, c2=true) = Pr(c1=true, c2=false) = Pr(c1=true, c2=true) = 1/3, we have that the expected return value is 0x(0, 0) + 1/3x(0, 1) + 1/3x(1, 0) + 1/3 x(1, 1) = (2/3, 2/3)." (Gordon et al., 2014)
The PROB-code snippet from Gordon et al. is translated by us to a functional CHURCH program to clarify its semantics. The code is here. The generative model is contained in the CHURCH function "take-a-sample". The number of necessary samples n was computed by the function hoeffding_invers. The arguments are 1) the tolerated deviation of estimator from parameter: eps = 0.01 and the tolerated deviation probability: p_bound = 0.05. For these numbers the function calculates a minimal number of samples n >= 18444. If eps is set to 0.001 n should be approximately 1.800.000. But then there is a stack overflow in the WebCHURCH platform. The sampling method used is the simple-to-understand 'rejection sampling'. The screen-shot presented was generated by using the PlaySpace environment of WebCHURCH.