Constructing denotational models of linear can be a tedious work. Categorical semantics are useful to identify the fundamental structure of these models, and thus simplify and make more abstract the elaboration of those models.
TODO: why categories? how to
Constructing denotational models of linear can be a tedious work. Categorical semantics are useful to identify the fundamental structure of these models, and thus simplify and make more abstract the elaboration of those models.
TODO: why categories? how to extract categorical models? etc.
Basic category theory recalled
Definition (Natural transformation)
In order to interpret the various fragments of linear logic, we define incrementally what structure we need in a categorical setting.
- The most basic underlying structure are symmetric monoidal categories which model the symmetric tensor and its unit 1.
- The fragment (IMLL) is captured by so-called symmetric monoidal closed categories.
- Upgrading to ILL, that is, adding the exponential modality to IMLL requires modelling it categorically. There are various ways to do so: using rich enough adjunctions, or with an ad-hoc definition of a well-behaved comonad which leads to linear categories and close relatives.
- Dealing with the additives is quite easy, as they are plain cartesian product and coproduct, usually defined through universal properties in category theory.
- Retrieving, and is just a matter of dualizing, 1 and, thus requiring the model to be a *-autonomous category for that purpose.
A model of IMLL is a closed symmetric monoidal category. We recall the definition of these categories below.
Definition (Monoidal category)
Definition (Braided, symmetric monoidal category)
Definition (Closed monoidal category)
In a symmetric monoidal category, a left closed structure induces a right closed structure and conversely, allowing us to simply speak of a closed symmetric monoidal category.
Modeling the additives
A category has finite products when it has products and a terminal object.
Definition (Linear-non linear (LNL) adjunction)
This section is devoted to defining the concepts necessary to define these adjunctions.
Definition (Monoidal functor)
Definition (Monoidal natural transformation)
Definition (Monoidal adjunction)
Definition (*-autonomous category)
Compact closed categories
Definition (Dual objects)
Definition (Compact closed category)
Remark: The above isomorphism does not hold in *-autonomous categories in general. This means that models which are compact closed categories identify and as well as 1 and.