作为资源项的策略及其范畴语义

如Tsukada与Ong所示，简单类型、正规且eta-long的资源项对应于Hyland-Ong博弈中的play，模去Melliès的同伦等价。这一启发性结果的原始证明是间接的，依赖于关系模型对该对应双方的单射性——特别地，资源演算的动力学仅通过关系模型对由归一化定义的正规项复合的兼容性而被考虑。本文中，我们重访并推广这些结果。我们的首要贡献是通过考虑称为augmentation的因果结构来重述该对应，augmentation是Hyland-Ong play模同伦的规范代表。这使我们能给出与正规资源项联系的直接显式刻画。第二点贡献是将此刻画推广至资源项的归约：基于将策略定义为augmentation的加权和，我们给出了资源演算的语义模型，其在归约下不变。关键一步——也是第三点贡献——是我们称为资源范畴的范畴模型，它之于资源演算犹如微分范畴之于微分λ演算。