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
"The Lotka-Volterra predator-prey model [37, 57] is a population model which describes how the population of a predator species and prey species evolves over time. It is specified using a system of so called “stoichiometric” reactions as follows:
- G --> 2G
- G + T --> 2T
- T --> 0
We consider an ecosystem with goat (denoted by G) and tiger (denoted by T). The first reaction models goat reproduction. The second reaction models consumption of goat by tiger and consequent increase in tiger. The third reaction models death of tiger due to natural causes.
It turns out that this system can be equivalently modeled as a Continuous Time Markov Chain (CTMC) whose state is an ordered pair (G, T) consisting of the number of goats G and the number of tigers T. The first reaction can be thought of as a transition in the CTMC from state (G, T) to (G + 1, T) and this happens with a rate equal to c1*G, where c1 is some rate constant, and is enabled only when G > 0. Next, the second reaction can be thought of as a transition in the CTMC from state (G, T) to (G - 1, T + 1) and this happens with a rate equal to c2*G*T, where c2 is some rate constant, and is enabled only when G > 0 and T > 0. Finally, the last reaction can be thought of as a transition in the CTMC from state (G, T) to (G, T - 1) and this happens with a rate equal to c3*T, where c3 is some rate constant, and is enabled only when T > 0." (Gordon et al., 2014, p.6).
"Using a process called uniformization, such a CTMC can be modeled using an embedded DTMC, and encoded as a probabilistic program, shown in Figure 10. The program starts with an initial population of goats and tigers and executes the transitions of the Lotka-Volterra model until a prescribed time limit is reached, and returns the resulting population of goats and tigers.
Since the executions are probabilistic, the program models the output distribution of the population of goats and tigers. The body of the while loop
is divided into 3 conditions:
(1) The first condition models the situation when both goats and tigers exist, and models the situation when all 3 reactions are possible.
(2) The second condition models the situation when only goats exist, which is an extreme case, where only reproduction of goats is possible.
(3) The third condition models the situation when only tigers exist, which is another extreme case, where only death of tigers is possible." (Gordon et al., 2014, p.6)
The imperative PROB-code snippet from Gordon et al. is translated by us to a pure 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 50.000 in this run. This number can be increased to get a better precision of estimates. According to the actual TIME_LIMIT (here 0.004) the program computes the PDFs of the state (here for goats and tigers). The screen-shot presented was generated by using the PlaySpace environment of WebCHURCH.