Categorical semantics
(introductory paragraph) |
(→Compact closed categories) |
||
(One intermediate revision by one user not shown) | |||
Line 305: | Line 305: | ||
</math> |
</math> |
||
It is easy to show that <math>\llcorner \ulcorner f\urcorner\lrcorner=f</math> and <math>\ulcorner\llcorner g\lrcorner\urcorner=g</math> from which we deduce the required bijection. |
It is easy to show that <math>\llcorner \ulcorner f\urcorner\lrcorner=f</math> and <math>\ulcorner\llcorner g\lrcorner\urcorner=g</math> from which we deduce the required bijection. |
||
+ | }} |
||
+ | |||
+ | {{Property| |
||
+ | A compact closed category is a (degenerated) *-autonomous category, with the obvious duality structure. In particular, <math>(A \otimes B)^* \cong A^*\otimes B^*</math>. |
||
+ | }} |
||
+ | |||
+ | {{Remark|The above isomorphism does not hold in *-autonomous categories in general. This means that models which are compact closed categories identify <math>\otimes</math> and <math>\parr</math> as well as <math>1</math> and <math>\bot</math>.}} |
||
+ | |||
+ | {{Proof| |
||
+ | The dualizing object <math>R</math> is simply <math>I^*</math>. |
||
+ | |||
+ | For any <math>A</math>, the reverse isomorphism <math>\delta_A : (A \multimap R)\multimap R \rightarrow A</math> is constructed as follows: |
||
+ | |||
+ | <math>\mathcal{C}((A \multimap R)\multimap R, A) := \mathcal{C}((A \otimes I^{**})\otimes I^{**}, A) \cong \mathcal{C}((A \otimes I)\otimes I, A) \cong \mathcal{C}(A, A)</math> |
||
+ | |||
+ | Identity on <math>A</math> is taken as the canonical morphism required. |
||
+ | |||
}} |
}} |
||
Latest revision as of 00:29, 4 October 2011
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 |
[edit] Basic category theory recalled
Definition (Category)
Definition (Functor)
Definition (Natural transformation)
Definition (Adjunction)
Definition (Monad)
[edit] 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.
[edit] 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.
[edit] 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.
[edit] 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.
[edit] Modeling negation
[edit] *-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.
[edit] 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.