Projects per year
Abstract
Higher-order probabilistic programming languages allow programmers to write sophisticated models in machine learning and statistics in a succinct and structured way, but step outside the standard measure-theoretic formalization of probability theory. Programs may use both higher-order functions and continuous distributions, or even define a probability distribution on functions. But standard probability theory does not handle higher-order functions well: the category of measurable spaces is not cartesian closed.
Here we introduce quasi-Borel spaces. We show that these spaces: form a new formalization of probability theory replacing measurable spaces; form a cartesian closed category and so support higher-order functions; form a well-pointed category and so support good proof principles for equational reasoning; and support continuous probability distributions. We demonstrate the use of quasi-Borel spaces for higher-order functions and probability by: showing that a well-known construction of probability theory involving random functions gains a cleaner expression; and generalizing de Finetti's theorem, that is a crucial theorem in probability theory, to quasi-Borel spaces.
Here we introduce quasi-Borel spaces. We show that these spaces: form a new formalization of probability theory replacing measurable spaces; form a cartesian closed category and so support higher-order functions; form a well-pointed category and so support good proof principles for equational reasoning; and support continuous probability distributions. We demonstrate the use of quasi-Borel spaces for higher-order functions and probability by: showing that a well-known construction of probability theory involving random functions gains a cleaner expression; and generalizing de Finetti's theorem, that is a crucial theorem in probability theory, to quasi-Borel spaces.
Original language | English |
---|---|
Title of host publication | 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) |
Publisher | Institute of Electrical and Electronics Engineers (IEEE) |
Pages | 1-12 |
Number of pages | 12 |
ISBN (Electronic) | 978-1-5090-3018-7 |
ISBN (Print) | 978-1-5090-3019-4 |
DOIs | |
Publication status | Published - 18 Aug 2017 |
Event | 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science - Reykjavik, Reykjavik, Iceland Duration: 20 Jun 2017 → 23 Jun 2017 http://lics.siglog.org/lics17/ |
Publication series
Name | IEEE Symposium on Logic in Computer Science |
---|---|
Publisher | IEEE |
ISSN (Electronic) | 1043-6871 |
Conference
Conference | 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science |
---|---|
Abbreviated title | LICS 2017 |
Country | Iceland |
City | Reykjavik |
Period | 20/06/17 → 23/06/17 |
Internet address |
Fingerprint Dive into the research topics of 'A Convenient Category for Higher-Order Probability Theory'. Together they form a unique fingerprint.
Projects
- 1 Finished
Profiles
-
Chris Heunen
- School of Informatics - Reader
- Laboratory for Foundations of Computer Science
- Foundations of Computation
Person: Academic: Research Active