On Banach spaces of sequences and free linear logic exponential modality

TL;DR

This paper introduces a category of Banach sequence spaces called rigged sequences spaces that models full propositional linear logic, providing a realization of the free linear logic exponential modality.

Contribution

It presents a novel class of Banach spaces that models linear logic and realizes the free exponential modality, extending previous probabilistic coherence spaces models.

Findings

Rigged sequences spaces form a category modeling linear logic.

The model realizes the free linear logic exponential modality.

Morphisms are bounded linear maps continuous in a suitable topology.

Abstract

We introduce a category of vector spaces modelling full propositional linear logic, similar to probabilistic coherence spaces and to Koethe sequences spaces. Its objects are {\it rigged sequences spaces}, Banach spaces of sequences, with norms defined from pairing with finite sequences, and morphisms are bounded linear maps, continuous in a suitable topology. The main interest of the work is that our model gives a realization of the free linear logic exponentials construction.