Document Open Access Logo

Strategies as Resource Terms, and Their Categorical Semantics

Authors Lison Blondeau-Patissier, Pierre Clairambault , Lionel Vaux Auclair

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2023.13.pdf
  • Filesize: 0.96 MB
  • 22 pages

Document Identifiers

Author Details

Lison Blondeau-Patissier
  • Aix Marseille Univ, CNRS, I2M and LIS, Marseille, France
Pierre Clairambault
  • Aix Marseille Univ, CNRS, LIS, Marseille, France
Lionel Vaux Auclair
  • Aix Marseille Univ, CNRS, I2M, Marseille, France

Funding

  • Clairambault, Pierre: Supported by the ANR projects DyVerSe (ANR-19-CE48-0010-01) and by the Labex MiLyon (ANR-10-LABX-0070) of Université de Lyon.
  • Vaux Auclair, Lionel: Supported by the ANR projects PPS (ANR-19-CE48-0014), LambdaComb (ANR-21-CE48-0017) and Reciprog (ANR-21-CE48-0019).

Cite AsGet BibTex

Lison Blondeau-Patissier, Pierre Clairambault, and Lionel Vaux Auclair. Strategies as Resource Terms, and Their Categorical Semantics. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 13:1-13:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.FSCD.2023.13

Abstract

As shown by Tsukada and Ong, simply-typed, normal and η-long resource terms correspond to plays in Hyland-Ong games, quotiented by Melliès' homotopy equivalence. Though inspiring, their proof is indirect, relying on the injectivity of the relational model {w.r.t.} both sides of the correspondence - in particular, the dynamics of the resource calculus is taken into account only via the compatibility of the relational model with the composition of normal terms defined by normalization. In the present paper, we revisit and extend these results. Our first contribution is to restate the correspondence by considering causal structures we call augmentations, which are canonical representatives of Hyland-Ong plays up to homotopy. This allows us to give a direct and explicit account of the connection with normal resource terms. As a second contribution, we extend this account to the reduction of resource terms: building on a notion of strategies as weighted sums of augmentations, we provide a denotational model of the resource calculus, invariant under reduction. A key step - and our third contribution - is a categorical model we call a resource category, which is to the resource calculus what differential categories are to the differential λ-calculus.

Subject Classification

ACM Subject Classification
  • Theory of computation → Denotational semantics
  • Theory of computation → Categorical semantics
Keywords
  • Resource calculus
  • Game semantics
  • Categorical semantics

Metrics

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

Related Versions

References

  1. Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. Full abstraction for PCF. CoRR, abs/1311.6125, 2013. Google Scholar
  2. Davide Barbarossa and Giulio Manzonetto. Taylor subsumes Scott, Berry, Kahn and Plotkin. Proc. ACM Program. Lang., 4(POPL):1:1-1:23, 2020. Google Scholar
  3. Hendrik Pieter Barendregt. The lambda calculus - its syntax and semantics, volume 103 of Studies in logic and the foundations of mathematics. North-Holland, 1985. Google Scholar
  4. Lison Blondeau-Patissier and Pierre Clairambault. Positional injectivity for innocent strategies. In Naoki Kobayashi, editor, 6th International Conference on Formal Structures for Computation and Deduction, FSCD 2021, July 17-24, 2021, Buenos Aires, Argentina (Virtual Conference), volume 195 of LIPIcs, pages 17:1-17:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.FSCD.2021.17.
  5. Richard Blute, J. Robin B. Cockett, Jean-Simon Pacaud Lemay, and Robert A. G. Seely. Differential categories revisited. Appl. Categorical Struct., 28(2):171-235, 2020. URL: https://doi.org/10.1007/s10485-019-09572-y.
  6. Richard F Blute, J Robin B Cockett, and Robert AG Seely. Cartesian differential categories. Theory and Applications of Categories, 22(23):622-672, 2009. Google Scholar
  7. Pierre Boudes. Thick subtrees, games and experiments. In TLCA, volume 5608 of Lecture Notes in Computer Science, pages 65-79. Springer, 2009. Google Scholar
  8. Antonio Bucciarelli, Alberto Carraro, Thomas Ehrhard, and Giulio Manzonetto. Full abstraction for the resource lambda calculus with tests, through Taylor expansion. Log. Methods Comput. Sci., 8(4), 2012. URL: https://doi.org/10.2168/LMCS-8(4:3)2012.
  9. Antonio Bucciarelli, Thomas Ehrhard, and Giulio Manzonetto. Categorical models for simply typed resource calculi. In MFPS, volume 265 of Electronic Notes in Theoretical Computer Science, pages 213-230. Elsevier, 2010. Google Scholar
  10. Simon Castellan and Pierre Clairambault. Disentangling parallelism and interference in game semantics. CoRR, abs/2103.15453, 2021. Google Scholar
  11. Simon Castellan, Pierre Clairambault, Silvain Rideau, and Glynn Winskel. Games and strategies as event structures. Log. Methods Comput. Sci., 13(3), 2017. URL: https://doi.org/10.23638/LMCS-13(3:35)2017.
  12. Simon Castellan, Pierre Clairambault, and Glynn Winskel. Thin games with symmetry and concurrent Hyland-Ong games. Log. Methods Comput. Sci., 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:18)2019.
  13. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theor. Comput. Sci., 309(1-3):1-41, 2003. Google Scholar
  14. Thomas Ehrhard and Laurent Regnier. Differential interaction nets. Theor. Comput. Sci., 364(2):166-195, 2006. Google Scholar
  15. Thomas Ehrhard and Laurent Regnier. Uniformity and the Taylor expansion of ordinary lambda-terms. Theor. Comput. Sci., 403(2-3):347-372, 2008. URL: https://doi.org/10.1016/j.tcs.2008.06.001.
  16. J. M. E. Hyland and C.-H. Luke Ong. On full abstraction for PCF: I, II, and III. Inf. Comput., 163(2):285-408, 2000. URL: https://doi.org/10.1006/inco.2000.2917.
  17. Jim Laird. A game semantics of the asynchronous π-calculus. In CONCUR, volume 3653 of Lecture Notes in Computer Science, pages 51-65. Springer, 2005. Google Scholar
  18. Giulio Manzonetto. What is a categorical model of the differential and the resource λ-calculi? Math. Struct. Comput. Sci., 22(3):451-520, 2012. Google Scholar
  19. Paul-André Melliès. Asynchronous games 2: The true concurrency of innocence. Theor. Comput. Sci., 358(2-3):200-228, 2006. URL: https://doi.org/10.1016/j.tcs.2006.01.016.
  20. Paul-André Mellies. Categorical semantics of linear logic. Panoramas et syntheses, 27:15-215, 2009. Google Scholar
  21. Reiji Nakajima. Infinite normal forms for the λ-calculus. In Corrado Böhm, editor, Lambda-Calculus and Computer Science Theory, Proceedings of the Symposium Held in Rome, Italy, March 25-27, 1975, volume 37 of Lecture Notes in Computer Science, pages 62-82. Springer, 1975. URL: https://doi.org/10.1007/BFb0029519.
  22. Ken Sakayori and Takeshi Tsukada. A truly concurrent game model of the asynchronous π-calculus. In Javier Esparza and Andrzej S. Murawski, editors, Foundations of Software Science and Computation Structures - 20th International Conference, FOSSACS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, volume 10203 of Lecture Notes in Computer Science, pages 389-406, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_23.
  23. Takeshi Tsukada and C.-H. Luke Ong. Plays as resource terms via non-idempotent intersection types. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, New York, NY, USA, July 5-8, 2016, pages 237-246. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934553.
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