Document Open Access Logo

Differentials and Distances in Probabilistic Coherence Spaces

Author Thomas Ehrhard

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2019.17.pdf
  • Filesize: 0.61 MB
  • 17 pages

Document Identifiers

Author Details

Thomas Ehrhard
  • CNRS, IRIF, Université de Paris, France

Acknowledgements

We thank Raphaëlle Crubillé, Paul-André Melliès, Michele Pagani and Christine Tasson for many enlightening discussions on this work. We also thank the referees for their precious comments and suggestions.

Cite As Get BibTex

Thomas Ehrhard. Differentials and Distances in Probabilistic Coherence Spaces. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSCD.2019.17

Abstract

In probabilistic coherence spaces, a denotational model of probabilistic functional languages, morphisms are analytic and therefore smooth. We explore two related applications of the corresponding derivatives. First we show how derivatives allow to compute the expectation of execution time in the weak head reduction of probabilistic PCF (pPCF). Next we apply a general notion of "local" differential of morphisms to the proof of a Lipschitz property of these morphisms allowing in turn to relate the observational distance on pPCF terms to a distance the model is naturally equipped with. This suggests that extending probabilistic programming languages with derivatives, in the spirit of the differential lambda-calculus, could be quite meaningful.

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Probabilistic computation
  • Theory of computation → Abstract machines
  • Theory of computation → Linear logic
Keywords
  • Denotational semantics
  • probabilistic coherence spaces
  • differentials of programs

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak. A lambda-calculus foundation for universal probabilistic programming. In Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, editors, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pages 33-46. ACM, 2016. Google Scholar
  2. Simon Castellan, Pierre Clairambault, Hugo Paquet, and Glynn Winskel. The concurrent game semantics of Probabilistic PCF. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 215-224. ACM, 2018. URL: http://dx.doi.org/10.1145/3209108.
  3. Raphaëlle Crubillé. Probabilistic Stable Functions on Discrete Cones are Power Series. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 275-284. ACM, 2018. URL: http://dx.doi.org/10.1145/3209108.3209198.
  4. Raphaëlle Crubillé and Ugo Dal Lago. Metric Reasoning About Lambda-Terms: The General Case. In Hongseok Yang, editor, 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, volume 10201 of Lecture Notes in Computer Science, pages 341-367. Springer, 2017. URL: http://dx.doi.org/10.1007/978-3-662-54434-1_13.
  5. Vincent Danos and Thomas Ehrhard. Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation, 152(1):111-137, 2011. Google Scholar
  6. Vincent Danos and Russell Harmer. Probabilistic game semantics. In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society, 2000. Google Scholar
  7. Daniel de Carvalho. Execution Time of lambda-Terms via Denotational Semantics and Intersection Types. CoRR, abs/0905.4251, 2009. URL: http://arxiv.org/abs/0905.4251.
  8. Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. MSCS, 28(7):1169-1203, 2018. Google Scholar
  9. Thomas Ehrhard. An introduction to differential linear logic: proof-nets, models and antiderivatives. Mathematical Structures in Computer Science, 28(7):995-1060, 2018. URL: http://dx.doi.org/10.1017/S0960129516000372.
  10. Thomas Ehrhard, Michele Pagani, and Christine Tasson. Full Abstraction for Probabilistic PCF. Journal of the ACM, 65(4):23:1-23:44, 2018. URL: http://dx.doi.org/10.1145/3164540.
  11. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theoretical Computer Science, 309(1-3):1-41, 2003. Google Scholar
  12. Jean-Yves Girard. Between logic and quantic: a tract. In Thomas Ehrhard, Jean-Yves Girard, Paul Ruet, and Philip Scott, editors, Linear Logic in Computer Science, volume 316 of London Mathematical Society Lecture Notes Series, pages 346-381. Cambridge University Press, 2004. Google Scholar
  13. Klaus Keimel and Gordon D. Plotkin. Mixed powerdomains for probability and nondeterminism. Logical Methods in Computer Science, 13(1), 2017. URL: http://dx.doi.org/10.23638/LMCS-13(1:2)2017.
  14. Peter Selinger. Towards a semantics for higher-order quantum computation. In Proceedings of the 2nd International Workshop on Quantum Programming Languages, Turku, Finland, number 33 in TUCS General Publication. Turku Centre for Computer Science, 2004. Google Scholar
  15. Matthijs Vákár, Ohad Kammar, and Sam Staton. A domain theory for statistical probabilistic programming. PACMPL, 3(POPL):36:1-36:29, 2019. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact