A convenient category for higher-order probability theory
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...
| Main Authors: | , , , |
|---|---|
| Format: | Conference item |
| Published: |
IEEE
2017
|
| _version_ | 1826259146331127808 |
|---|---|
| author | Heunen, C Kammar, O Staton, S Yang, H |
| author_facet | Heunen, C Kammar, O Staton, S Yang, H |
| author_sort | Heunen, C |
| collection | OXFORD |
| description | 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. |
| first_indexed | 2024-03-06T18:45:15Z |
| format | Conference item |
| id | oxford-uuid:0e477a89-389f-4a4d-8dc2-7a86d525552e |
| institution | University of Oxford |
| last_indexed | 2024-03-06T18:45:15Z |
| publishDate | 2017 |
| publisher | IEEE |
| record_format | dspace |
| spelling | oxford-uuid:0e477a89-389f-4a4d-8dc2-7a86d525552e2022-03-26T09:45:07ZA convenient category for higher-order probability theoryConference itemhttp://purl.org/coar/resource_type/c_5794uuid:0e477a89-389f-4a4d-8dc2-7a86d525552eSymplectic Elements at OxfordIEEE2017Heunen, CKammar, OStaton, SYang, HHigher-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. |
| spellingShingle | Heunen, C Kammar, O Staton, S Yang, H A convenient category for higher-order probability theory |
| title | A convenient category for higher-order probability theory |
| title_full | A convenient category for higher-order probability theory |
| title_fullStr | A convenient category for higher-order probability theory |
| title_full_unstemmed | A convenient category for higher-order probability theory |
| title_short | A convenient category for higher-order probability theory |
| title_sort | convenient category for higher order probability theory |
| work_keys_str_mv | AT heunenc aconvenientcategoryforhigherorderprobabilitytheory AT kammaro aconvenientcategoryforhigherorderprobabilitytheory AT statons aconvenientcategoryforhigherorderprobabilitytheory AT yangh aconvenientcategoryforhigherorderprobabilitytheory AT heunenc convenientcategoryforhigherorderprobabilitytheory AT kammaro convenientcategoryforhigherorderprobabilitytheory AT statons convenientcategoryforhigherorderprobabilitytheory AT yangh convenientcategoryforhigherorderprobabilitytheory |