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 two-dimensional dynamic and static models: we connect the bicategory of thin concurrent games and strategies, based on event structures, to the bicategory of generalized species of structures, based on distributors. In the first part of the paper, we construct an oplax functor from (the linear bicategory of) thin concurrent games to distributors. This explains how to view a strategy as a distributor, and highlights two fundamental differences: 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 bicategorical theory of the {\lambda}-calculus.
翻译:从线性逻辑的语义分析中涌现出两类指称语义模型:动态模型(通常表现为博弈语义)和静态模型(通常基于关系范畴)。本文为二维动态与静态模型之间搭建了一座形式化桥梁:我们将基于事件结构的薄并发博弈与策略的双范畴,与基于分配子的广义结构物种的双范畴联系起来。论文第一部分构建了一个从薄并发博弈(的线性双范畴)到分配子的弱逆变函子。这解释了如何将策略视为分配子,并凸显了两个根本性差异:复合机制与资源对称性的表示。论文第二部分调整了博弈语义中的既有方法(可见策略、收益结构),以强化两类模型之间的关联。我们由此获得了一个笛卡尔闭伪函子,并利用它为λ-演算双范畴理论的最新研究成果提供了新的阐释视角。