research-article

Open access

Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming

Authors:

Thomas Ehrhard,

Michele Pagani,

Christine TassonAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 2, Issue POPL

Article No.: 59, Pages 1 - 28

https://doi.org/10.1145/3158147

Published: 27 December 2017 Publication History

Abstract

We define a notion of stable and measurable map between cones endowed with measurability tests and show that it forms a cpo-enriched cartesian closed category. This category gives a denotational model of an extension of PCF supporting the main primitives of probabilistic functional programming, like continuous and discrete probabilistic distributions, sampling, conditioning and full recursion. We prove the soundness and adequacy of this model with respect to a call-by-name operational semantics and give some examples of its denotations.

Supplementary Material

WEBM File (measurablecones.webm)

Download
129.64 MB

References

[1]

Tsuyoshi Andô. 1962. On fundamental properties of a Banach space with a cone. Pacific J. Math. 12, 4 (1962), 1163–1169.

[2]

Robert J. Aumann. 1961. Borel structures for function spaces. Illinois J. Math. 5, 4 (12 1961), 614–630. https://projecteuclid.org: 443/euclid.ijm/1255631584

[3]

Tyler Barker. 2016. A monad for randomized algorithms. Ph.D. Dissertation. Tulane University.

[4]

Gérard Berry. 1978. Stable Models of Typed Lambda-calculi. In Automata, Languages and Programming, Fifth Colloquium, Udine, Italy, July 17-21, 1978, Proceedings (Lecture Notes in Computer Science), Vol. 62. Springer, 72–89.

[5]

Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak. 2016. A lambda-calculus foundation for universal probabilistic programming. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.). ACM, 33–46.

Digital Library

[6]

Vincent Danos and Thomas Ehrhard. 2011. Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation 209, 6 (2011), 966–991.

Digital Library

[7]

Vincent Danos and Russel Harmer. 2002. Probabilistic game semantics. ACM Transactions on Computational Logic 3, 3 (July 2002), 359–382.

Digital Library

[8]

Thomas Ehrhard, Michele Pagani, and Christine Tasson. 2011. The Computational Meaning of Probabilistic Coherence Spaces. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science (LICS 2011), Martin Grohe (Ed.). IEEE Computer Society Press, 87–96.

Digital Library

[9]

Thomas Ehrhard, Michele Pagani, and Christine Tasson. 2014. Probabilistic Coherence Spaces are Fully Abstract for Probabilistic PCF. In The 41th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL14, San Diego, USA, P. Sewell (Ed.). ACM.

Digital Library

[10]

Thomas Ehrhard, Michele Pagani, and Christine Tasson. 2017. The cartesian closed category of measurable cones and stable, measurable functions A model for probabilistic higher-order programming. (Oct. 2017). https://hal.archives- ouvertes.fr/ hal- 01622046 working paper or preprint.

[11]

Thomas Ehrhard and Christine Tasson. 2016. Probabilistic call by push value. (2016). Submitted, preprint available at http://arxiv.org/abs/1607.04690.

[12]

Martin Escardó, Martin Hofmann, and Thomas Streicher. 2004. On the non-sequential nature of the interval-domain model of real-number computation. Mathematical Structures in Computer Science 14, 6 (2004), 803–814.

Digital Library

[13]

Martin Escardó. 1996. PCF extended with real numbers. Theoretical Computer Science 162, 1 (1996), 79 – 115.

Digital Library

[14]

Florian Faissole and Bas Spitters. 2017. Synthetic topology in Homotopy Type Theory for probabilistic programming. (2017). available at: https://pps2017.soic.indiana.edu/files/2016/12/ProbProg.pdf .

[15]

Michèle Giry. 1982. A categorical approach to probability theory. Springer Berlin Heidelberg, Berlin, Heidelberg, 68–85.

[16]

Noah D. Goodman and Joshua B. Tenenbaum. 2014. Probabilistic models of cognition. (2014). http://probmods.org.

[17]

Jean Goubault-Larrecq and Daniele Varacca. 2011. Continuous Random Variables. In LICS. IEEE Computer Society, 97–106.

Digital Library

[18]

Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. 2017. A Convenient Category for Higher-Order Probability Theory. In Proceedings of the 32st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’17, Reykjavik, June 20-23, 2017, Joel Ouaknine (Ed.). ACM.

[19]

Daniel Huang and Greg Morrisett. 2017. An application of computable distributions to the semantics of probabilistic programs: part 2. (2017). available at: https://pps2017.soic.indiana.edu/files/2016/12/comp- dist- sem.pdf .

[20]

Claire Jones and Gordon D. Plotkin. 1989. A Probabilistic Powerdomain of Evaluations. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS ’89), Pacific Grove, California, USA, June 5-8, 1989. IEEE Computer Society, 186–195.

[21]

Achim Jung and Regina Tix. 1998. The troublesome probabilistic powerdomain. Electr. Notes Theor. Comput. Sci. 13 (1998), 70–91.

[22]

Klaus Keimel and Gordon D. Plotkin. 2017. Mixed powerdomains for probability and nondeterminism. Logical Methods in Computer Science 13, 1 (2017).

[23]

Dexter Kozen. 1981. Semantics of Probabilistic Programs. J. Comput. System Sci. 22, 3 (1981), 328–350.

[24]

Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. 2013. Weighted relational models of typed lambda-calculi. In 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, June 25-28, 2013. IEEE Computer Society.

Digital Library

[25]

Brockway McMillan. 1954. Absolutely Monotone Functions. Annals of Mathematics 60, 3 (1954), 467–501.

[26]

Michael W. Mislove. 2016. Domains and Random Variables. CoRR abs/1607.07698 (2016). http://arxiv.org/abs/1607.07698

[27]

Prakash Panangaden. 1999. The Category of Markov Kernels. Electronic Notes in Theoretical Computer Science 22 (1999), 171 – 187.

[28]

Sungwoo Park, Frank Pfenning, and Sebastian Thrun. 2008. A Probabilistic Language Based on Sampling Functions. ACM Trans. Program. Lang. Syst. 31, 1, Article 4 (Dec. 2008), 46 pages.

Digital Library

[29]

Gordon D. Plotkin. 1977. LCF Considered as a Programming Language. Theor. Comput. Sci. 5, 3 (1977), 225–255.

[30]

Mathys Rennela. 2016. Convexity and Order in Probabilistic Call-by-Name FPC. CoRR abs/1607.04332 (2016). http: //arxiv.org/abs/1607.04332

[31]

N. Saheb-Djahromi. 1980. CPO’S of Measures for Nondeterminism. Theor. Comput. Sci. 12 (1980), 19–37.

[32]

Peter Selinger. 2004. Toward a semantics for higher-order quantum computation. In Proceedings of the 2nd International Workshop on Quantum Programming Languages, Peter Selinger (Ed.), Vol. 33. TUCS General Publication, 127–143.

[33]

Sam Staton. 2017. Commutative Semantics for Probabilistic Programming. In Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings (Lecture Notes in Computer Science), Hongseok Yang (Ed.), Vol. 10201. Springer, 855–879.

Digital Library

[34]

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 Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016. ACM, 525–534.

Digital Library

[35]

Regina Tix, Klaus Keimel, and Gordon D. Plotkin. 2009. Semantic Domains for Combining Probability and Non-Determinism. Electr. Notes Theor. Comput. Sci. 222 (2009), 3–99.

Digital Library

[36]

Jean Vuillemin. 1988. Exact Real Computer Arithmetic with Continued Fractions. In Proceedings of the 1988 ACM Conference on LISP and Functional Programming (LFP ’88). ACM, New York, NY, USA, 14–27.

Digital Library

[37]

Glynn Winskel. 2014. Probabilistic and Quantum Event Structures. In Horizons of the Mind. A Tribute to Prakash Panangaden - Essays Dedicated to Prakash Panangaden on the Occasion of His 60th Birthday (Lecture Notes in Computer Science), Franck van Breugel, Elham Kashefi, Catuscia Palamidessi, and Jan Rutten (Eds.), Vol. 8464. Springer, 476–497.

Cited By

Di Gianantonio PEdalat ASobocinski PLago UEsparza J(2024)A Cartesian Closed Category for Random VariablesProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662126(1-14)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662126
Goubault-Larrecq JJia XThéron C(2023)A Domain-theoretic Approach to Statistical Programming LanguagesJournal of the ACM10.1145/361166070:5(1-63)Online publication date: 11-Oct-2023
https://dl.acm.org/doi/10.1145/3611660
Tassarotti JTristan J(2023)Verified Density Compilation for a Probabilistic Programming LanguageProceedings of the ACM on Programming Languages10.1145/35912457:PLDI(615-637)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591245
Show More Cited By

Index Terms

Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming
1. Theory of computation

Recommendations

Probabilistic Stable Functions on Discrete Cones are Power Series
LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

We study the category Cstabm of measurable cones and measurable stable functions---a denotational model of an higher-order language with continuous probabilities and full recursion [7]. We look at Cstabm as a model for discrete probabilities, by showing ...
Linear lambda calculus with non-linear first-class continuations
ICSCA '17: Proceedings of the 6th International Conference on Software and Computer Applications

The Curry-Howard isomorphism is the correspondence between propositions and types, proofs and lambda-terms, and proof normalization and evaluation. In Curry-Howard isomorphism, we find a duality between values and continuations in pure functional ...
Higher-order representation of substructural logics
ICFP '10

We present a technique for higher-order representation of substructural logics such as linear or modal logic. We show that such logics can be encoded in the (ordinary) Logical Framework, without any linear or modal extensions. Using this encoding, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 2, Issue POPL

January 2018

1961 pages

EISSN:2475-1421

DOI:10.1145/3177123

Issue’s Table of Contents

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 27 December 2017

Published in PACMPL Volume 2, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

ANR

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

31
Total Citations
View Citations
678
Total Downloads

Downloads (Last 12 months)104
Downloads (Last 6 weeks)14

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Di Gianantonio PEdalat ASobocinski PLago UEsparza J(2024)A Cartesian Closed Category for Random VariablesProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662126(1-14)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662126
Goubault-Larrecq JJia XThéron C(2023)A Domain-theoretic Approach to Statistical Programming LanguagesJournal of the ACM10.1145/361166070:5(1-63)Online publication date: 11-Oct-2023
https://dl.acm.org/doi/10.1145/3611660
Tassarotti JTristan J(2023)Verified Density Compilation for a Probabilistic Programming LanguageProceedings of the ACM on Programming Languages10.1145/35912457:PLDI(615-637)Online publication date: 6-Jun-2023
https://dl.acm.org/doi/10.1145/3591245
Ye WToro MOlmedo F(2023)A Gradual Probabilistic Lambda CalculusProceedings of the ACM on Programming Languages10.1145/35860367:OOPSLA1(256-285)Online publication date: 6-Apr-2023
https://dl.acm.org/doi/10.1145/3586036
Dash SKaddar YPaquet HStaton S(2023)Affine Monads and Lazy Structures for Bayesian ProgrammingProceedings of the ACM on Programming Languages10.1145/35712397:POPL(1338-1368)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571239
Lew AHuot MStaton SMansinghka V(2023)ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic ProgramsProceedings of the ACM on Programming Languages10.1145/35711987:POPL(121-153)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571198
Aguirre ABirkedal L(2023)Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic ChoiceProceedings of the ACM on Programming Languages10.1145/35711957:POPL(33-60)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571195
Di Lavore ERomán M(2023)Evidential Decision Theory via Partial Markov Categories2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175776(1-14)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175776
Dahlqvist FSilva ASmith W(2023)Deterministic stream-sampling for probabilistic programming: semantics and verification2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175773(1-13)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175773
Kerjean MLemay J(2023)Taylor Expansion as a Monad in Models of DiLL2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175753(1-13)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175753
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents