一句话：通过 augmentation 直接建立正规资源项与 Hyland-Ong 策略的对应，并给出归约不变的指称模型与资源范畴。
本文重访 Tsukada 与 Ong 的结果：简单类型、正规且 eta-long 的资源项对应 Hyland-Ong 博弈中的 play（在同伦意义下）。原证明间接依赖关系模型的单射性，动态性仅通过关系模型与正规项复合体现。作者引入称为 augmentation 的因果结构作为同伦下 play 的规范代表，直接显式刻画与正规资源项的联系；进而将对应扩展到资源项归约，以 augmentation 加权和作为策略，构造归约下不变的资源演算指称模型；最后提出 resource category，类比 differential categories 之于 differential lambda-calculus。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{Blondeau-Patissier23,
title = {Strategies as Resource Terms, and their Categorical Semantics},
author = {Lison Blondeau-Patissier and Pierre Clairambault and Lionel Vaux Auclair},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 4},
year = {2025},
doi = {10.46298/lmcs-21(4:9)2025}
}