Hostname: page-component-586b7cd67f-g8jcs Total loading time: 0 Render date: 2024-11-28T04:32:56.807Z Has data issue: false hasContentIssue false
  • English
  • Français

The geometry of Bayesian programming

Published online by Cambridge University Press:  07 December 2021

Ugo Dal Lago  and
Naohiko Hoshino Open the ORCID record for Naohiko Hoshino [Opens in a new window]
Ugo Dal Lago*
Affiliation:
Department of Computer Science and Engineering, University of Bologna, Bologna, Italy
Naohiko Hoshino
Affiliation:
Department of Computer and Information Sciences, Sojo University, Kumamoto, Japan
*
*Corresponding author. Email: [email protected]
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We give two geometry of interaction models for a typed λ-calculus with recursion endowed with operators for sampling from a continuous uniform distribution and soft conditioning, namely a paradigmatic calculus for higher-order Bayesian programming. The models are based on the category of measurable spaces and partial measurable functions, and the category of measurable spaces and s-finite kernels, respectively. The former is proved adequate with respect to both a distribution-based and a sampling-based operational semantics, while the latter is proved adequate with respect to a sampling-based operational semantics.

Keywords

Probabilistic lambda-calculusconditioningBayesian programminggeometry of interaction
Type
Paper
Information
Mathematical Structures in Computer Science , Volume 31 , Issue 6 , June 2021 , pp. 633 - 681
Check for updates
Creative Commons
Creative Common License - CCCreative Common License - BY
This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.
Copyright
© The Author(s), 2021. Published by Cambridge University Press

References

Abramsky, S., Haghverdi, E. and Scott, P. (2002). Geometry of interaction and linear combinatory algebras. Mathematical. Structures in Compter Science 12 (5) 625–665.CrossRefGoogle Scholar
Abramsky, S., Jagadeesan, R. and Malacaria, P. (2000). Full abstraction for PCF. Information and Computation 163 (2) 409–470.CrossRefGoogle Scholar
Abramsky, S. and McCusker, G. (1996). Linearity, sharing and state: a fully abstract game semantics for idealized algol with active expressions: Extended abstract. Electronic Notes in Theoretical Computer Science 3 2–14.CrossRefGoogle Scholar
Agrawal, M., Kayal, N. and Saxena, N. (2002). PRIMES is in P. Annals of Mathematics 2 781–793.Google Scholar
Billingsley, P. (1986). Probability and Measure, second edition. John Wiley and Sons.Google Scholar
Borgström, J., Dal Lago, U., Gordon, A. D. and Szymczak, M. (2016). A lambda-calculus foundation for universal probabilistic programming. In: Proceedings of ICFP 2016, 33–46.CrossRefGoogle Scholar
Breuvart, F. and Dal Lago, U. (2018). On intersection types and probabilistic lambda calculi. In: Proceedings of PPDP 2018, 8:1–8:13.Google Scholar
Castellan, S., Clairambault, P., Paquet, H. and Winskel, G. (2018). The concurrent game semantics of probabilistic PCF. In: Proceedings of LICS 2018, 215–224.CrossRefGoogle Scholar
Cho, K. and Jacobs, B. (2017). Disintegration and bayesian inversion, both abstractly and concretely. to appear in Mathematical Structures in Computer Science.Google Scholar
Clairambault, P. and Paquet, H. (2018). Fully abstract models of the probabilistic lambda-calculus. In: Proceedings of CSL 2018, 16:1–16:17.Google Scholar
Crubillé, R. and Dal Lago, U. (2014). On probabilistic applicative bisimulation and call-by-value λ-calculi. In: Proceedings of ESOP 2014, 209–228.CrossRefGoogle Scholar
Dal Lago, U., Faggian, C., Valiron, B. and Yoshimizu, A. (2017). The geometry of parallelism: classical, probabilistic, and quantum effects. In: Proceedings of POPL 2017, 833–845.Google Scholar
Dal Lago, U. and Grellois, C. (2017). Probabilistic termination by monadic affine sized typing. In: Proceedings of ESOP 2017, 393–419.Google Scholar
Dal Lago, U. and Hoshino, N. (2019a). The geometry of Bayesian programming. CoRR, abs/1904.07425.CrossRefGoogle Scholar
Dal Lago, U. and Hoshino, N. (2019b). The geometry of Bayesian programming. In: 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), 1–13.CrossRefGoogle Scholar
Dal Lago, U., Sangiorgi, D. and Alberti, M. (2014). On coinductive equivalences for higher-order probabilistic functional programs. In: Proceedings of POPL 2014, 297–308.Google Scholar
Danos, V. and Ehrhard, T. (2011). Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation 209 (6) 966–991.CrossRefGoogle Scholar
Danos, V. and Harmer, R. (2002). Probabilistic game semantics. ACM Transactions on Computational Logic 3 (3), 359–382.CrossRefGoogle Scholar
Ehrhard, T., Pagani, M. and Tasson, C. (2018a). Full abstraction for probabilistic PCF. Journal of the ACM 65 (4) 23:1–23:44.CrossRefGoogle Scholar
Ehrhard, T., Pagani, M. and Tasson, C. (2018b). Measurable cones and stable, measurable functions: a model for probabilistic higher-order programming. PACMPL 2(POPL) 59:1–59:28.Google Scholar
Girard, J.-Y. (1987). Linear logic. Theoretical Computer Science 50 (1) 1–101.CrossRefGoogle Scholar
Girard, J.-Y. (1989). Geometry of interaction 1: Interpretation of system F. In: Ferro, R., Bonotto, C., Valentini, S. and Zanardo, A. (eds.), Logic Colloquium 1988, vol. 127. Studies in Logic and the Foundations of Mathematics. Elsevier, 221–260.CrossRefGoogle Scholar
Goodman, N. D., Mansinghka, V. K., Roy, D. M., Bonawitz, K. and Tenenbaum, J. B. (2008). Church: A language for generative models. In: Proceedings of UAI 2008, 220–229.Google Scholar
Hastings, W. K. (1970). Monte carlo sampling methods using markov chains and their applications. Biometrika 57 (1) 97–109.CrossRefGoogle Scholar
Heunen, C., Kammar, O., Staton, S. and Yang, H. (2017). A convenient category for higher-order probability theory. In: Proceedings of LICS 2017. IEEE Computer Society, 1–12.CrossRefGoogle Scholar
Hoshino, N., Muroya, K. and Hasuo, I. (2014). Memoryful geometry of interaction: From coalgebraic components to algebraic effects. In: Proceedings of CSL-LICS 2014.Google Scholar
Hyland, J. M. E. and Ong, C. L. (2000). On full abstraction for PCF: i, ii, and III. Information and Computation 163 (2) 285–408.CrossRefGoogle Scholar
Hyland, M. and Schalk, A. (2003). Glueing and orthogonality for models of linear logic. Theoretical Computer Science 294 (1) 183–231. Category Theory and Computer Science.CrossRefGoogle Scholar
Jacobs, B. (2016). Introduction to Coalgebra: Towards Mathematics of States and Observation . Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.Google Scholar
Jacobs, B., Zanasi, F. and Kissinger, A. (2018). Causal inference by string diagram surgery. arXiv:1811.08338 [cs.LO].Google Scholar
Jones, C. (1990). Probabilistic Non-Determinism. PhD thesis, University of Edinburgh.Google Scholar
Joyal, A., Street, R. and Verity, D. (1996). Traced monoidal categories. Mathematical Proceedings of the Cambridge Philosophical Society 119 (3) 447–468.CrossRefGoogle Scholar
Jung, A. and Tix, R. (1998). The troublesome probabilistic powerdomain. Electronic Notes in Theoretical Computer Science 13 70–91.CrossRefGoogle Scholar
Lafont, Y. (1995). From Proof Nets to Interaction Nets . London Mathematical Society Lecture Note Series. Cambridge University Press, 225–248.Google Scholar
Laurent, O. (2001). A token machine for full geometry of interaction. In: Proceedings of TLCA 2001, 283–297.Google Scholar
Mackie, I. (1995). The geometry of interaction machine. In: Proceedings of POPL 1995, 198–208.CrossRefGoogle Scholar
Metropolis, N., Rosenbluth, A. W., Rosenbluth, M. N., Teller, A. H. and Teller, E. (1953). Equation of state calculations by fast computing machines. The Journal of Chemical Physics 21 (6) 1087–1092.CrossRefGoogle Scholar
Miller, G. L. (1976). Riemann’s hypothesis and tests for primality. Journal of Computer and System Sciences 13 (3) 300–317.CrossRefGoogle Scholar
Moggi, E. (1991). Notions of computation and monads. Information and Computation 93 (1) 55–92. Selections from 1989 IEEE Symposium on Logic in Computer Science.Google Scholar
Muroya, K., Hoshino, N. and Hasuo, I. (2016). Memoryful geometry of interaction ii: Recursion and adequacy. In: Proceedings of POPL 2016, 748–760.CrossRefGoogle Scholar
Paquet, H. and Winskel, G. (2018). Continuous probability distributions in concurrent games. Electronic Notes in Theoretical Computer Science 341 321–344.CrossRefGoogle Scholar
Rabin, M. O. (1980). Probabilistic algorithm for testing primality. Journal of Number Theory 12 (1) 128–138.CrossRefGoogle Scholar
Sato, T., Aguirre, A., Barthe, G., Gaboardi, M., Garg, D. and Hsu, J. (2019). Formal verification of higher-order probabilistic programs: Reasoning about approximation, convergence, Bayesian inference, and optimization. PACMPL 3 38:1–38:30.Google Scholar
Selinger, P. (2011). A Survey of Graphical Languages for Monoidal Categories. Springer Berlin Heidelberg, Berlin, Heidelberg, 289–355.Google Scholar
Staton, S. (2017). Commutative semantics for probabilistic programming. In: Proceedings of ESOP 2017, 855–879.CrossRefGoogle Scholar
Vákár, M., Kammar, O. and Staton, S. (2019). A domain theory for statistical probabilistic programming. Proceedings of the ACM on Programming Languages 3 (POPL) 36:1–36:29.Google Scholar
Wand, M., Culpepper, R., Giannakopoulos, T. and Cobb, A. (2018). Contextual equivalence for a probabilistic language with continuous random variables and recursion. Proceedings of the ACM on Programming Languages 2 (ICFP) 87:1–87:30.Google Scholar
Wood, F. D., van de Meent, J. and Mansinghka, V. (2014). A new approach to probabilistic programming inference. In: Proceedings of AISTATS 2014, 1024–1032.Google Scholar