一句话：在薄并发博弈与广义结构种两类线性逻辑指称模型间建立形式桥梁，并用 double category 与 bicategory 刻画动态-静态对应。
线性逻辑的指称语义中出现了动态模型（典型为博弈语义）与静态模型（典型为关系范畴）两大家族。本文在基于事件结构的薄并发博弈与策略模型和基于分配子（distributors）的广义结构种模型之间建立形式桥梁。文章特别关注动态-静态关系的二维性质，并用 double category 和 bicategory 将其形式化。第一部分构造从线性并发策略到分配子的对称幺半 oplax 函子，并指出两个模型在复合机制和资源对称性表示上的根本差异。第二部分借鉴博弈语义中的可见策略与 payoff structure，加强两者联系，得到一个笛卡尔闭 pseudofunctor，并借此重新审视 λ-演算理论中的近期结果。
Two families of denotational models have emerged from the semantic analysis of linear logic: dynamic models, typically presented as game semantics, and static models, typically based on a category of relations. In this paper we introduce a formal bridge between a dynamic model and a static model: the model of thin concurrent games and strategies, based on event structures, and the model of generalized species of structures, based on distributors. A special focus of this paper is the two-dimensional nature of the dynamic-static relationship, which we formalize with double categories and bicategories. In the first part of the paper, we construct a symmetric monoidal oplax functor from linear concurrent strategies to distributors. We highlight two fundamental differences between the two models: the composition mechanism, and the representation of resource symmetries. In the second part of the paper, we adapt established methods from game semantics (visible strategies, payoff structure) to enforce a tighter connection between the two models. We obtain a cartesian closed pseudofunctor, which we exploit to shed new light on recent results in the theory of the lambda-calculus.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{ClairambaultOP25,
title = {From Thin Concurrent Games to Generalized Species of Structures (Extended Version)},
author = {Pierre Clairambault and Federico Olimpieri and Hugo Paquet},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 4},
year = {2025},
doi = {10.46298/lmcs-21(4:12)2025}
}