Matthijs Vákár
Abstract
We give an adequate denotational semantics for languages with recursive higher-order types, continuous probability distributions, and soft constraints. These are expressive languages for building Bayesian models of the kinds used in computational statistics and machine learning. Among them are untyped languages, similar to Church and WebPPL, because our semantics allows recursive mixed-variance datatypes. Our semantics justifies important program equivalences including commutativity.
Our new semantic model is based on `quasi-Borel predomains'. These are a mixture of chain-complete partial orders (cpos) and quasi-Borel spaces. Quasi-Borel spaces are a recent model of probability theory that focuses on sets of admissible random elements. Probability is traditionally treated in cpo models using probabilistic powerdomains, but these are not known to be commutative on any class of cpos with higher order functions. By contrast, quasi-Borel predomains do support both a commutative probabilistic powerdomain and higher-order functions. As we show, quasi-Borel predomains form both a model of Fiore's axiomatic domain theory and a model of Kock's synthetic measure theory.
Supplemental Material
Available for Download
A PDF file containing the article together with the supplementary material in the appendices.
- Martin Abadi and Marcelo P Fiore. 1996. Syntactic considerations on recursive types. In Proc. LICS 1996. IEEE, 242–252. Google Scholar
Digital Library
- Nathanael L Ackerman, Cameron E. Freer, and Daniel M. Roy. 2011. Noncomputable conditional distributions. In Proc. LICS 2011. 107–116. Google ScholarDigital Library
- J. Adamek and J. Rosicky. 1994. Locally Presentable and Accessible Categories. Cambridge University Press.Google Scholar
- Giorgio Bacci, Robert Furber, Dexter Kozen, Radu Mardare, Prakash Panangaden, and Dana Scott. 2018. Boolean-valued semantics for the stochastic λ-calculus. In Proc. LICS 2018. Google ScholarDigital Library
- Tyler Barker. 2016. A monad for randomized algorithms, In Proc. MFPS 2016. Electronic Notes in Theoretical Computer Science 325, 47–62.Google ScholarCross Ref
- Ingo Battenfeld, Matthias Schröder, and Alex Simpson. 2007. A convenient category of domains. Electronic Notes in Theoretical Computer Science 172 (2007), 69–99. Google ScholarDigital Library
- Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak. 2016. A lambda-calculus foundation for universal probabilistic programming. In Proc. ICFP 2016. 33–46. Full version at arxiv:abs/1512.08990. Google ScholarDigital Library
- Thomas Ehrhard, Michele Pagani, and Christine Tasson. 2017. Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming. Proceedings of the ACM on Programming Languages 2, POPL (2017), 59. Google ScholarDigital Library
- Marcelo P. Fiore. 1996. Axiomatic Domain Theory in Categories of Partial Maps. Cambridge University Press. Google Scholar
- Marcelo P Fiore and Gordon D Plotkin. 1994. An axiomatisation of computationally adequate domain theoretic models of FPC. In Proc. LICS 1994. 92–102.Google ScholarCross Ref
- Noah Goodman, Vikash Mansinghka, Daniel M Roy, Keith Bonawitz, and Joshua B Tenenbaum. 2008. Church: a language for generative models. In Proc. UAI 2008. Google ScholarDigital Library
- Noah Goodman and Andreas Stuhlmüller. 2014. Design and Implementation of Probabilistic Programming Languages. http://dippl.org . Online book.Google Scholar
- Jean Goubault-Larrecq and Daniele Varacca. 2011. Continuous random variables. In Logic in Computer Science (LICS), 2011 26th Annual IEEE Symposium on. IEEE, 97–106. Google ScholarDigital Library
- Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. 2017. A convenient category for higher-order probability theory. In Proc. LICS 2017.Google ScholarCross Ref
- Daniel Huang, Greg Morrisett, and Bas Spitters. 2018. An application of computable distributions to the semantics of probabilistic programs. (2018). arxiv:1806.07966.Google Scholar
- Claire Jones and Gordon D Plotkin. 1989. A probabilistic powerdomain of evaluations. In Proc. LICS 1989. 186–195. Google ScholarDigital Library
- Achim Jung and Regina Tix. 1998. The troublesome probabilistic powerdomain, In Proc. Comprox 1998. Electronic Notes in Theoretical Computer Science 13, 70–91.Google ScholarCross Ref
- Olav Kallenberg. 2006. Foundations of modern probability. Springer.Google Scholar
- Olav Kallenberg. 2017. Random Measures, Theory and Applications. Probability Theory and Stochastic Modelling, Vol. 77. Springer.Google Scholar
- Ohad Kammar and Gordon D. Plotkin. 2012. Algebraic foundations for effect-dependent optimisations. In Proc. POPL 2012. 349–360. Google ScholarDigital Library
- Alexander Kechris. 2012. Classical descriptive set theory. Vol. 156. Springer Science & Business Media.Google Scholar
- Klaus Keimel and Gordon D Plotkin. 2009. Predicate transformers for extended probability and non-determinism. Mathematical Structures in Computer Science 19, 3 (2009), 501–539. Google ScholarDigital Library
- Oleg Kiselyov and Chung-Chieh Shan. 2009. Embedded probabilistic programming. In Domain-Specific Languages. Springer, 360–384. Google ScholarDigital Library
- Anders Kock. 2012. Commutative monads as a theory of distributions. Theory and Applications of Categories 26, 4 (2012), 97–131.Google Scholar
- Jimmy D. Lawson. 1982. Valuations on continuous lattices. In Continuous Lattices and Related Topics, Rudolf-Eberhard Höffman (Ed.). Mathematik Arbeitspapiere, Vol. 27. Universitat Bremen, 204–225.Google Scholar
- Paul Blain Levy. 2004. Call-By-Push-Value: A Functional/Imperative Synthesis. Kluwer.Google Scholar
- Vikash K. Mansinghka, Daniel Selsam, and Yura N. Perov. 2014. Venture: a higher-order probabilistic programming platform with programmable inference. arXiv:1404.0099 (2014). http://arxiv.org/abs/1404.0099Google Scholar
- Dylan McDermott and Ohad Kammar. 2018. Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics. Proc. MFPS 2018 (2018). To appear.Google Scholar
- Michael W Mislove. 2016. Domains and random variables. arXiv preprint arXiv:1607.07698 (2016).Google Scholar
- Eugenio Moggi. 1989. Computational lambda-calculus and monads. In Proc. LICS 1989. 14–23. Google ScholarDigital Library
- Praveen Narayanan, Jacques Carette, Wren Romano, Chung-chieh Shan, and Robert Zinkov. 2016. Probabilistic inference by program transformation in Hakaru (system description). In Proc. FLOPS 2016. Springer, 62–79.Google ScholarCross Ref
- Federico Olmedo, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Christoph Matheja. 2016. Reasoning about recursive probabilistic programs. In Proc. LICS 2016. 672–681. Google ScholarDigital Library
- Andrew M Pitts. 1996. Relational properties of domains. Inform. Comput. 127, 2 (1996), 66–90.Google ScholarCross Ref
- Gordon D. Plotkin. 1977. LCF Considered as a Programming Language. Theor. Comput. Sci. 5, 3 (1977), 223–255.Google ScholarCross Ref
- Nasser Saheb-Djahromi. 1980. CPO’s of measures for nondeterminism. Theoret. Comput. Sci. 12, 1 (1980), 19–37.Google ScholarCross Ref
- Adam Ścibior, Ohad Kammar, Matthijs Vákár, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani. 2017. Denotational validation of higher-order Bayesian inference. Proc. ACM Program. Lang. 2, POPL, Article 60 (Dec. 2017), 29 pages. Google ScholarDigital Library
- Dana S. Scott. 1993. A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoret. Comput. Sci. 121, 1 (1993), 411–440. Google ScholarDigital Library
- Chung-chieh Shan and Norman Ramsey. 2017. Exact Bayesian inference by symbolic disintegration. In Proc. POPL 2017. 130–144. Google ScholarDigital Library
- Michael B. Smyth and Gordon D. Plotkin. 1982. The category-theoretic solution of recursive domain equations. SIAM J. Comput. 11, 4 (1982), 761–783.Google ScholarDigital Library
- Sam Staton. 2017. Commutative semantics for probabilistic programming. In Proc. ESOP 2017. Google ScholarDigital Library
- Sam Staton, Hongseok Yang, Frank Wood, Chris Heunen, and Ohad Kammar. 2016. Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints. In Proc. LICS 2016. 525–534. Google ScholarDigital Library
- Matthijs Vákár and Luke Ong. 2018. On S-Finite Measures and Kernels. arXiv preprint arXiv:1810.01837 (2018).Google Scholar
- David Wingate, Andreas Stuhlmüller, and Noah Goodman. 2011. Lightweight implementations of probabilistic programming languages via transformational compilation. In Proc. AISTATS 2011.Google Scholar
- Frank Wood, Jan Willem van de Meent, and Vikash Mansinghka. 2014. A new approach to probabilistic programming inference. In Proc. AISTATS 2014. 1024–1032.Google Scholar
Index Terms
- A domain theory for statistical probabilistic programming
Recommendations
Observationally-induced Effect Monads: Upper and Lower Powerspace Constructions
Alex Simpson has suggested to use an observationally-induced approach towards modelling computational effects in denotational semantics. The principal idea is that a single observation algebra is used for defining the computational type structure. He ...
Computational Effects in Topological Domain Theory
This paper contributes towards establishing the category QCB, of topological quotients of countably based spaces, and its subcategory TP, of topological predomains, as a flexible framework for denotational semantics of programming languages. In ...
Observationally-induced Algebras in Domain Theory
We investigate the observationally-induced free algebra approach for constructing computational monads in the categories of classical domain theory. Our investigation yields that the free algebra construction exists for all finitary algebraic signatures ...
Reviews
Santiago Escobar
On the one hand, a statistical programming language is similar to a traditional programming language, but with libraries providing statistical functions. Examples are Mathematica, MATLAB, and the omnipresent R. On the other hand, probabilistic programming aims at providing a model of a probabilistic function or distribution as a program written in a programming language. As an example, WebPPL is a probabilistic extension of JavaScript. Essentially, we define a probabilistic function not mathematically, but as a program that computes an output using a sample from a specific given distribution function. Statistical probabilistic programming aims at their seamless combination. When writing a program in a traditional programming language, each one of its executions must provide an output for each given input. However, when reasoning about programs, we usually cannot compute all the possible executions and use other techniques. A very common one is compositionality. That is, we obtain properties of a given program by composing properties of its inner parts. But when writing a probabilistic program, there is no given input-we are not interested in specific data, but in input distribution functions. That is, the notion of an execution in a traditional program is related not to a concrete execution of the probabilistic program, but to executing the program many times using specific input data taken from an uncertainty distribution and extrapolating the probability associated to the output generated from each input. But reasoning about probabilistic programs becomes much more difficult, and compositionality is a must. This paper explores how the commutativity property of compositionality fails in statistical probabilistic programming and provides a denotational semantics for statistical probabilistic programming with recursive types. The authors use quasi-Borel predomains, which are "a mixture of chain-complete partial orders (CPOs) and quasi-Borel spaces." The main language is statistical FPC (SFPC), a statistical variant of fixed-point calculus (FPC), including sum, product, function, and recursive types; real numbers and measurable functions from reals into reals; a construct for testing real numbers for zero; a construct for random numbers; and a construct for soft constraints.
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments