License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2023.13
URN: urn:nbn:de:0030-drops-179976
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/17997/
Go to the corresponding LIPIcs Volume Portal

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

Strategies as Resource Terms, and Their Categorical Semantics

pdf-format:
LIPIcs-FSCD-2023-13.pdf (1.0 MB)

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.

BibTeX - Entry

@InProceedings{blondeaupatissier_et_al:LIPIcs.FSCD.2023.13,
  author =	{Blondeau-Patissier, Lison and Clairambault, Pierre and Vaux Auclair, Lionel},
  title =	{{Strategies as Resource Terms, and Their Categorical Semantics}},
  booktitle =	{8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
  pages =	{13:1--13:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-277-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{260},
  editor =	{Gaboardi, Marco and van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/17997},
  URN =		{urn:nbn:de:0030-drops-179976},
  doi =		{10.4230/LIPIcs.FSCD.2023.13},
  annote =	{Keywords: Resource calculus, Game semantics, Categorical semantics}
}

Keywords: Resource calculus, Game semantics, Categorical semantics
Collection: 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)
Issue Date: 2023
Date of publication: 28.06.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI