Categorical semantics
(→Modeling IMLL) |
(→Modeling negation) |
||
Line 79: | Line 79: | ||
Suppose that we are given a symmetric monoidal closed category <math>(\mathcal{C},\tens,I)</math> and an object <math>R</math> of <math>\mathcal{C}</math>. For every object <math>A</math>, we define a morphism |
Suppose that we are given a symmetric monoidal closed category <math>(\mathcal{C},\tens,I)</math> and an object <math>R</math> of <math>\mathcal{C}</math>. For every object <math>A</math>, we define a morphism |
||
:<math>\partial_{A}:A\to(A\limp R)\limp R</math> |
:<math>\partial_{A}:A\to(A\limp R)\limp R</math> |
||
− | as follows. By applying the bijection of the adjunction defining (left) closed monoidal categories to the identity morphism <math>\mathrm{id}_{A\limp R}:A\limp R \to A\limp R</math>, we get a morphism <math>A\tens (A\limp R)\to R</math>, and thus a morphism <math>(A\limp R)\tens A\to R</math> by precomposing with the symmetry <math>\gamma_{A\limp R,A}</math>. The morphism <math>\partial_A</math> is finally obtained by applying the bijection of the adjunction defining (left) closed monoidal categories to this morphism. |
+ | as follows. By applying the bijection of the adjunction defining (left) closed monoidal categories to the identity morphism <math>\mathrm{id}_{A\limp R}:A\limp R \to A\limp R</math>, we get a morphism <math>A\tens (A\limp R)\to R</math>, and thus a morphism <math>(A\limp R)\tens A\to R</math> by precomposing with the symmetry <math>\gamma_{A\limp R,A}</math>. The morphism <math>\partial_A</math> is finally obtained by applying the bijection of the adjunction defining (left) closed monoidal categories to this morphism. The object <math>R</math> is called ''dualizing'' when the morphism <math>\partial_A</math> is a bijection for every object <math>A</math> of <math>\mathcal{C}</math>. A symmetric monoidal closed category is ''*-autonomous'' when it admits such a dualizing object. |
}} |
}} |
||
Revision as of 19:17, 23 March 2009
Constructing denotational models of linear can be a tedious work. Categorical model 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.
Contents |
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 diagrams
commute.
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
- UNIQ752bc9c837bd3db7-math-00000011-QINU
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
- TODO
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)
Definition (Monoid)
Property
Categories with products vs monoidal categories.
Modeling IMALL
Modeling negation
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.
References
- ↑ MacLane, Saunders. Categories for the Working Mathematician.