一句话:在基于事件结构的薄并发博弈与基于分配子的广义结构种之间建立双范畴桥接,并获得笛卡尔闭伪函子。
线性逻辑的指称语义产生了动态模型(以博弈语义为代表)与静态模型(以关系范畴/分配子为代表)两族。本文在二维层面为二者建立形式桥接:把基于事件结构的薄并发博弈与策略的双范畴,连到基于分配子的广义结构种双范畴。第一部分构造从薄并发博弈(线性双范畴)到分配子的 oplax 函子,从而将策略视为分配子,并揭示复合机制与资源对称表示两个根本差异。第二部分借用博弈语义中的可见策略与 payoff 结构等方法,收紧两模型联系,得到一个笛卡尔闭伪函子,并用它重新解释 λ-演算双范畴理论中的近期结果。
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 λ-calculus.