从薄并发博弈到结构的广义物种（扩展版）
From Thin Concurrent Games to Generalized Species of Structures (Extended Version)
AI总结：
本文在线性逻辑的薄并发博弈动态模型与结构广义物种静态模型间构建形式化桥梁，通过双范畴刻画二维关系，构造对称幺半函子并调整博弈语义方法得到笛卡尔闭伪函子，为λ演算研究提供新视角。
摘要：
线性逻辑的语义分析中涌现出两类指称模型：动态模型（通常以博弈语义形式呈现）和静态模型（通常基于关系范畴）。本文在动态模型与静态模型之间搭建了一座形式化桥梁：基于事件结构的薄并发博弈与策略模型，以及基于分配子的结构广义物种模型。本文重点关注动静态关系的二维特性，并通过双范畴和二范畴对其进行形式化。\n在论文第一部分，我们构建了从线性并发策略到分配子的对称幺半 oplax 函子。我们指出了两类模型之间的两个根本差异：复合机制，以及资源对称性的表示方式。在论文第二部分，我们调整了博弈语义中已有的方法（可见策略、收益结构），以强化两类模型之间的联系。我们得到了一个笛卡尔闭伪函子，并利用它为λ演算理论的最新研究成果提供了新的阐释视角。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
