Document Open Access Logo

The Discriminating Power of the Let-In Operator in the Lazy Call-by-Name Probabilistic lambda-Calculus

Authors Simona Kašterović, Michele Pagani

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2019.26.pdf
  • Filesize: 0.61 MB
  • 20 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
Keywords
  • probabilistic lambda calculus
  • bisimulation
  • Howe’s technique
  • context equivalence
  • testing

Metrics

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

Abstract

We consider the notion of probabilistic applicative bisimilarity (PAB), recently introduced as a behavioural equivalence over a probabilistic extension of the untyped lambda-calculus. Alberti, Dal Lago and Sangiorgi have shown that PAB is not fully abstract with respect to the context equivalence induced by the lazy call-by-name evaluation strategy. We prove that extending this calculus with a let-in operator allows for achieving the full abstraction. In particular, we recall Larsen and Skou’s testing language, which is known to correspond with PAB, and we prove that every test is representable by a context of our calculus.

Cite As Get BibTex

Simona Kašterović and Michele Pagani. The Discriminating Power of the Let-In Operator in the Lazy Call-by-Name Probabilistic lambda-Calculus. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.FSCD.2019.26

Author Details

Simona Kašterović
  • Faculty of Technical Sciences, University of Novi Sad , Trg Dositeja Obradovića 6, 21000 Novi Sad, Serbia
Michele Pagani
  • IRIF, University Paris Diderot - Paris 7, France

Acknowledgements

We wish to thank the anonymous reviewers for their valuable suggestions, helping us to improve the paper.

References

  1. Samson Abramsky. Research Topics in Functional Programming, chapter The Lazy Lambda Calculus, pages 65-116. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1990. URL: http://dl.acm.org/citation.cfm?id=119830.119834.
  2. Pierre Clairambault and Hugo Paquet. Fully Abstract Models of the Probabilistic lambda-calculus. In Dan R. Ghica and Achim Jung, editors, 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK, volume 119 of LIPIcs, pages 16:1-16:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. URL: http://dx.doi.org/10.4230/LIPIcs.CSL.2018.16.
  3. Raphaëlle Crubillé and Ugo Dal Lago. On Probabilistic Applicative Bisimulation and Call-by-Value λ-Calculi. In Programming Languages and Systems - 23rd European Symposium on Programming, ESOP 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings, pages 209-228, 2014. URL: http://dx.doi.org/10.1007/978-3-642-54833-8_12.
  4. Raphaëlle Crubillé, Ugo Dal Lago, Davide Sangiorgi, and Valeria Vignudelli. On Applicative Similarity, Sequentiality, and Full Abstraction. In Correct System Design - Symposium in Honor of Ernst-Rüdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings, pages 65-82, 2015. URL: http://dx.doi.org/10.1007/978-3-319-23506-6_7.
  5. Ugo Dal Lago, Francesco Gavazzo, and Ryo Tanaka. Effectful Applicative Similarity for Call-by-Name Lambda Calculi. In Dario Della Monica, Aniello Murano, Sasha Rubin, and Luigi Sauro, editors, Joint Proceedings of the 18th Italian Conference on Theoretical Computer Science and the 32nd Italian Conference on Computational Logic co-located with the 2017 IEEE International Workshop on Measurements and Networking (2017 IEEE M&N), Naples, Italy, September 26-28, 2017., volume 1949 of CEUR Workshop Proceedings, pages 87-98. CEUR-WS.org, 2017. Google Scholar
  6. Ugo Dal Lago, Davide Sangiorgi, and Michele Alberti. On Coinductive Equivalences for Higher-Order Probabilistic Functional Programs (Long Version). CoRR, abs/1311.1722, 2013. URL: http://arxiv.org/abs/1311.1722.
  7. Ugo Dal Lago, Davide Sangiorgi, and Michele Alberti. On coinductive equivalences for higher-order probabilistic functional programs. In The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, San Diego, CA, USA, January 20-21, 2014, pages 297-308, 2014. URL: http://dx.doi.org/10.1145/2535838.2535872.
  8. Ugo Dal Lago and Margherita Zorzi. Probabilistic operational semantics for the lambda calculus. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, 46(3):413-450, 2012. URL: http://dx.doi.org/10.1051/ita/2012012.
  9. Thomas Ehrhard, Michele Pagani, and Christine Tasson. The Computational Meaning of Probabilistic Coherence Spaces. In Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, LICS 2011, June 21-24, 2011, Toronto, Ontario, Canada, pages 87-96, 2011. URL: http://dx.doi.org/10.1109/LICS.2011.29.
  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. Jean-Yves Girard. Linear Logic. Theoretical Computer Science, 50:1-102, 1987. URL: http://dx.doi.org/10.1016/0304-3975(87)90045-4.
  12. Kim Guldstrand Larsen and Arne Skou. Bisimulation through Probabilistic Testing. Information and Computation, 94(1):1-28, 1991. URL: http://dx.doi.org/10.1016/0890-5401(91)90030-6.
  13. Thomas Leventis. Probabilistic Böhm Trees and Probabilistic Separation. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 649-658, 2018. URL: http://dx.doi.org/10.1145/3209108.3209126.
  14. Thomas Leventis and Michele Pagani. Strong Adequacy and Untyped Full Abstraction for Probabilistic Coherence Spaces. accepted to FOSSACS 2019, 2019. Google Scholar
  15. Sungwoo Park, Frank Pfenning, and Sebastian Thrun. A Probabilistic Language Based on Sampling Functions. ACM Transactions on Programming Languages and Systems, 31(1):4:1-4:46, December 2008. URL: http://dx.doi.org/10.1145/1452044.1452048.
  16. Franck Van Breugel, Michael W. Mislove, Joël Ouaknine, and James Worrell. Domain theory, testing and simulation for labelled Markov processes. Theoretical Computer Science, 333(1-2):171-197, 2005. URL: http://dx.doi.org/10.1016/j.tcs.2004.10.021.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact