Document Open Access Logo

Solvability in a Probabilistic Setting (Invited Talk)

Authors Simona Ronchi Della Rocca, Ugo Dal Lago, Claudia Faggian

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.1.pdf
  • Filesize: 0.55 MB
  • 17 pages

Document Identifiers

Author Details

Simona Ronchi Della Rocca
  • Dipartimento di Informatica, Università di Torino, Italy
Ugo Dal Lago
  • Dipartimento di Informatica, Università di Bologna, Italy
Claudia Faggian
  • Université de Paris, IRIF, CNRS, France

Cite As Get BibTex

Simona Ronchi Della Rocca, Ugo Dal Lago, and Claudia Faggian. Solvability in a Probabilistic Setting (Invited Talk). In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 1:1-1:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.FSCD.2020.1

Abstract

The notion of solvability, crucial in the λ-calculus, is conservatively extended to a probabilistic setting, and a complete characterization of it is given. The employed technical tool is a type assignment system, based on non-idempotent intersection types, whose typable terms turn out to be precisely the terms which are solvable with nonnull probability. We also supply an operational characterization of solvable terms, through the notion of head normal form, and a denotational model of Λ_⊕, itself induced by the type system, which equates all the unsolvable terms.

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Models of computation
Keywords
  • Probabilistic Computation
  • Lambda Calculus
  • Solvability
  • Intersection Types

Metrics

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

References

  1. Martin Avanzini, Ugo Dal Lago, and Alexis Ghyselen. Type-based complexity analysis of probabilistic functional programs. In Proc. of LICS 2019, pages 1-13, 2019. Google Scholar
  2. Martin Avanzini, Ugo Dal Lago, and Akihisa Yamada. On probabilistic term rewriting. In Proc. of FLOPS 2018, pages 132-148, 2018. Google Scholar
  3. H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103. North Holland, 1984. Google Scholar
  4. Flavien Breuvart and Ugo Dal Lago. On intersection types and probabilistic lambda calculi. In David Sabel and Peter Thiemann, editors, Proc. of PPDP 2018, pages 8:1-8:13, 2018. Google Scholar
  5. Pierre Clairambault and Hugo Paquet. Fully abstract models of the probabilistic lambda-calculus. In Proc. of CSL 2018, pages 16:1-16:17, 2018. Google Scholar
  6. Ugo Dal Lago and Charles Grellois. Probabilistic termination by monadic affine sized typing. ACM Trans. Program. Lang. Syst., 41(2):10:1-10:65, 2019. Google Scholar
  7. Ugo Dal Lago, Davide Sangiorgi, and Michele Alberti. On coinductive equivalences for higher-order probabilistic functional programs. In Proc. of POPL 2014, pages 297-308, 2014. Google Scholar
  8. Ugo Dal Lago and Margherita Zorzi. Probabilistic operational semantics for the lambda calculus. RAIRO - Theor. Inf. and Applic., 46(3):413-450, 2012. Google Scholar
  9. Vincent Danos and Thomas Ehrhard. Probabilistic coherence spaces as a model of higher-order probabilistic computation. Inf. Comput., 209(6):966-991, 2011. Google Scholar
  10. Daniel de Carvalho. Execution time of λ-terms via denotational semantics and intersection types. Math. Struct. Comput. Sci., 28(7):1169-1203, 2018. Google Scholar
  11. Alessandra Di Pierro, Chris Hankin, and Herbert Wiklicky. Probabilistic lambda-calculus and quantitative program analysis. J. Log. Comput., 15(2):159-179, 2005. Google Scholar
  12. T. Ehrhard, C. Tasson, and M. Pagani. Probabilistic coherence spaces are fully abstract for probabilistic PCF. In Proc. of POPL 2014, pages 309-320, 2014. Google Scholar
  13. Thomas Ehrhard, Michele Pagani, and Christine Tasson. The computational meaning of probabilistic coherence spaces. In Proc. of LICS 2011, pages 87-96, 2011. Google Scholar
  14. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theor. Comput. Sci., 309(1-3):1-41, 2003. Google Scholar
  15. Claudia Faggian and Simona Ronchi Della Rocca. Lambda calculus and probabilistic computation. In Proc. of LICS 2019, pages 1-13, 2019. Google Scholar
  16. Jean Goubault-Larrecq. A probabilistic and non-deterministic call-by-push-value language. In Proc. of LICS 2019, pages 1-13, 2019. Google Scholar
  17. Claire Jones. Probabilistic non-determinism. PhD thesis, University of Edinburgh, UK, 1990. Google Scholar
  18. Achim Jung and Regina Tix. The troublesome probabilistic powerdomain. Electron. Notes Theor. Comput. Sci., 13:70-91, 1998. Google Scholar
  19. Simona Kasterovic and Michele Pagani. The discriminating power of the let-in operator in the lazy call-by-name probabilistic lambda-calculus. In Proc. of FSCD 2019, pages 26:1-26:20, 2019. Google Scholar
  20. Jonathan Katz and Yehuda Lindell. Introduction to Modern Cryptography. Chapman & Hall Cryptography and Network Security Series. Chapman & Hall, 2007. Google Scholar
  21. J. Laird, G. Manzonetto, G. McCusker, and M. Pagani. Weighted relational models of typed lambda-calculi. In proc. of LICS 2013, pages 301-310, 2013. Google Scholar
  22. Thomas Leventis. Probabilistic lambda-theories. Phd Thesis, Aix-Marseille Université, 2016. Available at URL: https://tel.archives-ouvertes.fr/tel-01427279v2/document.
  23. Thomas Leventis. Probabilistic böhm trees and probabilistic separation. In Proc. of LICS 2018, pages 649-658, 2018. Google Scholar
  24. Thomas Leventis and Michele Pagani. Strong adequacy and untyped full-abstraction for probabilistic coherence spaces. In Proc. of FoSSaCS 2019, pages 365-381, 2019. Google Scholar
  25. Rajeev Motwani and Prabhakar Raghavan. Randomized Algorithms. Cambridge University Press, 1995. Google Scholar
  26. Luca Paolini, Mauro Piccolo, and Simona Ronchi Della Rocca. Essential and relational models. Math. Struct. Comput. Sci., 27(5):626-650, 2017. Google Scholar
  27. Sungwoo Park. A calculus for probabilistic languages. In Proc. of TLDI 2003, pages 38-49, 2003. Google Scholar
  28. Gordon D. Plotkin. Call-by-name, call-by-value and the lambda-calculus. Theor. Comput. Sci., 1(2):125-159, 1975. Google Scholar
  29. Norman Ramsey and Avi Pfeffer. Stochastic lambda calculus and monads of probability distributions. In Proc. of POPL 2002, pages 154-165, 2002. Google Scholar
  30. Simona Ronchi Della Rocca and Luca Paolini. The Parametric Lambda Calculus - A Metamodel for Computation. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. Google Scholar
  31. N. Saheb-Djahromi. Probabilistic LCF. In Proc. of MFCS 1978, pages 442-451, 1978. Google Scholar
  32. Lionel Vaux. The algebraic lambda calculus. Mathematical Structures in Computer Science, 19(5):1029-1059, 2009. 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