Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Strategies as Resource Terms, and their Categorical Semantics

Lison Blondeau-Patissier, Pierre Clairambault, Lionel Vaux Auclair

TL;DR

This work unifies the η-long, simply-typed resource calculus with Hyland-Ong game semantics by introducing augmentations as canonical causal representations of plays and establishing a bijection with normal resource terms via isogmentations. It then elevates this correspondence to a denotational model of the resource calculus in which terms are interpreted as weighted sums of augmentations, hence invariant under reduction. Central to the development is the construction of a new categorical framework, called a resource category, in which strategies form a closed, additive, bialgebraic structure that faithfully models resource substitution and reduction. This yields a robust bridge between syntax, operational dynamics, and semantics, enabling a compositional interpretation that parallels the Taylor expansion and provides a foundation for quantitative analyses in resource-aware semantics.

Abstract

As shown by Tsukada and Ong, simply-typed, normal and eta-long resource terms correspond to plays in Hyland-Ong games, quotiented by Melliès' homotopy equivalence. The original proof of this inspiring result 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 lambda-calculus.

Strategies as Resource Terms, and their Categorical Semantics

TL;DR

This work unifies the η-long, simply-typed resource calculus with Hyland-Ong game semantics by introducing augmentations as canonical causal representations of plays and establishing a bijection with normal resource terms via isogmentations. It then elevates this correspondence to a denotational model of the resource calculus in which terms are interpreted as weighted sums of augmentations, hence invariant under reduction. Central to the development is the construction of a new categorical framework, called a resource category, in which strategies form a closed, additive, bialgebraic structure that faithfully models resource substitution and reduction. This yields a robust bridge between syntax, operational dynamics, and semantics, enabling a compositional interpretation that parallels the Taylor expansion and provides a foundation for quantitative analyses in resource-aware semantics.

Abstract

As shown by Tsukada and Ong, simply-typed, normal and eta-long resource terms correspond to plays in Hyland-Ong games, quotiented by Melliès' homotopy equivalence. The original proof of this inspiring result 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 lambda-calculus.
Paper Structure (57 sections, 36 theorems, 100 equations, 16 figures)

This paper contains 57 sections, 36 theorems, 100 equations, 16 figures.

Table of Contents

  1. Introduction
  2. Related and future work.
  3. Outline of the paper.
  4. Differences with the conference version.
  5. Preliminaries on tuples and bags
  6. The Simply-Typed $\eta$-Expanded Resource Calculus
  7. Resource calculus.
  8. Typing and $\eta$-long terms.
  9. Resource Terms as Augmentations
  10. Plays in game semantics.
  11. Plays and resource terms.
  12. Arenas, Configurations, Augmentations
  13. Arenas.
  14. Constructions.
  15. Configurations.
  16. ...and 42 more sections

Key Result

Theorem 3.1

The reduction $\leadsto$ on $\Sigma([)]{\Delta}$ is confluent and strongly normalizing.

Figures (16)

  • Figure 1: Syntax of the resource calculus: resource terms and resource bags
  • Figure 2: Inductive definition of substitution ($z$ is chosen fresh in the abstraction case)
  • Figure 3: Rules of resource reduction
  • Figure 4: Typing rules for the simply-typed $η$-long resource calculus
  • Figure 5: Two homotopic plays in HO games
  • ...and 11 more figures

Theorems & Definitions (75)

  • Theorem 3.1: ER08
  • Lemma 3.2
  • proof
  • Corollary 3.3
  • Lemma 3.4
  • proof
  • Lemma 3.5: Subject reduction
  • proof
  • Definition 4.1
  • Definition 4.2
  • ...and 65 more