From Thin Concurrent Games to Generalized Species of Structures (Extended Version)

TL;DR

This work builds a two-dimensional bridge between dynamic denotational models (thin concurrent games) and static models (generalized species of structures) for linear logic by embedding both within symmetric monoidal double categories and bicategories. It first constructs a symmetric monoidal oplax functor from linear concurrent strategies to distributors, clarifying how resource symmetries arise from groupoid actions and how two-dimensional morphisms capture dynamics. It then refines the connection using visibility and payoff to obtain a cartesian closed pseudofunctor Wis_oc → Esp, enabling lambda-calculus semantics via a reflexive object and a categorified graph model D^*. Overall, the results unify dynamic and static semantic frameworks and illuminate symmetry handling in resource-sensitive, bicategorical settings with implications for translating game-semantic insights to generalized species and vice versa.

Abstract

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.