A Linear Category of Polynomial Diagrams

TL;DR

This paper develops a categorical model for intuitionistic linear logic using polynomial diagrams and simulation diagrams, with a focus on structures in the category Set related to games and strategies.

Contribution

It introduces a new categorical framework for linear logic based on polynomial diagrams and explores its structures in different categories, especially Set.

Findings

Multiplicative structures are definable in any locally cartesian closed category.

Additive and exponential structures are specifically developed in Set.

Objects and morphisms have interpretations in terms of games, simulation, and strategies.

Abstract

We present a categorical model for intuitionistic linear logic where objects are polynomial diagrams and morphisms are simulation diagrams. The multiplicative structure (tensor product and its adjoint) can be defined in any locally cartesian closed category, whereas the additive (product and coproduct) and exponential Tensor-comonoid comonad) structures require additional properties and are only developed in the category Set, where the objects and morphisms have natural interpretations in terms of games, simulation and strategies.