Document Open Access Logo

Fully Abstract Models of the Probabilistic lambda-calculus

Authors Pierre Clairambault, Hugo Paquet

PDF
Thumbnail PDF

File

LIPIcs.CSL.2018.16.pdf
  • Filesize: 0.58 MB
  • 17 pages

Document Identifiers

Author Details

Pierre Clairambault
  • Univ Lyon, CNRS, ENS de Lyon, UCB Lyon 1, LIP, France
Hugo Paquet
  • Department of Computer Science and Technology, University of Cambridge, UK

Cite AsGet BibTex

Pierre Clairambault and Hugo Paquet. Fully Abstract Models of the Probabilistic lambda-calculus. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 16:1-16:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CSL.2018.16

Abstract

We compare three models of the probabilistic lambda-calculus: the probabilistic Böhm trees of Leventis, the probabilistic concurrent games of Winskel et al., and the weighted relational model of Ehrhard et al. Probabilistic Böhm trees and probabilistic strategies are shown to be related by a precise correspondence theorem, in the spirit of existing work for the pure lambda-calculus. Using Leventis' theorem (probabilistic Böhm trees characterise observational equivalence), we derive a full abstraction result for the games model. Then, we relate probabilistic strategies to the weighted relational model, using an interpretation-preserving functor from the former to the latter. We obtain that the relational model is also fully abstract.

Subject Classification

ACM Subject Classification
  • Theory of computation → Denotational semantics
  • Theory of computation → Probabilistic computation
Keywords
  • Game Semantics
  • Lambda-calculus
  • Probabilistic programming
  • Relational model
  • Full abstraction

Metrics

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

References

  1. Patrick Baillot, Vincent Danos, Thomas Ehrhard, and Laurent Regnier. Timeless games. In International Workshop on Computer Science Logic, pages 56-77. Springer, 1997. Google Scholar
  2. Hendrik Pieter Barendregt. The lambda calculus, volume 2. North-Holland Amsterdam, 1984. Google Scholar
  3. Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak. A Lambda-Calculus Foundation for Universal Probabilistic Programming. CoRR, abs/1512.08990, 2015. URL: http://arxiv.org/abs/1512.08990.
  4. Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. Not enough points is enough. In International Workshop on Computer Science Logic, pages 298-312. Springer, 2007. Google Scholar
  5. Simon Castellan, Pierre Clairambault, Hugo Paquet, and Glynn Winskel. The Concurrent Game Semantics of Probabilistic PCF. In Logic in Computer Science (LICS), 2018 33rd Annual ACM/IEEE Symposium on, page to appear. ACM/IEEE, 2018. Google Scholar
  6. Simon Castellan, Pierre Clairambault, and Glynn Winskel. Symmetry in Concurrent Games. In Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), page 28. ACM, 2014. Google Scholar
  7. Simon Castellan, Pierre Clairambault, and Glynn Winskel. The Parallel Intensionally Fully Abstract Games Model of PCF. In Logic in Computer Science (LICS), 2015 30th Annual ACM/IEEE Symposium on, pages 232-243. IEEE, 2015. Google Scholar
  8. Simon Castellan, Pierre Clairambault, and Glynn Winskel. Concurrent hyland-ong games. arXiv, 2016. URL: http://arxiv.org/abs/1409.7542.
  9. Vincent Danos and Thomas Ehrhard. Probabilistic coherence spaces as a model of higher-order probabilistic computation. Information and Computation, 209(6):966-991, 2011. Google Scholar
  10. Vincent Danos and Russell S Harmer. Probabilistic game semantics. ACM Transactions on Computational Logic (TOCL), 3(3):359-382, 2002. Google Scholar
  11. Thomas Ehrhard, Michele Pagani, and Christine Tasson. The computational meaning of probabilistic coherence spaces. In Logic in Computer Science (LICS), 2011 26th Annual IEEE Symposium on, pages 87-96. IEEE, 2011. Google Scholar
  12. J Martin E Hyland and C-HL Ong. On full abstraction for PCF: I, II, and III. Information and computation, 163(2):285-408, 2000. Google Scholar
  13. Andrew D Ker, Hanno Nickau, and C-H Luke Ong. Innocent game models of untyped λ-calculus. Theoretical Computer Science, 272(1-2):247-292, 2002. Google Scholar
  14. Dexter Kozen. Semantics of probabilistic programs. In Foundations of Computer Science, 1979., 20th Annual Symposium on, pages 101-114. IEEE, 1979. Google Scholar
  15. Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. Weighted relational models of typed lambda-calculi. In Proceedings of the 2013 28th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 301-310. IEEE Computer Society, 2013. Google Scholar
  16. Thomas Leventis. Probabilistic lambda-theories. PhD thesis, Aix-Marseille Université, 2016. Google Scholar
  17. Thomas Leventis. Probabilistic Böhm Trees and Probabilistic Separation. In Logic in Computer Science (LICS), 2018 33rd Annual ACM/IEEE Symposium on. ACM/IEEE, 2018. Google Scholar
  18. Paul-André Mellies. Categorical semantics of linear logic. Panoramas et syntheses, 27:15-215, 2009. Google Scholar
  19. Paul-André Mellies and Samuel Mimram. Asynchronous games: innocence without alternation. In International Conference on Concurrency Theory, pages 395-411. Springer, 2007. Google Scholar
  20. Silvain Rideau and Glynn Winskel. Concurrent strategies. In Logic in Computer Science (LICS), 2011 26th Annual IEEE Symposium on, pages 409-418. IEEE, 2011. Google Scholar
  21. Nasser Saheb-Djahromi. Cpo’s of measures for nondeterminism. Theoretical Computer Science, 12(1):19-37, 1980. Google Scholar
  22. Glynn Winskel. Events in Computation. PhD thesis, University of Edinburgh, 1980. Google Scholar
  23. Glynn Winskel. Event structures with symmetry. Electronic Notes in Theoretical Computer Science, 172:611-652, 2007. Google Scholar
  24. Glynn Winskel. Distributed probabilistic and quantum strategies. Electronic Notes in Theoretical Computer Science, 298:403-425, 2013. 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 Imprint Privacy Contact