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

TL;DR

This paper establishes a formal connection between dynamic game semantics and static categorical models using double categories, providing new insights into the relationship between linear logic models and lambda-calculus.

Contribution

It introduces a formal bridge between thin concurrent games and generalized species of structures, formalized via double categories and bicategories, and adapts game semantics techniques to relate these models.

Findings

Constructed a symmetric monoidal oplax functor from strategies to distributors.

Identified key differences in composition and resource symmetries between models.

Developed a cartesian closed pseudofunctor linking the models to lambda-calculus.

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.