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.
翻译:从线性逻辑的语义分析中产生了两个分解模型的两组。 动态模型,通常以游戏语义和静态模型的形式出现, 通常以某种关系类别为基础。 在本文中, 我们引入了两维动态模型和静态模型之间的正式桥梁: 我们根据事件结构, 将薄色同时游戏和战略的双类与基于经销商的通用结构的双类连接起来。 在文件的第一部分, 我们从( 线性双类) 薄相伴游戏到经销商, 构建了一种简单易懂的喜乐器。 这解释了如何将战略看成一个分销商, 并突出了两个基本差异: 构成机制和资源配对的表述。 在论文的第二部分, 我们从游戏语义结构( 可见的策略、 报酬结构) 中建立了方法, 以强化两种模式之间的联系。 我们得到了一个cartesian 封闭的伪体, 我们利用它来展示最近的结果。