Differentials and Distances in Probabilistic Coherence Spaces

Ehrhard, Thomas

doi:10.4230/LIPIcs.FSCD.2019.17

File

LIPIcs.FSCD.2019.17.pdf

Filesize: 0.61 MB
17 pages

Document Identifiers

DOI: 10.4230/LIPIcs.FSCD.2019.17
URN: urn:nbn:de:0030-drops-105243

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 AsGet 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

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.
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.
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.
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.
Vincent Danos and Thomas Ehrhard. Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation, 152(1):111-137, 2011.
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.
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.
Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. MSCS, 28(7):1169-1203, 2018.
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.
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.
Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theoretical Computer Science, 309(1-3):1-41, 2003.
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.
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.
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.
Matthijs Vákár, Ohad Kammar, and Sam Staton. A domain theory for statistical probabilistic programming. PACMPL, 3(POPL):36:1-36:29, 2019.