Example 7: The Fair Die (Discrete Time Markov Chain)
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
"This simple probabilistic algorithm due to Knuth and Yao [KY76]. for emulating a 6-sided die with a fair coin. The idea of the algorithm is as follows. Starting from step 0 (i.e. the circle labelled 0), at every step a coin is tossed and there is 50% chance of taking each of the two possible choices. The algorithm terminates when you reach one of the values for the die on the right-hand side" (PRISM-Tutorial)
"The DTMC-graph (left) shows an example with 13 vertices. The DTMC implements the Knuth-Yao algorithm for obtaining a fair die from fair coin tosses. It turns out that the steady state probability pi(v) for each of the vertices 11 through 16 is 1/6 and for each of the other vertices is 0. Every DTMC can be encoded as a probabilistic program. Cycles in the DTMC graph can be encoded using while-loops in the probabilistic program.
Unlike the semantics we have given for probabilistic programs, which considers terminating runs (which are finite), the semantics of DTMCs inherently considers infinite runs. However, in cases where every terminal SCC (strongly-connected component) of a DTMC is a singleton vertex (which is the case, here), we can terminate the execution of the probabilistic program on reaching the terminal SCC..." (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 generative model is contained in the CHURCH function "take-a-sample". The number of samples taken was set to 30.000 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.