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.

翻译：在线性逻辑的语义分析中，已涌现出两类指称模型：动态模型（通常以博弈语义形式呈现）与静态模型（通常基于关系范畴构建）。本文在动态模型与静态模型之间建立了一座形式化的桥梁：基于事件结构的细并发博弈与策略模型，以及基于分布器的广义结构物种模型。本文特别关注动态-静态关系的二维本质，我们通过双范畴和双函子对此进行形式化。在第一部分中，我们构建了一个从线性并发策略到分布器的对称幺半松弛函子。我们着重指出两个模型间的两个根本差异：组合机制与资源对称性的表示方式。在第二部分中，我们借鉴博弈语义中的成熟方法（可见策略、收益结构）以强化两个模型间的关联。我们获得了一个笛卡尔闭伪函子，并借此对λ演算理论中的最新成果提出了新的见解。