License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2017.4
URN: urn:nbn:de:0030-drops-77456
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2017/7745/
Go to the corresponding LIPIcs Volume Portal

Tasson, Christine

Quantitative Semantics for Probabilistic Programming (Invited Talk)

pdf-format:
LIPIcs-FSCD-2017-4.pdf (0.2 MB)

Abstract

Probabilistic programming has many applications in statistics, physics, ... so that all programming languages have been equipped with probabilistic library. However, there is a need in developing semantical tools in order to formalize higher order and recursive probabilistic languages. Indeed, it is well known that categories of measurable spaces are not Cartesian closed. We have been studying quantitative semantics of probabilistic spaces to fill this gap. A first step has been to focus on probabilistic programming languages with discrete types such as integers and booleans. In this setting, probabilistic programs can be seen as linear combinations of deterministic programs. Probabilistic Coherent Spaces constitute a Cartesian closed category that is fully abstract with respect to probabilistic Call-By-Push-Value. Moreover, this toy language is endowed with a memorization operator that allow to encode most discrete probabilistic programs. The second step is to move on probabilistic programming with continuous types representing for instance reals endowed with Lebesgue measurable sets. We introduce the category of cones and stable functions which is Cartesian closed. The trick is to enlarge the category of measurable spaces to gain closeness and to embrace measurable spaces. Besides, the category of cones is a sound and adequate model of a higher order and recursive probabilistic language in which most classical distributions and probabilistic tools can be encoded. This is joint work with Thomas Ehrhard and Michele Pagani.

BibTeX - Entry

@InProceedings{tasson:LIPIcs:2017:7745,
  author =	{Christine Tasson},
  title =	{{Quantitative Semantics for Probabilistic Programming (Invited Talk)}},
  booktitle =	{2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)},
  pages =	{4:1--4:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-047-7},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{84},
  editor =	{Dale Miller},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2017/7745},
  URN =		{urn:nbn:de:0030-drops-77456},
  doi =		{10.4230/LIPIcs.FSCD.2017.4},
  annote =	{Keywords: denotational semantics, probabilistic programming, programming language, probability}
}

Keywords: denotational semantics, probabilistic programming, programming language, probability
Collection: 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
Issue Date: 2017
Date of publication: 30.08.2017

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI