Conference item
Densities of almost surely terminating probabilistic programs are differentiable almost everywhere
- Abstract:
- We study the differential properties of higher-order statistical probabilistic programs with recursion and conditioning. Our starting point is an open problem posed by Hongseok Yang: what class of statistical probabilistic programs have densities that are differentiable almost everywhere? To formalise the problem, we consider Statistical PCF (SPCF), an extension of call-by-value PCF with real numbers, and constructs for sampling and conditioning. We give SPCF a sampling-style operational semantics à la Borgström et al., and study the associated weight (commonly referred to as the density) function and value function on the set of possible execution traces. Our main result is that almost surely terminating SPCF programs, generated from a set of primitive functions (e.g. the set of analytic functions) satisfying mild closure properties, have weight and value functions that are almost everywhere differentiable. We use a stochastic form of symbolic execution to reason about almost everywhere differentiability. A by-product of this work is that almost surely terminating deterministic (S)PCF programs with real parameters denote functions that are almost everywhere differentiable. Our result is of practical interest, as almost everywhere differentiability of the density function is required to hold for the correctness of major gradient-based inference algorithms.
- Publication status:
- Published
- Peer review status:
- Reviewed (other)
Actions
Access Document
- Files:
-
-
(Preview, Version of record, 40.9MB, Terms of use)
-
- Publisher copy:
- 10.1007/978-3-030-72019-3_16
Authors
- Publisher:
- Springer
- Host title:
- Proceedings of the 30th European Symposium on Programming (ESOP 2021)
- Journal:
- Lecture Notes in Computer Science More from this journal
- Volume:
- 12648
- Pages:
- 432-461
- Series:
- Lecture Notes in Computer Science
- Publication date:
- 2021-03-23
- Acceptance date:
- 2021-01-28
- Event title:
- 30th European Symposium on Programming, ESOP 2021, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021
- Event website:
- https://etaps.org/2021/esop
- Event start date:
- 2021-03-27
- Event end date:
- 2021-04-01
- DOI:
- ISSN:
-
0302-9743
- Language:
-
English
- Keywords:
- Pubs id:
-
1166367
- Local pid:
-
pubs:1166367
- Deposit date:
-
2021-03-08
Terms of use
- Copyright holder:
- Mak et al.
- Copyright date:
- 2021
- Rights statement:
- © The Author(s) 2021. This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
- Notes:
- This paper will be presented at the 30th European Symposium on Programming (ESOP 2021), 27th March - 1st April 2021.
- Licence:
- CC Attribution (CC BY)
If you are the owner of this record, you can report an update to it here: Report update to this record