×

zbMATH — the first resource for mathematics

Contextual equivalence for probabilistic programs with continuous random variables and scoring. (English) Zbl 06721328
Yang, Hongseok (ed.), Programming languages and systems. 26th European symposium on programming, ESOP 2017, held as part of the European joint conferences on theory and practice of software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 10201, 368-392 (2017).
Summary: We present a logical relation for proving contextual equivalence in a probabilistic programming language (PPL) with continuous random variables and with a scoring operation for expressing observations and soft constraints.{
}Our PPL model is based on a big-step operational semantics that represents an idealized sampler with likelihood weighting. The semantics treats probabilistic non-determinism as a deterministic process guided by a source of entropy. We derive a measure on result values by aggregating (that is, integrating) the behavior of the operational semantics over the entropy space. Contextual equivalence is defined in terms of these measures, taking real events as observable behavior.{
}We define a logical relation and prove it sound with respect to contextual equivalence. We demonstrate the utility of the logical relation by using it to prove several useful examples of equivalences, including the equivalence of a \(\beta_v\)-redex and its contractum and a general form of expression re-ordering. The latter equivalence is sound for the sampling and scoring effects of probabilistic programming but not for effects like mutation or control.
For the entire collection see [Zbl 1360.68021].

MSC:
68Nxx Theory of software
PDF BibTeX Cite
Full Text: DOI
References:
[1] Bizjak, A., Birkedal, L.: Step-indexed logical relations for probability. In: Pitts, A. (ed.) FoSSaCS 2015. LNCS, vol. 9034, pp. 279–294. Springer, Heidelberg (2015). doi: 10.1007/978-3-662-46678-0_18 · Zbl 1459.68031
[2] Borgström, J., Gordon, A.D., Greenberg, M., Margetson, J., Gael, J.V.: Measure transformer semantics for Bayesian machine learning. Log. Methods Comput. Sci. 9(3) (2013) · Zbl 1274.68295
[3] Borgström, J., Lago, U.D., Gordon, A.D., Szymczak, M.: A lambda-calculus foundation for universal probabilistic programming. In: Conference Record of 21st ACM International Conference on Functional Programming, September 2016 · Zbl 1360.68314
[4] Carpenter, B., Gelman, A., Hoffman, M., Lee, D., Goodrich, B., Betancourt, M., Brubaker, M.A., Guo, J., Li, P., Riddell, A.: Stan: a probabilistic programming language. J. Stat. Softw. 20, 1–30 (2016)
[5] Culpepper, R.: Gamble (2015). https://github.com/rmculpepper/gamble
[6] Edalat, A., Escardó, M.H.: Integration in real PCF. Inf. Comput. 160(1), 128–166 (2000) · Zbl 1005.03035
[7] Escardó, M.H.: PCF extended with real numbers. Theoret. Comput. Sci. 162(1), 79–115 (1996) · Zbl 0871.68034
[8] Goodman, N.D., Mansinghka, V.K., Roy, D.M., Bonawitz, K., Tenenbaum, J.B.: Church: a language for generative models. In: UAI, pp. 220–229 (2008)
[9] Huang, D., Morrisett, G.: An application of computable distributions to the semantics of probabilistic programming languages. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 337–363. Springer, Heidelberg (2016). doi: 10.1007/978-3-662-49498-1_14 · Zbl 1335.68028
[10] Kiselyov, O., Shan, C.: Embedded probabilistic programming. In: Taha, W.M. (ed.) DSL 2009. LNCS, vol. 5658, pp. 360–384. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-03034-5_17 · Zbl 05574270
[11] Lieb, E.H., Loss, M.: Analysis. Graduate Studies in Mathematics, vol. 14. American Mathematical Society, Providence (1997)
[12] Lunn, D.J., Thomas, A., Best, N., Spiegelhalter, D.: Winbugs - a Bayesian modelling framework: concepts, structure, and extensibility. Stat. Comput. 10(4), 325–337 (2000)
[13] Mansinghka, V., Selsam, D., Perov, Y.: Venture: a higher-order probabilistic programming platform with programmable inference, March 2014. http://arxiv.org/abs/1404.0099
[14] Minka, T., Winn, J., Guiver, J., Webster, S., Zaykov, Y., Yangel, B., Spengler, A., Bronskill, J.: Infer.NET 2.6. Microsoft Research Cambridge (2014). http://research.microsoft.com/infernet
[15] Narayanan, P., Carette, J., Romano, W., Shan, C., Zinkov, R.: Probabilistic inference by program transformation in hakaru (system description). In: Kiselyov, O., King, A. (eds.) FLOPS 2016. LNCS, vol. 9613, pp. 62–79. Springer, Heidelberg (2016). doi: 10.1007/978-3-319-29604-3_5 · Zbl 06562504
[16] Park, S., Pfenning, F., Thrun, S.: A probabilistic language based on sampling functions. ACM Trans. Program. Lang. Syst. 31(1), 4:1–4:46 (2008) · Zbl 05517453
[17] Pfeffer, A.: Figaro: an object-oriented probabilistic programming language. Technical report, Charles River Analytics (2009)
[18] Ramsey, N., Pfeffer, A.: Stochastic lambda calculus and monads of probability distributions. In: Conference Record of 29th ACM Symposium on Principles of Programming Languages, pp. 154–165 (2002) · Zbl 1323.68150
[19] Sangiorgi, D., Vignudelli, V.: Environmental bisimulations for probabilistic higher-order languages. In: Conference Record of 43rd ACM Symposium on Principles of Programming Languages, POPL 2016, pp. 595–607 (2016) · Zbl 1347.68056
[20] Staton, S., Yang, H., Heunen, C., Kammar, O., Wood, F.: Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In: Proceedings of 31st IEEE Symposium on Logic in Computer Science (2016) · Zbl 1395.68082
[21] Wingate, D., Goodman, N.D., Stuhlmüller, A., Siskind, J.M.: Nonstandard interpretations of probabilistic programs for efficient inference. In: Advances in Neural Information Processing Systems, vol. 24 (2011)
[22] Wood, F., van de Meent, J.W., Mansinghka, V.: A new approach to probabilistic programming inference. In: Proceedings of 17th International Conference on Artificial Intelligence and Statistics, pp. 1024–1032 (2014)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.