Interaction Systems and Linear Logic, a different games semantics

TL;DR

This paper introduces a novel game-based model for linear logic that does not rely on strategies, enabling new interpretations of interaction, tensor products, and differential calculus within a categorical framework.

Contribution

It presents a unique game semantics for linear logic that avoids strategies, constructs a model for differential calculus, and demonstrates its applicability to classical linear logic.

Findings

The model interprets formulas as games with a new morphism concept.

Tensor product corresponds to a strongly synchronous operation.

Constructs a reflexive object for the untyped differential -calculus.

Abstract

We define a model for linear logic based on two well-known ingredients: games and simulations. This model is interesting in the following respect: while it is obvious that the objects interpreting formulas are games and that everything is developed with the intuition of interaction in mind, the notion of morphism is very different from traditional morphisms in games semantics. In particular, we make no use of the notion of strategy! The resulting structure is very different from what is usually found in categories of games. We start by defining several constructions on those games and show, using elementary considerations, that they enjoy the appropriate algebraic properties making this category a denotational model for intuitionistic linear logic. An interesting point is that the tensor product corresponds to a strongly synchronous operation on games. This category can also, using traditional translations, serve as a model for the simply typed -calculus. We use some of the additional structure of the category to extend this to a model of the simply typed differential -calculus. Once this is done, we go a little further by constructing a reflexive object in this category, thus getting a concrete non-trivial model for the untyped differential -calculus. We then show, using a highly non-constructive principle, that this category is in fact a model for full classical linear logic ; and we finally have a brief look at the related notions of predicate transformers and containers.