Document Open Access Logo

On the Taylor Expansion of Probabilistic lambda-terms

Authors Ugo Dal Lago, Thomas Leventis

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2019.13.pdf
  • Filesize: 0.6 MB
  • 16 pages

Document Identifiers

Author Details

Ugo Dal Lago
  • University of Bologna, Italy
  • INRIA Sophia Antipolis, France
Thomas Leventis
  • INRIA Sophia Antipolis, France

Funding

The authors are partially supported by the ERC Consolidator Grant DLV-818616 DIAPASoN, as well as by the ANR projects 14CE250005 ELICA and 16CE250011 REPAS.

Cite AsGet BibTex

Ugo Dal Lago and Thomas Leventis. On the Taylor Expansion of Probabilistic lambda-terms. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.FSCD.2019.13

Abstract

We generalise Ehrhard and Regnier’s Taylor expansion from pure to probabilistic lambda-terms. We prove that the Taylor expansion is adequate when seen as a way to give semantics to probabilistic lambda-terms, and that there is a precise correspondence with probabilistic Böhm trees, as introduced by the second author. We prove this adequacy through notions of probabilistic resource terms and explicit Taylor expansion.

Subject Classification

ACM Subject Classification
  • Theory of computation → Lambda calculus
  • Theory of computation → Equational logic and rewriting
Keywords
  • Probabilistic Lambda-Calculi
  • Taylor Expansion
  • Linear Logic

Metrics

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

Related Versions

References

  1. H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics. Elsevier Science, 1984. Google Scholar
  2. Johannes Borgström, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak. A lambda-calculus foundation for universal probabilistic programming. In Proc. of ICFP 2016, pages 33-46, 2016. Google Scholar
  3. Gérard Boudol. The Lambda-Calculus with Multiplicities. Technical Report 2025, INRIA Sophia-Antipolis, 1993. Google Scholar
  4. Ugo Dal Lago and Thomas Leventis. On the Taylor Expansion of Probabilistic Lambda Terms (Long Version), 2019. URL: http://arxiv.org/abs/1904.09650.
  5. Thomas Ehrhard, Michele Pagani, and Christine Tasson. Full Abstraction for Probabilistic PCF. J. ACM, 65(4):23:1-23:44, 2018. Google Scholar
  6. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theor. Comput. Sci., 309(1-3):1-41, 2003. Google Scholar
  7. Thomas Ehrhard and Laurent Regnier. Böhm Trees, Krivine’s Machine and the Taylor Expansion of Lambda-Terms. In Proc. of CIE 2006, pages 186-197, 2006. Google Scholar
  8. Thomas Ehrhard and Laurent Regnier. Differential interaction nets. Theor. Comput. Sci., 364(2):166-195, 2006. Google Scholar
  9. Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theor. Comput. Sci., 403(2-3):347-372, 2008. Google Scholar
  10. Jean-Yves Girard. Linear Logic. Theor. Comput. Sci., 50:1-102, 1987. Google Scholar
  11. Claire Jones and Gordon D. Plotkin. A Probabilistic Powerdomain of Evaluations. In Proc. of LICS 1989, pages 186-195, 1989. Google Scholar
  12. Emma Kerinec, Giulio Manzonetto, and Michele Pagani. Revisiting Call-by-value Bohm trees in light of their Taylor expansion, 2018. URL: http://arxiv.org/abs/1809.02659.
  13. Thomas Leventis. Probabilistic Böhm Trees and Probabilistic Separation. In Proc. of LICS 2018, pages 649-658, 2018. Google Scholar
  14. Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong. Generalised species of rigid resource terms. In Proc. of LICS 2017, pages 1-12, 2017. Google Scholar
  15. Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong. Species, Profunctors and Taylor Expansion Weighted by SMCC: A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs. In Proc. of LICS 2018, pages 889-898, 2018. Google Scholar
  16. 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
  17. Franck van Breugel, Michael W. Mislove, Joël Ouaknine, and James Worrell. Domain theory, testing and simulation for labelled Markov processes. Theor. Comput. Sci., 333(1-2):171-197, 2005. Google Scholar
  18. Lionel Vaux. The algebraic lambda calculus. Mathematical Structures in Computer Science, 19(5):1029-1059, 2009. Google Scholar
  19. Lionel Vaux Auclair and Federico Olimpieri. On the Taylor expansion of λ-terms and the groupoid structure of their rigid approximants. Informal proc. of TLLA 2018, 2018. 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