Document Open Access Logo

Taylor expansion for Call-By-Push-Value

Authors Jules Chouquet , Christine Tasson

PDF

File

Thumbnail PDF
PDF
LIPIcs.CSL.2020.16.pdf
  • Filesize: 0.63 MB
  • 16 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • Call-By-Push-Value
  • Quantitative semantics
  • Taylor expansion
  • Linear Logic

Metrics

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

Abstract

The connection between the Call-By-Push-Value lambda-calculus introduced by Levy and Linear Logic introduced by Girard has been widely explored through a denotational view reflecting the precise ruling of resources in this language. We take a further step in this direction and apply Taylor expansion introduced by Ehrhard and Regnier. We define a resource lambda-calculus in whose terms can be used to approximate terms of Call-By-Push-Value. We show that this approximation is coherent with reduction and with the translations of Call-By-Name and Call-By-Value strategies into Call-By-Push-Value.

Cite As Get BibTex

Jules Chouquet and Christine Tasson. Taylor expansion for Call-By-Push-Value. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 16:1-16:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CSL.2020.16

Author Details

Jules Chouquet
  • IRIF UMR 8243, Université de Paris, CNRS, France
Christine Tasson
  • IRIF UMR 8243, Université Paris Diderot, Sorbonne Paris Cité, CNRS, France

Funding

This work was supported by french ANR project Rapido (ANR number: ANR-14-CE25-0007).

Acknowledgements

The authors thank the ANR project Rapido, together with Lionel Vaux and Thomas Ehrhard for their useful advises and fertile discussions.

References

  1. Samson Abramsky and Guy McCusker. Call-by-Value Games. In CSL, volume 1414 of Lecture Notes in Computer Science, pages 1-17. Springer, 1997. Google Scholar
  2. J. Chouquet. Taylor expansion, finiteness and strategies. In MFPS 2019, 2019. Google Scholar
  3. Jules Chouquet and Lionel Vaux Auclair. An Application of Parallel Cut Elimination in Unit-Free Multiplicative Linear Logic to the Taylor Expansion of Proof Nets. In CSL, volume 119 of LIPIcs, pages 15:1-15:17. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2018. Google Scholar
  4. Pierre-Louis Curien, Marcelo P. Fiore, and Guillaume Munch-Maccagnoni. A theory of effects and resources: adjunction models and polarised calculi. In POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, 2016. Google Scholar
  5. V. Danos and T. Ehrhard. Probabilistic coherence spaces as a model of higher-order probabilistic computation. Inf. Comput., 209(6):966-991, 2011. URL: https://doi.org/10.1016/j.ic.2011.02.001.
  6. Jeff Egger, Rasmus Ejlers Møgelberg, and Alex K. Simpson. The enriched effect calculus: syntax and semantics. J. Log. Comput., 24:615-654, 2014. Google Scholar
  7. T. Ehrhard. On Köthe Sequence Spaces and Linear Logic. Mathematical Structures in Computer Science, 12(5):579-623, 2002. URL: https://doi.org/10.1017/S0960129502003729.
  8. T. Ehrhard. Finiteness spaces. Mathematical Structures in Computer Science, 2005. URL: https://doi.org/10.1017/S0960129504004645.
  9. T. Ehrhard and L. Regnier. The differential lambda-calculus. Theor. Comput. Sci., 2003. Google Scholar
  10. T. Ehrhard and L. Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theor. Comput. Sci., 403(2-3):347-372, 2008. Google Scholar
  11. Thomas Ehrhard. Collapsing non-idempotent intersection types. In CSL, volume 16 of LIPIcs, pages 259-273. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2012. Google Scholar
  12. Thomas Ehrhard. Call-By-Push-Value from a Linear Logic Point of View. In ESOP, volume 9632 of Lecture Notes in Computer Science, pages 202-228. Springer, 2016. Google Scholar
  13. Thomas Ehrhard and Giulio Guerrieri. The Bang Calculus: an untyped lambda-calculus generalizing call-by-name and call-by-value. In PPDP, pages 174-187. ACM, 2016. Google Scholar
  14. Thomas Ehrhard and Christine Tasson. Probabilistic call by push value. Logical Methods in Computer Science, 15(1), 2019. Google Scholar
  15. J-Y. Girard. Linear Logic. Theor. Comput. Sci., 50:1-102, 1987. Google Scholar
  16. Giulio Guerrieri and Giulio Manzonetto. The Bang Calculus and the Two Girard’s Translations. CoRR, abs/1904.06845, 2019. http://arxiv.org/abs/1904.06845, URL: https://doi.org/10.4204/EPTCS.292.2.
  17. E. Kerinec, G. Manzonetto, and M. Pagani. Revisiting Call-by-value Böhm trees in light of their Taylor expansion. CoRR, abs/1809.02659, 2018. URL: http://arxiv.org/abs/1809.02659.
  18. M. Kerjean and C. Tasson. Mackey-complete spaces and power series - a topological model of differential linear logic. Mathematical Structures in Computer Science, 28(4):472-507, 2018. URL: https://doi.org/10.1017/S0960129516000281.
  19. Ugo Dal Lago and Thomas Leventis. On the Taylor Expansion of Probabilistic λ-Terms. CoRR, abs/1904.09650, 2019. URL: http://arxiv.org/abs/1904.09650.
  20. Olivier Laurent and Laurent Regnier. About Translations of Classical Logic into Polarized Linear Logic. In 18th IEEE Symposium on Logic in Computer Science (LICS 2003), 22-25 June 2003, Ottawa, Canada, Proceedings, pages 11-20. IEEE Computer Society, 2003. URL: https://doi.org/10.1109/LICS.2003.1210040.
  21. P. B. Levy. Call-by-push-value: Decomposing call-by-value and call-by-name. Higher-Order and Symbolic Computation, 19(4):377-414, 2006. URL: https://doi.org/10.1007/s10990-006-0480-6.
  22. Michael Marz, Alexander Rohr, and Thomas Streicher. Full Abstraction and Universality via Realisability. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 174-182. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/LICS.1999.782612.
  23. Damiano Mazza. An Infinitary Affine Lambda-Calculus Isomorphic to the Full Lambda-Calculus. In LICS, pages 471-480. IEEE Computer Society, 2012. Google Scholar
  24. Damiano Mazza, Luc Pellissier, and Pierre Vial. Polyadic approximations, fibrations and intersection types. PACMPL, 2(POPL):6:1-6:28, 2018. Google Scholar
  25. P-A. Melliès. Categorical semantics of linear logic. In In: Interactive Models of Computation and Program Behaviour, Panoramas et Synthèses 27, Société Mathématique de France 1–196, 2009. Google Scholar
  26. M. Pagani, C. Tasson, and L. Vaux. Strong Normalizability as a Finiteness Structure via the Taylor Expansion of lambda-terms. In FOSSACS 2016, pages 408-423, 2016. Google Scholar
  27. L. Vaux. Taylor expansion, β-reduction and normalization. In 26th EACSL Annual Conference on Computer Science Logic, CSL 2017, Stockholm, Sweden, pages 39:1-39:16, 2017. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact