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.
See for a more detailed introduction to category theory. See for a detailed treatment of categorical semantics of linear logic.
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)
A monoidal category is a category equipped with
- a functor called tensor product,
- an object I called unit object,
- three natural isomorphisms α, λ and ρ, called respectively associator, left unitor and right unitor, whose components are
- for every objects A,B,C,D in , the diagram
- for every objects A and B in , the diagram
Definition (Braided, symmetric monoidal category)
A braided monoidal category is a category together with a natural isomorphism of components
called braiding, such that the two diagrams
commute for every objects A, B and C.
A symmetric monoidal category is a braided monoidal category in which the braiding satisfies
for every objects A and B.
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.
A monoid (M,μ,η) in a monoidal category is an object M together with two morphisms
such that the diagrams
Categories with products vs monoidal categories.
Definition (Linear-non linear (LNL) adjunction)
A linear-non linear adjunction is a symmetric monoidal adjunction between lax monoidal functors
in which the category has finite products.
This section is devoted to defining the concepts necessary to define these adjunctions.
Definition (Monoidal functor)
Definition (Monoidal natural transformation)
Definition (Monoidal adjunction)
A monoidal adjunction between two monoidal functors
is an adjunction between the underlying functors F and G such that the unit and the counit
induce monoidal natural transformations between the corresponding monoidal functors.
Definition (*-autonomous category)
Compact closed categories
Definition (Dual objects)
A dual object structure in a monoidal category is a pair of objects A and B together with two morphisms
such that the diagrams
commute. The object A is called a left dual of B (and conversely B is a right dual of A).
Two left (resp. right) duals of a same object B are necessarily isomorphic.
Definition (Compact closed category)
A symmetric monoidal category is compact closed when every object A has a right dual A * . We write
for the corresponding duality morphisms.
In a compact closed category the left and right duals of an object A are isomorphic.
A compact closed category is monoidal closed, with closure defined by
A compact closed category is a (degenerated) *-autonomous category, with the obvious duality structure. In particular, .
Remark: The above isomorphism does not hold in *-autonomous categories in general.
The dualizing object R is simply I * .
For any A, the reverse isomorphism is constructed as follows:
Identity on A is taken as the canonical morphism required.
Other categorical models
Properties of categorical models
The Kleisli category
- ↑ MacLane, Saunders. Categories for the Working Mathematician. Volume 5, 1971.
- ↑ Melliès, Paul-André. Categorical Semantics of Linear Logic.
- ↑ Benton, Nick. A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.. CSL'94. journal. Volume 933, 1995.