Categorical semantics
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 [1]for a more detailed introduction to category theory. See [2]for a detailed treatment of categorical semantics of linear logic.
Contents |
Basic category theory recalled
Definition (Category)
Definition (Functor)
Definition (Natural transformation)
Definition (Adjunction)
Definition (Monad)
Overview
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.
Modeling IMLL
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
such that
- for every objects A,B,C,D in
, the diagram
commutes,
- for every objects A and B in
, the diagram
commutes.
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
and
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)
A monoidal category is left closed when for every object A, the functor
has a right adjoint, written
This means that there exists a bijection
which is natural in B and C. Equivalently, a monoidal category is left closed when it is equipped with a left closed structure, which consists of
- an object
,
- a morphism
, called left evaluation,
for every objects A and B, such that for every morphism there exists a unique morphism
making the diagram
commute.
Dually, the monoidal category is right closed when the functor
admits a right adjoint. The notion of right closed structure can be defined similarly.
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
Definition (Product)
A product (X,π1,π2) of two coinitial morphisms and
in a category
is an object X of
together with two morphisms
and
such that there exists a unique morphism
making the diagram
commute.
A category has finite products when it has products and a terminal object.
Definition (Monoid)
A monoid (M,μ,η) in a monoidal category is an object M together with two morphisms
and
such that the diagrams
and
commute.
Property
Categories with products vs monoidal categories.
Modeling ILL
Introduced in[3].
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)
A lax monoidal functor (F,f) between two monoidal categories and
consists of
- a functor
between the underlying categories,
- a natural transformation f of components
,
- a morphism
such that the diagrams
and
and
commute for every objects A, B and C of . The morphisms fA,B and f are called coherence maps.
A lax monoidal functor is strong when the coherence maps are invertible and strict when they are identities.
Definition (Monoidal natural transformation)
Suppose that and
are two monoidal categories and
and
are two monoidal functors between these categories. A monoidal natural transformation between these monoidal functors is a natural transformation
between the underlying functors such that the diagrams
and
commute for every objects A and B of .
Definition (Monoidal adjunction)
A monoidal adjunction between two monoidal functors
and
is an adjunction between the underlying functors F and G such that the unit and the counit
and
induce monoidal natural transformations between the corresponding monoidal functors.
Modeling negation
*-autonomous categories
Definition (*-autonomous category)
Suppose that we are given a symmetric monoidal closed category and an object R of
. For every object A, we define a morphism
as follows. By applying the bijection of the adjunction defining (left) closed monoidal categories to the identity morphism , we get a morphism
, and thus a morphism
by precomposing with the symmetry
. The morphism
is finally obtained by applying the bijection of the adjunction defining (left) closed monoidal categories to this morphism. The object R is called dualizing when the morphism
is a bijection for every object A of
. A symmetric monoidal closed category is *-autonomous when it admits such a dualizing object.
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
and
such that the diagrams
and
commute. The object A is called a left dual of B (and conversely B is a right dual of A).
Lemma
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
and
for the corresponding duality morphisms.
Lemma
In a compact closed category the left and right duals of an object A are isomorphic.
Property
A compact closed category is monoidal closed, with closure defined by
Proof.
To every morphism , we associate a morphism
defined as
and to every morphism , we associate a morphism
defined as
It is easy to show that and
from which we deduce the required bijection.
Property
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. This means that models which are compact closed categories identify and
as well as 1 and
.
Proof. 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.