LLWiki - User contributions [en]

Categorical semantics

2009-03-25T15:24:23Z

Samuel Mimram: /* Modeling ILL */

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 <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> 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|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
\xymatrix{
&(M\tens M)\tens M\ar[dl]_{\alpha_{M,M,M}}\ar[r]^-{\mu\tens M}&M\tens M\ar[dd]^{\mu}\\
M\tens(M\tens M)\ar[d]_{M\tens\mu}&&\\
M\tens M\ar[rr]_{\mu}&&M\\
}
</math>
and
:<math>
\xymatrix{
I\tens M\ar[r]^{\eta\tens M}\ar[dr]_{\lambda_M}&M\tens M\ar[d]_\mu&\ar[l]_{M\tens\eta}\ar[dl]^{\rho_M}M\tens I\\
&M&
}
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
\xymatrix{
(\mathcal{M},\times,\top)\ar@/^/[rr]^{(L,l)}&\bot&\ar@/^/[ll]^{(M,m)}(\mathcal{L},\otimes,I)
}
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>
\xymatrix{
(FA\bullet FB)\bullet FC\ar[d]_{\phi_{A,B}\bullet FC}\ar[r]^{\alpha_{FA,FB,FC}}&FA\bullet(FB\bullet FC)\ar[dr]^{FA\bullet\phi_{B,C}}\\
F(A\otimes B)\bullet FC\ar[dr]_{\phi_{A\otimes B,C}}&&FA\bullet F(B\otimes C)\ar[d]^{\phi_{A,B\otimes C}}\\
&F((A\otimes B)\otimes C)\ar[r]_{F\alpha_{A,B,C}}&F(A\otimes(B\otimes C))
}
</math>
and
:<math>
\xymatrix{
FA\bullet J\ar[d]_{\rho_{FA}}\ar[r]^{FA\bullet\phi}&FA\bullet FI\ar[d]^{\phi_{A,I}}\\
FA&\ar[l]^{F\rho_A}F(A\otimes I)
}
</math> and <math>
\xymatrix{
J\bullet FB\ar[d]_{\lambda_{FB}}\ar[r]^{\phi\bullet FB}&FI\bullet FB\ar[d]^{\phi_{I,B}}\\
FB&\ar[l]^{F\lambda_B}F(I\otimes B)
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>
\xymatrix{
FA\bullet FB\ar[d]_{f_{A,B}}\ar[r]^{\theta_A\bullet\theta_B}&\ar[d]^{g_{A,B}}GA\bullet GB\\
F(A\tens B)\ar[r]_{\theta_{A\tens B}}&G(A\tens B)
}
</math> and <math>
\xymatrix{
&\ar[dl]_{f}J\ar[dr]^{g}&\\
FI\ar[rr]_{\theta_I}&&GI
}
</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
A ''monoidal adjunction'' between two monoidal functors
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{D},\bullet,J)\Rightarrow(\mathcal{C},\tens,I)
</math>
is an adjunction between the underlying functors <math>F</math> and <math>G</math> such that the unit and the counit
:<math>\eta:\mathcal{C}\Rightarrow G\circ F</math> and <math>\varepsilon:F\circ G\Rightarrow\mathcal{D}</math>
induce monoidal natural transformations between the corresponding monoidal functors.
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
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>
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.
}}

=== Compact closed categories ===

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
\xymatrix{
&A\tens(B\tens A)\ar[r]^{\alpha_{A,B,A}^{-1}}&(A\tens B)\tens A\ar[dr]^{\varepsilon\tens A}\\
A\tens I\ar[ur]^{A\tens\eta}&&&I\tens A\ar[d]^{\lambda_A}\\
A\ar[u]^{\rho_A^{-1}}\ar@{=}[rrr]&&&A\\
}
</math>
and
:<math>
\xymatrix{
&(B\tens A)\tens B\ar[r]^{\alpha_{B,A,B}}&B\tens(A\tens B)\ar[dr]^{B\tens\varepsilon}\\
I\tens B\ar[ur]^{\eta\tens B}&&&B\tens I\ar[d]^{\rho_B}\\
B\ar[u]^{\lambda_B^{-1}}\ar@{=}[rrr]&&&B\\
}
</math>
commute. The object <math>A</math> is called a left dual of <math>B</math> (and conversely <math>B</math> is a right dual of <math>A</math>).
}}

{{Lemma|
Two left (resp. right) duals of a same object <math>B</math> are necessarily isomorphic.
}}

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a right dual <math>A^*</math>. We write
:<math>\eta_A:I\to A^*\tens A</math> and <math>\varepsilon_A:A\tens A^*\to I</math>
for the corresponding duality morphisms.
}}

{{Lemma|
In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.
}}

{{Property|
A compact closed category <math>\mathcal{C}</math> is monoidal closed, with closure defined by
:<math>\mathcal{C}(A\tens B,C)\cong\mathcal{C}(B,A^*\tens C)</math>
}}
{{Proof|
To every morphism <math>f:A\tens B\to C</math>, we associate a morphism <math>\ulcorner f\urcorner:B\to A^*\tens C</math> defined as
:<math>
\xymatrix{
B\ar[r]^-{\lambda_B^{-1}}&I\tens B\ar[r]^-{\eta_A\tens B}&(A^*\tens A)\tens B\ar[r]^-{\alpha_{A^*,A,B}}&A^*\tens(A\tens B)\ar[r]^-{A^*\tens f}&A\tens C\\
}
</math>
and to every morphism <math>g:B\to A^*\tens C</math>, we associate a morphism <math>\llcorner g\lrcorner:A\tens B\to C</math> defined as
:<math>
\xymatrix{
A\tens B\ar[r]^-{A\tens g}&A\tens(A^*\tens C)\ar[r]^-{\alpha_{A,A^*,C}^{-1}}&(A\tens A^*)\tens C\ar[r]^-{\varepsilon_A\tens C}&I\tens C\ar[r]^-{\lambda_C}&C
}
</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.
}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2009-03-25T15:12:55Z

Samuel Mimram: /* Compact closed categories */

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 <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> 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|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
\xymatrix{
&(M\tens M)\tens M\ar[dl]_{\alpha_{M,M,M}}\ar[r]^-{\mu\tens M}&M\tens M\ar[dd]^{\mu}\\
M\tens(M\tens M)\ar[d]_{M\tens\mu}&&\\
M\tens M\ar[rr]_{\mu}&&M\\
}
</math>
and
:<math>
\xymatrix{
I\tens M\ar[r]^{\eta\tens M}\ar[dr]_{\lambda_M}&M\tens M\ar[d]_\mu&\ar[l]_{M\tens\eta}\ar[dl]^{\rho_M}M\tens I\\
&M&
}
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
\xymatrix{
(\mathcal{M},\times,\top)\ar[rr]^{(L,l)}&\bot&\ar[ll]^{(M,m)}(\mathcal{L},\otimes,I)
}
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>
\xymatrix{
(FA\bullet FB)\bullet FC\ar[d]_{\phi_{A,B}\bullet FC}\ar[r]^{\alpha_{FA,FB,FC}}&FA\bullet(FB\bullet FC)\ar[dr]^{FA\bullet\phi_{B,C}}\\
F(A\otimes B)\bullet FC\ar[dr]_{\phi_{A\otimes B,C}}&&FA\bullet F(B\otimes C)\ar[d]^{\phi_{A,B\otimes C}}\\
&F((A\otimes B)\otimes C)\ar[r]_{F\alpha_{A,B,C}}&F(A\otimes(B\otimes C))
}
</math>
and
:<math>
\xymatrix{
FA\bullet J\ar[d]_{\rho_{FA}}\ar[r]^{FA\bullet\phi}&FA\bullet FI\ar[d]^{\phi_{A,I}}\\
FA&\ar[l]^{F\rho_A}F(A\otimes I)
}
</math> and <math>
\xymatrix{
J\bullet FB\ar[d]_{\lambda_{FB}}\ar[r]^{\phi\bullet FB}&FI\bullet FB\ar[d]^{\phi_{I,B}}\\
FB&\ar[l]^{F\lambda_B}F(I\otimes B)
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>
\xymatrix{
FA\bullet FB\ar[d]_{f_{A,B}}\ar[r]^{\theta_A\bullet\theta_B}&\ar[d]^{g_{A,B}}GA\bullet GB\\
F(A\tens B)\ar[r]_{\theta_{A\tens B}}&G(A\tens B)
}
</math> and <math>
\xymatrix{
&\ar[dl]_{f}J\ar[dr]^{g}&\\
FI\ar[rr]_{\theta_I}&&GI
}
</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
A ''monoidal adjunction'' between two monoidal functors
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{D},\bullet,J)\Rightarrow(\mathcal{C},\tens,I)
</math>
is an adjunction between the underlying functors <math>F</math> and <math>G</math> such that the unit and the counit
:<math>\eta:\mathcal{C}\Rightarrow G\circ F</math> and <math>\varepsilon:F\circ G\Rightarrow\mathcal{D}</math>
induce monoidal natural transformations between the corresponding monoidal functors.
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
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>
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.
}}

=== Compact closed categories ===

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
\xymatrix{
&A\tens(B\tens A)\ar[r]^{\alpha_{A,B,A}^{-1}}&(A\tens B)\tens A\ar[dr]^{\varepsilon\tens A}\\
A\tens I\ar[ur]^{A\tens\eta}&&&I\tens A\ar[d]^{\lambda_A}\\
A\ar[u]^{\rho_A^{-1}}\ar@{=}[rrr]&&&A\\
}
</math>
and
:<math>
\xymatrix{
&(B\tens A)\tens B\ar[r]^{\alpha_{B,A,B}}&B\tens(A\tens B)\ar[dr]^{B\tens\varepsilon}\\
I\tens B\ar[ur]^{\eta\tens B}&&&B\tens I\ar[d]^{\rho_B}\\
B\ar[u]^{\lambda_B^{-1}}\ar@{=}[rrr]&&&B\\
}
</math>
commute. The object <math>A</math> is called a left dual of <math>B</math> (and conversely <math>B</math> is a right dual of <math>A</math>).
}}

{{Lemma|
Two left (resp. right) duals of a same object <math>B</math> are necessarily isomorphic.
}}

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a right dual <math>A^*</math>. We write
:<math>\eta_A:I\to A^*\tens A</math> and <math>\varepsilon_A:A\tens A^*\to I</math>
for the corresponding duality morphisms.
}}

{{Lemma|
In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.
}}

{{Property|
A compact closed category <math>\mathcal{C}</math> is monoidal closed, with closure defined by
:<math>\mathcal{C}(A\tens B,C)\cong\mathcal{C}(B,A^*\tens C)</math>
}}
{{Proof|
To every morphism <math>f:A\tens B\to C</math>, we associate a morphism <math>\ulcorner f\urcorner:B\to A^*\tens C</math> defined as
:<math>
\xymatrix{
B\ar[r]^-{\lambda_B^{-1}}&I\tens B\ar[r]^-{\eta_A\tens B}&(A^*\tens A)\tens B\ar[r]^-{\alpha_{A^*,A,B}}&A^*\tens(A\tens B)\ar[r]^-{A^*\tens f}&A\tens C\\
}
</math>
and to every morphism <math>g:B\to A^*\tens C</math>, we associate a morphism <math>\llcorner g\lrcorner:A\tens B\to C</math> defined as
:<math>
\xymatrix{
A\tens B\ar[r]^-{A\tens g}&A\tens(A^*\tens C)\ar[r]^-{\alpha_{A,A^*,C}^{-1}}&(A\tens A^*)\tens C\ar[r]^-{\varepsilon_A\tens C}&I\tens C\ar[r]^-{\lambda_C}&C
}
</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.
}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2009-03-25T14:52:59Z

Samuel Mimram: /* Compact closed categories */

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 <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> 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|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
\xymatrix{
&(M\tens M)\tens M\ar[dl]_{\alpha_{M,M,M}}\ar[r]^-{\mu\tens M}&M\tens M\ar[dd]^{\mu}\\
M\tens(M\tens M)\ar[d]_{M\tens\mu}&&\\
M\tens M\ar[rr]_{\mu}&&M\\
}
</math>
and
:<math>
\xymatrix{
I\tens M\ar[r]^{\eta\tens M}\ar[dr]_{\lambda_M}&M\tens M\ar[d]_\mu&\ar[l]_{M\tens\eta}\ar[dl]^{\rho_M}M\tens I\\
&M&
}
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
\xymatrix{
(\mathcal{M},\times,\top)\ar[rr]^{(L,l)}&\bot&\ar[ll]^{(M,m)}(\mathcal{L},\otimes,I)
}
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>
\xymatrix{
(FA\bullet FB)\bullet FC\ar[d]_{\phi_{A,B}\bullet FC}\ar[r]^{\alpha_{FA,FB,FC}}&FA\bullet(FB\bullet FC)\ar[dr]^{FA\bullet\phi_{B,C}}\\
F(A\otimes B)\bullet FC\ar[dr]_{\phi_{A\otimes B,C}}&&FA\bullet F(B\otimes C)\ar[d]^{\phi_{A,B\otimes C}}\\
&F((A\otimes B)\otimes C)\ar[r]_{F\alpha_{A,B,C}}&F(A\otimes(B\otimes C))
}
</math>
and
:<math>
\xymatrix{
FA\bullet J\ar[d]_{\rho_{FA}}\ar[r]^{FA\bullet\phi}&FA\bullet FI\ar[d]^{\phi_{A,I}}\\
FA&\ar[l]^{F\rho_A}F(A\otimes I)
}
</math> and <math>
\xymatrix{
J\bullet FB\ar[d]_{\lambda_{FB}}\ar[r]^{\phi\bullet FB}&FI\bullet FB\ar[d]^{\phi_{I,B}}\\
FB&\ar[l]^{F\lambda_B}F(I\otimes B)
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>
\xymatrix{
FA\bullet FB\ar[d]_{f_{A,B}}\ar[r]^{\theta_A\bullet\theta_B}&\ar[d]^{g_{A,B}}GA\bullet GB\\
F(A\tens B)\ar[r]_{\theta_{A\tens B}}&G(A\tens B)
}
</math> and <math>
\xymatrix{
&\ar[dl]_{f}J\ar[dr]^{g}&\\
FI\ar[rr]_{\theta_I}&&GI
}
</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
A ''monoidal adjunction'' between two monoidal functors
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{D},\bullet,J)\Rightarrow(\mathcal{C},\tens,I)
</math>
is an adjunction between the underlying functors <math>F</math> and <math>G</math> such that the unit and the counit
:<math>\eta:\mathcal{C}\Rightarrow G\circ F</math> and <math>\varepsilon:F\circ G\Rightarrow\mathcal{D}</math>
induce monoidal natural transformations between the corresponding monoidal functors.
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
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>
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.
}}

=== Compact closed categories ===

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
\xymatrix{
&A\tens(B\tens A)\ar[r]^{\alpha_{A,B,A}^{-1}}&(A\tens B)\tens A\ar[dr]^{\varepsilon\tens A}\\
A\tens I\ar[ur]^{A\tens\eta}&&&I\tens A\ar[d]^{\lambda_A}\\
A\ar[u]^{\rho_A^{-1}}\ar@{=}[rrr]&&&A\\
}
</math>
and
:<math>
\xymatrix{
&(B\tens A)\tens B\ar[r]^{\alpha_{B,A,B}}&B\tens(A\tens B)\ar[dr]^{B\tens\varepsilon}\\
I\tens B\ar[ur]^{\eta\tens B}&&&B\tens I\ar[d]^{\rho_B}\\
B\ar[u]^{\lambda_B^{-1}}\ar@{=}[rrr]&&&B\\
}
</math>
commute. The object <math>A</math> is called a left dual of <math>B</math> (and conversely <math>B</math> is a right dual of <math>A</math>).
}}

{{Lemma|
Two left (resp. right) duals of a same object <math>B</math> are necessarily isomorphic.
}}

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a right dual <math>A^*</math>. We write
:<math>\eta_A:I\to A^*\tens A</math> and <math>\varepsilon:A\tens A^*\to I</math>
for the corresponding duality morphisms.
}}

{{Lemma|
In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.
}}

{{Property|
A compact closed category <math>\mathcal{C}</math> is monoidal closed, with closure defined by
:<math>\mathcal{C}(A\tens B,C)\cong\mathcal{C}(B,A^*\tens C)</math>
}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2009-03-25T14:48:35Z

Samuel Mimram: /* Compact closed categories */

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 <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> 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|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
\xymatrix{
&(M\tens M)\tens M\ar[dl]_{\alpha_{M,M,M}}\ar[r]^-{\mu\tens M}&M\tens M\ar[dd]^{\mu}\\
M\tens(M\tens M)\ar[d]_{M\tens\mu}&&\\
M\tens M\ar[rr]_{\mu}&&M\\
}
</math>
and
:<math>
\xymatrix{
I\tens M\ar[r]^{\eta\tens M}\ar[dr]_{\lambda_M}&M\tens M\ar[d]_\mu&\ar[l]_{M\tens\eta}\ar[dl]^{\rho_M}M\tens I\\
&M&
}
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
\xymatrix{
(\mathcal{M},\times,\top)\ar[rr]^{(L,l)}&\bot&\ar[ll]^{(M,m)}(\mathcal{L},\otimes,I)
}
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>
\xymatrix{
(FA\bullet FB)\bullet FC\ar[d]_{\phi_{A,B}\bullet FC}\ar[r]^{\alpha_{FA,FB,FC}}&FA\bullet(FB\bullet FC)\ar[dr]^{FA\bullet\phi_{B,C}}\\
F(A\otimes B)\bullet FC\ar[dr]_{\phi_{A\otimes B,C}}&&FA\bullet F(B\otimes C)\ar[d]^{\phi_{A,B\otimes C}}\\
&F((A\otimes B)\otimes C)\ar[r]_{F\alpha_{A,B,C}}&F(A\otimes(B\otimes C))
}
</math>
and
:<math>
\xymatrix{
FA\bullet J\ar[d]_{\rho_{FA}}\ar[r]^{FA\bullet\phi}&FA\bullet FI\ar[d]^{\phi_{A,I}}\\
FA&\ar[l]^{F\rho_A}F(A\otimes I)
}
</math> and <math>
\xymatrix{
J\bullet FB\ar[d]_{\lambda_{FB}}\ar[r]^{\phi\bullet FB}&FI\bullet FB\ar[d]^{\phi_{I,B}}\\
FB&\ar[l]^{F\lambda_B}F(I\otimes B)
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>
\xymatrix{
FA\bullet FB\ar[d]_{f_{A,B}}\ar[r]^{\theta_A\bullet\theta_B}&\ar[d]^{g_{A,B}}GA\bullet GB\\
F(A\tens B)\ar[r]_{\theta_{A\tens B}}&G(A\tens B)
}
</math> and <math>
\xymatrix{
&\ar[dl]_{f}J\ar[dr]^{g}&\\
FI\ar[rr]_{\theta_I}&&GI
}
</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
A ''monoidal adjunction'' between two monoidal functors
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{D},\bullet,J)\Rightarrow(\mathcal{C},\tens,I)
</math>
is an adjunction between the underlying functors <math>F</math> and <math>G</math> such that the unit and the counit
:<math>\eta:\mathcal{C}\Rightarrow G\circ F</math> and <math>\varepsilon:F\circ G\Rightarrow\mathcal{D}</math>
induce monoidal natural transformations between the corresponding monoidal functors.
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
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>
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.
}}

=== Compact closed categories ===

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a (left) dual.
}}

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
\xymatrix{
&A\tens(B\tens A)\ar[r]^{\alpha_{A,B,A}^{-1}}&(A\tens B)\tens A\ar[dr]^{\varepsilon\tens A}\\
A\tens I\ar[ur]^{A\tens\eta}&&&I\tens A\ar[d]^{\lambda_A}\\
A\ar[u]^{\rho_A^{-1}}\ar@{=}[rrr]&&&A\\
}
</math>
and
:<math>
\xymatrix{
&(B\tens A)\tens B\ar[r]^{\alpha_{B,A,B}}&B\tens(A\tens B)\ar[dr]^{B\tens\varepsilon}\\
I\tens B\ar[ur]^{\eta\tens B}&&&B\tens I\ar[d]^{\rho_B}\\
B\ar[u]^{\lambda_B^{-1}}\ar@{=}[rrr]&&&B\\
}
</math>
commute. The object <math>A</math> is called a left dual of <math>B</math> (and conversely <math>B</math> is a right dual of <math>A</math>).
}}

{{Lemma|
Two left (resp. right) duals of a same object <math>B</math> are necessarily isomorphic.
}}

{{Lemma|
In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.
}}

{{Property|
A compact closed category <math>\mathcal{C}</math> is monoidal closed, with closure defined by
:<math>\mathcal{C}(A\tens B,C)\cong\mathcal{C}(B,A^*\tens C)</math>
}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2009-03-25T14:46:06Z

Samuel Mimram: /* Compact closed categories */

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 <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> 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|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
\xymatrix{
&(M\tens M)\tens M\ar[dl]_{\alpha_{M,M,M}}\ar[r]^-{\mu\tens M}&M\tens M\ar[dd]^{\mu}\\
M\tens(M\tens M)\ar[d]_{M\tens\mu}&&\\
M\tens M\ar[rr]_{\mu}&&M\\
}
</math>
and
:<math>
\xymatrix{
I\tens M\ar[r]^{\eta\tens M}\ar[dr]_{\lambda_M}&M\tens M\ar[d]_\mu&\ar[l]_{M\tens\eta}\ar[dl]^{\rho_M}M\tens I\\
&M&
}
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
\xymatrix{
(\mathcal{M},\times,\top)\ar[rr]^{(L,l)}&\bot&\ar[ll]^{(M,m)}(\mathcal{L},\otimes,I)
}
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>
\xymatrix{
(FA\bullet FB)\bullet FC\ar[d]_{\phi_{A,B}\bullet FC}\ar[r]^{\alpha_{FA,FB,FC}}&FA\bullet(FB\bullet FC)\ar[dr]^{FA\bullet\phi_{B,C}}\\
F(A\otimes B)\bullet FC\ar[dr]_{\phi_{A\otimes B,C}}&&FA\bullet F(B\otimes C)\ar[d]^{\phi_{A,B\otimes C}}\\
&F((A\otimes B)\otimes C)\ar[r]_{F\alpha_{A,B,C}}&F(A\otimes(B\otimes C))
}
</math>
and
:<math>
\xymatrix{
FA\bullet J\ar[d]_{\rho_{FA}}\ar[r]^{FA\bullet\phi}&FA\bullet FI\ar[d]^{\phi_{A,I}}\\
FA&\ar[l]^{F\rho_A}F(A\otimes I)
}
</math> and <math>
\xymatrix{
J\bullet FB\ar[d]_{\lambda_{FB}}\ar[r]^{\phi\bullet FB}&FI\bullet FB\ar[d]^{\phi_{I,B}}\\
FB&\ar[l]^{F\lambda_B}F(I\otimes B)
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>
\xymatrix{
FA\bullet FB\ar[d]_{f_{A,B}}\ar[r]^{\theta_A\bullet\theta_B}&\ar[d]^{g_{A,B}}GA\bullet GB\\
F(A\tens B)\ar[r]_{\theta_{A\tens B}}&G(A\tens B)
}
</math> and <math>
\xymatrix{
&\ar[dl]_{f}J\ar[dr]^{g}&\\
FI\ar[rr]_{\theta_I}&&GI
}
</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
A ''monoidal adjunction'' between two monoidal functors
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{D},\bullet,J)\Rightarrow(\mathcal{C},\tens,I)
</math>
is an adjunction between the underlying functors <math>F</math> and <math>G</math> such that the unit and the counit
:<math>\eta:\mathcal{C}\Rightarrow G\circ F</math> and <math>\varepsilon:F\circ G\Rightarrow\mathcal{D}</math>
induce monoidal natural transformations between the corresponding monoidal functors.
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
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>
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.
}}

=== Compact closed categories ===

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a (left) dual.
}}

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
\xymatrix{
&A\tens(B\tens A)\ar[r]^{\alpha_{A,B,A}^{-1}}&(A\tens B)\tens A\ar[dr]^{\varepsilon\tens A}\\
A\tens I\ar[ur]^{A\tens\eta}&&&I\tens A\ar[d]^{\lambda_A}\\
A\ar[u]^{\rho_A^{-1}}\ar@{=}[rrr]&&&A\\
}
</math>
and
:<math>
\xymatrix{
&(B\tens A)\tens B\ar[r]^{\alpha_{B,A,B}}&B\tens(A\tens B)\ar[dr]^{B\tens\varepsilon}\\
I\tens B\ar[ur]^{\eta\tens B}&&&B\tens I\ar[d]^{\rho_B}\\
B\ar[u]^{\lambda_B^{-1}}\ar@{=}[rrr]&&&B\\
}
</math>
commute. The object <math>A</math> is called a left dual of <math>B</math> (and conversely <math>B</math> is a right dual of <math>A</math>).
}}

{{Lemma|
Two left (resp. right) duals of a same object <math>B</math> are necessarily isomorphic.
}}

{{Lemma|
In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.
}}

{{Property|
A compact closed category is monoidal closed.
}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2009-03-25T14:42:56Z

Samuel Mimram: /* Compact closed categories */

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 <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> 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|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
\xymatrix{
&(M\tens M)\tens M\ar[dl]_{\alpha_{M,M,M}}\ar[r]^-{\mu\tens M}&M\tens M\ar[dd]^{\mu}\\
M\tens(M\tens M)\ar[d]_{M\tens\mu}&&\\
M\tens M\ar[rr]_{\mu}&&M\\
}
</math>
and
:<math>
\xymatrix{
I\tens M\ar[r]^{\eta\tens M}\ar[dr]_{\lambda_M}&M\tens M\ar[d]_\mu&\ar[l]_{M\tens\eta}\ar[dl]^{\rho_M}M\tens I\\
&M&
}
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
\xymatrix{
(\mathcal{M},\times,\top)\ar[rr]^{(L,l)}&\bot&\ar[ll]^{(M,m)}(\mathcal{L},\otimes,I)
}
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>
\xymatrix{
(FA\bullet FB)\bullet FC\ar[d]_{\phi_{A,B}\bullet FC}\ar[r]^{\alpha_{FA,FB,FC}}&FA\bullet(FB\bullet FC)\ar[dr]^{FA\bullet\phi_{B,C}}\\
F(A\otimes B)\bullet FC\ar[dr]_{\phi_{A\otimes B,C}}&&FA\bullet F(B\otimes C)\ar[d]^{\phi_{A,B\otimes C}}\\
&F((A\otimes B)\otimes C)\ar[r]_{F\alpha_{A,B,C}}&F(A\otimes(B\otimes C))
}
</math>
and
:<math>
\xymatrix{
FA\bullet J\ar[d]_{\rho_{FA}}\ar[r]^{FA\bullet\phi}&FA\bullet FI\ar[d]^{\phi_{A,I}}\\
FA&\ar[l]^{F\rho_A}F(A\otimes I)
}
</math> and <math>
\xymatrix{
J\bullet FB\ar[d]_{\lambda_{FB}}\ar[r]^{\phi\bullet FB}&FI\bullet FB\ar[d]^{\phi_{I,B}}\\
FB&\ar[l]^{F\lambda_B}F(I\otimes B)
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>
\xymatrix{
FA\bullet FB\ar[d]_{f_{A,B}}\ar[r]^{\theta_A\bullet\theta_B}&\ar[d]^{g_{A,B}}GA\bullet GB\\
F(A\tens B)\ar[r]_{\theta_{A\tens B}}&G(A\tens B)
}
</math> and <math>
\xymatrix{
&\ar[dl]_{f}J\ar[dr]^{g}&\\
FI\ar[rr]_{\theta_I}&&GI
}
</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
A ''monoidal adjunction'' between two monoidal functors
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{D},\bullet,J)\Rightarrow(\mathcal{C},\tens,I)
</math>
is an adjunction between the underlying functors <math>F</math> and <math>G</math> such that the unit and the counit
:<math>\eta:\mathcal{C}\Rightarrow G\circ F</math> and <math>\varepsilon:F\circ G\Rightarrow\mathcal{D}</math>
induce monoidal natural transformations between the corresponding monoidal functors.
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
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>
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.
}}

=== Compact closed categories ===

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a (left) dual.
}}

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
\xymatrix{
&A\tens(B\tens A)\ar[r]^{\alpha_{A,B,A}^{-1}}&(A\tens B)\tens A\ar[dr]^{\varepsilon\tens A}\\
A\tens I\ar[ur]^{A\tens\eta}&&&I\tens A\ar[d]^{\lambda_A}\\
A\ar[u]^{\rho_A^{-1}}\ar@{=}[rrr]&&&A\\
}
</math>
and
:<math>
\xymatrix{
&(B\tens A)\tens B\ar[r]^{\alpha_{B,A,B}}&B\tens(A\tens B)\ar[dr]^{B\tens\varepsilon}\\
I\tens B\ar[ur]^{\eta\tens B}&&&B\tens I\ar[d]^{\rho_B}\\
B\ar[u]^{\lambda_B^{-1}}\ar@{=}[rrr]&&&B\\
}
</math>
commute.
}}

In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.

{{Property|
A compact closed category is monoidal closed.
}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2009-03-25T14:40:53Z

Samuel Mimram: /* Compact closed categories */

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 <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> 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|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
\xymatrix{
&(M\tens M)\tens M\ar[dl]_{\alpha_{M,M,M}}\ar[r]^-{\mu\tens M}&M\tens M\ar[dd]^{\mu}\\
M\tens(M\tens M)\ar[d]_{M\tens\mu}&&\\
M\tens M\ar[rr]_{\mu}&&M\\
}
</math>
and
:<math>
\xymatrix{
I\tens M\ar[r]^{\eta\tens M}\ar[dr]_{\lambda_M}&M\tens M\ar[d]_\mu&\ar[l]_{M\tens\eta}\ar[dl]^{\rho_M}M\tens I\\
&M&
}
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
\xymatrix{
(\mathcal{M},\times,\top)\ar[rr]^{(L,l)}&\bot&\ar[ll]^{(M,m)}(\mathcal{L},\otimes,I)
}
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>
\xymatrix{
(FA\bullet FB)\bullet FC\ar[d]_{\phi_{A,B}\bullet FC}\ar[r]^{\alpha_{FA,FB,FC}}&FA\bullet(FB\bullet FC)\ar[dr]^{FA\bullet\phi_{B,C}}\\
F(A\otimes B)\bullet FC\ar[dr]_{\phi_{A\otimes B,C}}&&FA\bullet F(B\otimes C)\ar[d]^{\phi_{A,B\otimes C}}\\
&F((A\otimes B)\otimes C)\ar[r]_{F\alpha_{A,B,C}}&F(A\otimes(B\otimes C))
}
</math>
and
:<math>
\xymatrix{
FA\bullet J\ar[d]_{\rho_{FA}}\ar[r]^{FA\bullet\phi}&FA\bullet FI\ar[d]^{\phi_{A,I}}\\
FA&\ar[l]^{F\rho_A}F(A\otimes I)
}
</math> and <math>
\xymatrix{
J\bullet FB\ar[d]_{\lambda_{FB}}\ar[r]^{\phi\bullet FB}&FI\bullet FB\ar[d]^{\phi_{I,B}}\\
FB&\ar[l]^{F\lambda_B}F(I\otimes B)
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>
\xymatrix{
FA\bullet FB\ar[d]_{f_{A,B}}\ar[r]^{\theta_A\bullet\theta_B}&\ar[d]^{g_{A,B}}GA\bullet GB\\
F(A\tens B)\ar[r]_{\theta_{A\tens B}}&G(A\tens B)
}
</math> and <math>
\xymatrix{
&\ar[dl]_{f}J\ar[dr]^{g}&\\
FI\ar[rr]_{\theta_I}&&GI
}
</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
A ''monoidal adjunction'' between two monoidal functors
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{D},\bullet,J)\Rightarrow(\mathcal{C},\tens,I)
</math>
is an adjunction between the underlying functors <math>F</math> and <math>G</math> such that the unit and the counit
:<math>\eta:\mathcal{C}\Rightarrow G\circ F</math> and <math>\varepsilon:F\circ G\Rightarrow\mathcal{D}</math>
induce monoidal natural transformations between the corresponding monoidal functors.
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
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>
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.
}}

=== Compact closed categories ===

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a (left) dual.
}}

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
\xymatrix{
&A\tens(B\tens A)\ar[r]^{\alpha_{A,B,A}^{-1}}&(A\tens B)\tens A\ar[dr]^{\varepsilon\tens A}\\
A\tens I\ar[ur]^{A\tens\eta}&&&I\tens A\ar[d]^{\lambda_A}\\
A\ar[u]^{\rho_A^{-1}}\ar@{=}[rrr]&&&A\\
}
</math>
commute.
}}

In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.

{{Property|
A compact closed category is monoidal closed.
}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2009-03-25T14:35:58Z

Samuel Mimram: /* Modeling ILL */

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 <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> 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|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
\xymatrix{
&(M\tens M)\tens M\ar[dl]_{\alpha_{M,M,M}}\ar[r]^-{\mu\tens M}&M\tens M\ar[dd]^{\mu}\\
M\tens(M\tens M)\ar[d]_{M\tens\mu}&&\\
M\tens M\ar[rr]_{\mu}&&M\\
}
</math>
and
:<math>
\xymatrix{
I\tens M\ar[r]^{\eta\tens M}\ar[dr]_{\lambda_M}&M\tens M\ar[d]_\mu&\ar[l]_{M\tens\eta}\ar[dl]^{\rho_M}M\tens I\\
&M&
}
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
\xymatrix{
(\mathcal{M},\times,\top)\ar[rr]^{(L,l)}&\bot&\ar[ll]^{(M,m)}(\mathcal{L},\otimes,I)
}
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>
\xymatrix{
(FA\bullet FB)\bullet FC\ar[d]_{\phi_{A,B}\bullet FC}\ar[r]^{\alpha_{FA,FB,FC}}&FA\bullet(FB\bullet FC)\ar[dr]^{FA\bullet\phi_{B,C}}\\
F(A\otimes B)\bullet FC\ar[dr]_{\phi_{A\otimes B,C}}&&FA\bullet F(B\otimes C)\ar[d]^{\phi_{A,B\otimes C}}\\
&F((A\otimes B)\otimes C)\ar[r]_{F\alpha_{A,B,C}}&F(A\otimes(B\otimes C))
}
</math>
and
:<math>
\xymatrix{
FA\bullet J\ar[d]_{\rho_{FA}}\ar[r]^{FA\bullet\phi}&FA\bullet FI\ar[d]^{\phi_{A,I}}\\
FA&\ar[l]^{F\rho_A}F(A\otimes I)
}
</math> and <math>
\xymatrix{
J\bullet FB\ar[d]_{\lambda_{FB}}\ar[r]^{\phi\bullet FB}&FI\bullet FB\ar[d]^{\phi_{I,B}}\\
FB&\ar[l]^{F\lambda_B}F(I\otimes B)
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>
\xymatrix{
FA\bullet FB\ar[d]_{f_{A,B}}\ar[r]^{\theta_A\bullet\theta_B}&\ar[d]^{g_{A,B}}GA\bullet GB\\
F(A\tens B)\ar[r]_{\theta_{A\tens B}}&G(A\tens B)
}
</math> and <math>
\xymatrix{
&\ar[dl]_{f}J\ar[dr]^{g}&\\
FI\ar[rr]_{\theta_I}&&GI
}
</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
A ''monoidal adjunction'' between two monoidal functors
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{D},\bullet,J)\Rightarrow(\mathcal{C},\tens,I)
</math>
is an adjunction between the underlying functors <math>F</math> and <math>G</math> such that the unit and the counit
:<math>\eta:\mathcal{C}\Rightarrow G\circ F</math> and <math>\varepsilon:F\circ G\Rightarrow\mathcal{D}</math>
induce monoidal natural transformations between the corresponding monoidal functors.
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
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>
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.
}}

=== Compact closed categories ===

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a (left) dual.
}}

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
TODO
</math>
commute.
}}

In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.

{{Property|
A compact closed category is monoidal closed.
}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2009-03-25T14:28:08Z

Samuel Mimram: /* Modeling ILL */

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 <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> 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|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
\xymatrix{
&(M\tens M)\tens M\ar[dl]_{\alpha_{M,M,M}}\ar[r]^-{\mu\tens M}&M\tens M\ar[dd]^{\mu}\\
M\tens(M\tens M)\ar[d]_{M\tens\mu}&&\\
M\tens M\ar[rr]_{\mu}&&M\\
}
</math>
and
:<math>
\xymatrix{
I\tens M\ar[r]^{\eta\tens M}\ar[dr]_{\lambda_M}&M\tens M\ar[d]_\mu&\ar[l]_{M\tens\eta}\ar[dl]^{\rho_M}M\tens I\\
&M&
}
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
\xymatrix{
(\mathcal{M},\times,\top)\ar[rr]^{(L,l)}&\bot&\ar[ll]^{(M,m)}(\mathcal{L},\otimes,I)
}
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>
\xymatrix{
(FA\bullet FB)\bullet FC\ar[d]_{\phi_{A,B}\bullet FC}\ar[r]^{\alpha_{FA,FB,FC}}&FA\bullet(FB\bullet FC)\ar[dr]^{FA\bullet\phi_{B,C}}\\
F(A\otimes B)\bullet FC\ar[dr]_{\phi_{A\otimes B,C}}&&FA\bullet F(B\otimes C)\ar[d]^{\phi_{A,B\otimes C}}\\
&F((A\otimes B)\otimes C)\ar[r]_{F\alpha_{A,B,C}}&F(A\otimes(B\otimes C))
}
</math>
and
:<math>
\xymatrix{
FA\bullet J\ar[d]_{\rho_{FA}}\ar[r]^{FA\bullet\phi}&FA\bullet FI\ar[d]^{\phi_{A,I}}\\
FA&\ar[l]^{F\rho_A}F(A\otimes I)
}
</math> and <math>
\xymatrix{
J\bullet FB\ar[d]_{\lambda_{FB}}\ar[r]^{\phi\bullet FB}&FI\bullet FB\ar[d]^{\phi_{I,B}}\\
FB&\ar[l]^{F\lambda_B}F(I\otimes B)
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>
\xymatrix{
FA\bullet FB\ar[d]_{f_{A,B}}\ar[r]^{\theta_A\bullet\theta_B}&\ar[d]^{g_{A,B}}GA\bullet GB\\
F(A\tens B)\ar[r]_{\theta_{A\tens B}}&G(A\tens B)
}
</math> and <math>
\xymatrix{
&\ar[dl]_{f}J\ar[dr]^{g}&\\
FI\ar[rr]_{\theta_I}&&GI
}
</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
TODO
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
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>
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.
}}

=== Compact closed categories ===

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a (left) dual.
}}

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
TODO
</math>
commute.
}}

In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.

{{Property|
A compact closed category is monoidal closed.
}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2009-03-24T18:59:48Z

Samuel Mimram: /* Modeling ILL */

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 <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> 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|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
\xymatrix{
&(M\tens M)\tens M\ar[dl]_{\alpha_{M,M,M}}\ar[r]^-{\mu\tens M}&M\tens M\ar[dd]^{\mu}\\
M\tens(M\tens M)\ar[d]_{M\tens\mu}&&\\
M\tens M\ar[rr]_{\mu}&&M\\
}
</math>
and
:<math>
\xymatrix{
I\tens M\ar[r]^{\eta\tens M}\ar[dr]_{\lambda_M}&M\tens M\ar[d]_\mu&\ar[l]_{M\tens\eta}\ar[dl]^{\rho_M}M\tens I\\
&M&
}
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
\xymatrix{
(\mathcal{M},\times,\top)\ar[rr]^{(L,l)}&\bot&\ar[ll]^{(M,m)}(\mathcal{L},\otimes,I)
}
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>
\xymatrix{
(FA\bullet FB)\bullet FC\ar[d]_{\phi_{A,B}\bullet FC}\ar[r]^{\alpha_{FA,FB,FC}}&FA\bullet(FB\bullet FC)\ar[dr]^{FA\bullet\phi_{B,C}}\\
F(A\otimes B)\bullet FC\ar[dr]_{\phi_{A\otimes B,C}}&&FA\bullet F(B\otimes C)\ar[d]^{\phi_{A,B\otimes C}}\\
&F((A\otimes B)\otimes C)\ar[r]_{F\alpha_{A,B,C}}&F(A\otimes(B\otimes C))
}
</math>
and
:<math>
\xymatrix{
FA\bullet J\ar[d]_{\rho_{FA}}\ar[r]^{FA\bullet\phi}&FA\bullet FI\ar[d]^{\phi_{A,I}}\\
FA&\ar[l]^{F\rho_A}F(A\otimes I)
}
</math> and <math>
\xymatrix{
J\bullet FB\ar[d]_{\lambda_{FB}}\ar[r]^{\phi\bullet FB}&FI\bullet FB\ar[d]^{\phi_{I,B}}\\
FB&\ar[l]^{F\lambda_B}F(I\otimes B)
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>TODO</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
TODO
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
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>
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.
}}

=== Compact closed categories ===

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a (left) dual.
}}

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
TODO
</math>
commute.
}}

In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.

{{Property|
A compact closed category is monoidal closed.
}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2009-03-24T18:40:22Z

Samuel Mimram: /* Modeling ILL */

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 <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> 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|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
\xymatrix{
&(M\tens M)\tens M\ar[dl]_{\alpha_{M,M,M}}\ar[r]^-{\mu\tens M}&M\tens M\ar[dd]^{\mu}\\
M\tens(M\tens M)\ar[d]_{M\tens\mu}&&\\
M\tens M\ar[rr]_{\mu}&&M\\
}
</math>
and
:<math>
\xymatrix{
I\tens M\ar[r]^{\eta\tens M}\ar[dr]_{\lambda_M}&M\tens M\ar[d]_\mu&\ar[l]_{M\tens\eta}\ar[dl]^{\rho_M}M\tens I\\
&M&
}
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
\xymatrix{
(\mathcal{M},\times,\top)\ar[rr]^{(L,l)}&\bot&\ar[ll]^{(M,m)}(\mathcal{L},\otimes,I)
}
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>
\xymatrix{
(FA\bullet FB)\bullet FC\ar[d]_{\phi_{A,B}\bullet FC}\ar[r]^{\alpha_{FA,FB,FC}}&FA\bullet(FB\bullet FC)\ar[d]^{FA\bullet\phi_{B,C}}\\
F(A\otimes B)\bullet FC\ar[d]_{\phi_{A\otimes B,C}}&FA\bullet F(B\otimes C)\ar[d]^{\phi_{A,B\otimes C}}\\
F((A\otimes B)\otimes C)\ar[r]_{F\alpha_{A,B,C}}&F(A\otimes(B\otimes C))
}
</math>
and
:<math>
\xymatrix{
FA\bullet J\ar[d]_{\rho_{FA}}\ar[r]^{FA\bullet\phi}&FA\bullet FI\ar[d]^{\phi_{A,I}}\\
FA&\ar[l]^{F\rho_A}F(A\otimes I)
}
</math> and <math>
\xymatrix{
J\bullet FB\ar[d]_{\lambda_{FB}}\ar[r]^{\phi\bullet FB}&FI\bullet FB\ar[d]^{\phi_{I,B}}\\
FB&\ar[l]^{F\lambda_B}F(I\otimes B)
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math> and <math>
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>TODO</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
TODO
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
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>
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.
}}

=== Compact closed categories ===

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a (left) dual.
}}

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
TODO
</math>
commute.
}}

In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.

{{Property|
A compact closed category is monoidal closed.
}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2009-03-24T18:39:55Z

Samuel Mimram: /* Modeling ILL */

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 <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> 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|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
\xymatrix{
&(M\tens M)\tens M\ar[dl]_{\alpha_{M,M,M}}\ar[r]^-{\mu\tens M}&M\tens M\ar[dd]^{\mu}\\
M\tens(M\tens M)\ar[d]_{M\tens\mu}&&\\
M\tens M\ar[rr]_{\mu}&&M\\
}
</math>
and
:<math>
\xymatrix{
I\tens M\ar[r]^{\eta\tens M}\ar[dr]_{\lambda_M}&M\tens M\ar[d]_\mu&\ar[l]_{M\tens\eta}\ar[dl]^{\rho_M}M\tens I\\
&M&
}
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
\xymatrix{
(\mathcal{M},\times,\top)\ar[rr]^{(L,l)}&\bot&\ar[ll]^{(M,m)}(\mathcal{L},\otimes,I)
}
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>
\xymatrix{
(FA\bullet FB)\bullet FC\ar[d]_{\phi_{A,B}\bullet FC}\ar[r]^{\alpha_{FA,FB,FC}}&FA\bullet(FB\bullet FC)\ar[d]^{FA\bullet\phi_{B,C}}\\
F(A\otimes B)\bullet FC\ar[d]_{\phi_{A\otimes B,C}}&FA\bullet F(B\otimes C)\ar[d]^{\phi_{A,B\otimes C}}\\
F((A\otimes B)\otimes C)\ar[r]_{F\alpha_{A,B,C}}&F(A\otimes(B\otimes C))
}
</math>
and
:<math>
\xymatrix{
FA\bullet J\ar[d]_{\rho_{FA}}\ar[r]^{FA\bullet\phi}&FA\bullet FI\ar[d]^{\phi_{A,I}}\\
FA&\ar[l]^{F\rho_A}F(A\otimes I)
}
</math> and <math>
\xymatrix{
J\bullet FB\ar[d]_{\lambda_{FB}}\ar[r]^{\phi\bullet FB}&FI\bullet FB\ar[d]^{\phi_{I,B}}\\
FB&\ar[l]^{F\lambda_B}F(I\otimes B)
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
\qquad
\text{and}
\qquad
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>TODO</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
TODO
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
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>
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.
}}

=== Compact closed categories ===

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a (left) dual.
}}

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
TODO
</math>
commute.
}}

In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.

{{Property|
A compact closed category is monoidal closed.
}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2009-03-24T18:38:42Z

Samuel Mimram: /* Modeling ILL */

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 <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> 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|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
\xymatrix{
&(M\tens M)\tens M\ar[dl]_{\alpha_{M,M,M}}\ar[r]^-{\mu\tens M}&M\tens M\ar[dd]^{\mu}\\
M\tens(M\tens M)\ar[d]_{M\tens\mu}&&\\
M\tens M\ar[rr]_{\mu}&&M\\
}
</math>
and
:<math>
\xymatrix{
I\tens M\ar[r]^{\eta\tens M}\ar[dr]_{\lambda_M}&M\tens M\ar[d]_\mu&\ar[l]_{M\tens\eta}\ar[dl]^{\rho_M}M\tens I\\
&M&
}
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
\xymatrix{
(\mathcal{M},\times,\top)\ar[rr]^{(L,l)}&\bot&\ar[ll]^{(M,m)}(\mathcal{L},\otimes,I)
}
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>
\xymatrix{
(FA\bullet FB)\bullet FC\ar[d]_{\phi_{A,B}\bullet FC}\ar[r]^{\alpha_{FA,FB,FC}}&FA\bullet(FB\bullet FC)\ar[d]^{FA\bullet\phi_{B,C}}\\
F(A\otimes B)\bullet FC\ar[d]_{\phi_{A\otimes B,C}}&FA\bullet F(B\otimes C)\ar[d]^{\phi_{A,B\otimes C}}\\
F((A\otimes B)\otimes C)\ar[r]_{F\alpha_{A,B,C}}&F(A\otimes(B\otimes C))
}
</math>
and
:<math>
\xymatrix{
FA\bullet J\ar[d]_{\rho_{FA}}\ar[r]^{FA\bullet\phi}&FA\bullet FI\ar[d]^{\phi_{A,I}}\\
FA&\ar[l]^{F\rho_A}F(A\otimes I)
}
</math> and <math>TODO</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
\qquad
\text{and}
\qquad
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>TODO</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
TODO
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
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>
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.
}}

=== Compact closed categories ===

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a (left) dual.
}}

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
TODO
</math>
commute.
}}

In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.

{{Property|
A compact closed category is monoidal closed.
}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2009-03-24T18:36:25Z

Samuel Mimram: /* Modeling ILL */

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 <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> 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|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
\xymatrix{
&(M\tens M)\tens M\ar[dl]_{\alpha_{M,M,M}}\ar[r]^-{\mu\tens M}&M\tens M\ar[dd]^{\mu}\\
M\tens(M\tens M)\ar[d]_{M\tens\mu}&&\\
M\tens M\ar[rr]_{\mu}&&M\\
}
</math>
and
:<math>
\xymatrix{
I\tens M\ar[r]^{\eta\tens M}\ar[dr]_{\lambda_M}&M\tens M\ar[d]_\mu&\ar[l]_{M\tens\eta}\ar[dl]^{\rho_M}M\tens I\\
&M&
}
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
\xymatrix{
(\mathcal{M},\times,\top)\ar[rr]^{(L,l)}&\bot&\ar[ll]^{(M,m)}(\mathcal{L},\otimes,I)
}
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>
\xymatrix{
(FA\bullet FB)\bullet FC\ar[d]_{\phi_{A,B}\bullet FC}\ar[r]^{\alpha_{FA,FB,FC}}&FA\bullet(FB\bullet FC)\ar[d]^{FA\bullet\phi_{B,C}}\\
F(A\otimes B)\bullet FC\ar[d]_{\phi_{A\otimes B,C}}&FA\bullet F(B\otimes C)\ar[d]^{\phi_{A,B\otimes C}}\\
F((A\otimes B)\otimes C)\ar[r]_{F\alpha_{A,B,C}}&F(A\otimes(B\otimes C))
}
</math>
and
:<math>TODO</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
\qquad
\text{and}
\qquad
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>TODO</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
TODO
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
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>
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.
}}

=== Compact closed categories ===

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a (left) dual.
}}

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
TODO
</math>
commute.
}}

In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.

{{Property|
A compact closed category is monoidal closed.
}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2009-03-24T18:33:31Z

Samuel Mimram: /* Modeling ILL */

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 <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> 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|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
\xymatrix{
&(M\tens M)\tens M\ar[dl]_{\alpha_{M,M,M}}\ar[r]^-{\mu\tens M}&M\tens M\ar[dd]^{\mu}\\
M\tens(M\tens M)\ar[d]_{M\tens\mu}&&\\
M\tens M\ar[rr]_{\mu}&&M\\
}
</math>
and
:<math>
\xymatrix{
I\tens M\ar[r]^{\eta\tens M}\ar[dr]_{\lambda_M}&M\tens M\ar[d]_\mu&\ar[l]_{M\tens\eta}\ar[dl]^{\rho_M}M\tens I\\
&M&
}
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
\xymatrix{
(\mathcal{M},\times,\top)\ar[rr]^{(L,l)}&\bot&\ar[ll]^{(M,m)}(\mathcal{L},\otimes,I)
}
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>TODO</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
\qquad
\text{and}
\qquad
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>TODO</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
TODO
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
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>
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.
}}

=== Compact closed categories ===

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a (left) dual.
}}

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
TODO
</math>
commute.
}}

In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.

{{Property|
A compact closed category is monoidal closed.
}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2009-03-24T18:29:42Z

Samuel Mimram: /* Modeling the additives */

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 <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> 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|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
\xymatrix{
&(M\tens M)\tens M\ar[dl]_{\alpha_{M,M,M}}\ar[r]^-{\mu\tens M}&M\tens M\ar[dd]^{\mu}\\
M\tens(M\tens M)\ar[d]_{M\tens\mu}&&\\
M\tens M\ar[rr]_{\mu}&&M\\
}
</math>
and
:<math>
\xymatrix{
I\tens M\ar[r]^{\eta\tens M}\ar[dr]_{\lambda_M}&M\tens M\ar[d]_\mu&\ar[l]_{M\tens\eta}\ar[dl]^{\rho_M}M\tens I\\
&M&
}
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
(\mathcal{M},\times,\top) TODO (\mathcal{L},\otimes,I)
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>TODO</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
\qquad
\text{and}
\qquad
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>TODO</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
TODO
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
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>
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.
}}

=== Compact closed categories ===

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a (left) dual.
}}

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
TODO
</math>
commute.
}}

In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.

{{Property|
A compact closed category is monoidal closed.
}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2009-03-24T18:21:50Z

Samuel Mimram: /* Modeling the additives */

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 <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> 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|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
TODO
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
(\mathcal{M},\times,\top) TODO (\mathcal{L},\otimes,I)
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>TODO</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
\qquad
\text{and}
\qquad
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>TODO</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
TODO
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
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>
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.
}}

=== Compact closed categories ===

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a (left) dual.
}}

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
TODO
</math>
commute.
}}

In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.

{{Property|
A compact closed category is monoidal closed.
}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2009-03-24T18:20:29Z

Samuel Mimram: /* Modeling IMLL */

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 <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> 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|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
TODO
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
TODO
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
(\mathcal{M},\times,\top) TODO (\mathcal{L},\otimes,I)
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>TODO</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
\qquad
\text{and}
\qquad
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>TODO</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
TODO
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
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>
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.
}}

=== Compact closed categories ===

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a (left) dual.
}}

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
TODO
</math>
commute.
}}

In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.

{{Property|
A compact closed category is monoidal closed.
}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2009-03-24T18:16:44Z

Samuel Mimram: /* Modeling IMLL */

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 <ref>{{BibEntry|bibtype=book|author=MacLane, Saunders|title=Categories for the Working Mathematician|publisher=Springer Verlag|year=1971|volume=5|series=Graduate Texts in Mathematics}}</ref>for a more detailed introduction to category theory. See <ref>{{BibEntry|bibtype=book|author=Melliès, Paul-André|title=Categorical Semantics of Linear Logic}}</ref>for a detailed treatment of categorical semantics of linear logic.

== Basic category theory recalled ==
{{Definition|title=Category|
}}

{{Definition|title=Functor|
}}

{{Definition|title=Natural transformation|
}}

{{Definition|title=Adjunction|
}}

{{Definition|title=Monad|
}}

== Modeling [[IMLL]] ==

A model of [[IMLL]] is a ''closed symmetric monoidal category''. We recall the definition of these categories below.

{{Definition|title=Monoidal category|
A ''monoidal category'' <math>(\mathcal{C},\otimes,I,\alpha,\lambda,\rho)</math> is a category <math>\mathcal{C}</math> equipped with
* a functor <math>\otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C}</math> called ''tensor product'',
* an object <math>I</math> called ''unit object'',
* three natural isomorphisms <math>\alpha</math>, <math>\lambda</math> and <math>\rho</math>, called respectively ''associator'', ''left unitor'' and ''right unitor'', whose components are
: <math>
\alpha_{A,B,C}:(A\otimes B)\otimes C\to A\otimes (B\otimes C)
\qquad
\lambda_A:I\otimes A\to A
\qquad
\rho_A:A\otimes I\to A
</math>
such that
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
((A\otimes B)\otimes C)\otimes D\ar[d]_{\alpha_{A\otimes B,C,D}}\ar[r]^{\alpha_{A,B,C}\otimes D}&(A\otimes(B\otimes C))\otimes D\ar[r]^{\alpha_{A,B\otimes C,D}}&A\otimes((B\otimes C)\otimes D)\ar[d]^{A\otimes\alpha_{B,C,D}}\\
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
</math>
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
:<math>
\xymatrix{
(A\otimes I)\otimes B\ar[dr]_{\rho_A\otimes B}\ar[rr]^{\alpha_{A,I,B}}&&\ar[dl]^{A\otimes\lambda_B}A\otimes(I\otimes B)\\
&A\otimes B&
}
</math>
commutes.
}}

{{Definition|title=Braided, symmetric monoidal category|
A ''braided'' monoidal category is a category together with a natural isomorphism of components
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
called ''braiding'', such that the two diagrams
:<math>
\xymatrix{
&A\otimes(B\otimes C)\ar[r]^{\gamma_{A,B\otimes C}}&(B\otimes C)\otimes A\ar[dr]^{\alpha_{B,C,A}}\\
(A\otimes B)\otimes C\ar[ur]^{\alpha_{A,B,C}}\ar[dr]_{\gamma_{A,B}\otimes C}&&&B\otimes (C\otimes A)\\
&(B\otimes A)\otimes C\ar[r]_{\alpha_{B,A,C}}&B\otimes(A\otimes C)\ar[ur]_{B\otimes\gamma_{A,C}}\\
}
</math>
and
:<math>
\xymatrix{
&(A\otimes B)\otimes C\ar[r]^{\gamma_{A\otimes B,C}}&C\otimes (A\otimes B)\ar[dr]^{\alpha^{-1}_{C,A,B}}&\\
A\otimes (B\otimes C)\ar[ur]^{\alpha^{-1}_{A,B,C}}\ar[dr]_{A\otimes\gamma_{B,C}}&&&(C\otimes A)\otimes B\\
&A\otimes(C\otimes B)\ar[r]_{\alpha^{-1}_{A,C,B}}&(A\otimes C)\otimes B\ar[ur]_{\gamma_{A,C}\otimes B}&\\
}
</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.

A ''symmetric'' monoidal category is a braided monoidal category in which the braiding satisfies
:<math>\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B</math>
for every objects <math>A</math> and <math>B</math>.
}}

{{Definition|title=Closed monoidal category|
A monoidal category <math>(\mathcal{C},\tens,I)</math> is ''left closed'' when for every object <math>A</math>, the functor
:<math>B\mapsto A\otimes B</math>
has a right adjoint, written
:<math>B\mapsto(A\limp B)</math>
This means that there exists a bijection
:<math>\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)</math>
which is natural in <math>B</math> and <math>C</math>.
Equivalently, a monoidal category is left closed when it is equipped with a ''left closed structure'', which consists of
* an object <math>A\limp B</math>,
* a morphism <math>\mathrm{eval}_{A,B}:A\tens (A\limp B)\to B</math>, called ''left evaluation'',
for every objects <math>A</math> and <math>B</math>, such that for every morphism <math>f:A\otimes X\to B</math> there exists a unique morphism <math>h:X\to A\limp B</math> making the diagram
:<math>
TODO
</math>
commute.

Dually, the monoidal category <math>\mathcal{C}</math> is ''right closed'' when the functor <math>B\mapsto B\otimes A</math> 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|title=Product|
A ''product'' <math>(X,\pi_1,\pi_2)</math> of two coinitial morphisms <math>f:A\to B</math> and <math>g:A\to C</math> in a category <math>\mathcal{C}</math> is an object <math>X</math> of <math>\mathcal{C}</math> together with two morphisms <math>\pi_1:X\to A</math> and <math>\pi_2:X\to B</math> such that there exists a unique morphism <math>h:A\to X</math> making the diagram
:<math>
TODO
</math>
commute.
}}

A category has ''finite products'' when it has products and a terminal object.

{{Definition|title=Monoid|
A ''monoid'' <math>(M,\mu,\eta)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is an object <math>M</math> together with two morphisms
:<math>\mu:M\tens M \to M</math> and <math>\eta:I\to M</math>
such that the diagrams
:<math>
TODO
</math>
commute.
}}

{{Property|
Categories with products vs monoidal categories.
}}

== Modeling [[ILL]] ==

Introduced in<ref>{{BibEntry|type=journal|author=Benton, Nick|title=A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.|journal=CSL'94|volume=933|year=1995}}</ref>.

{{Definition|title=Linear-non linear (LNL) adjunction|
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
:<math>
(\mathcal{M},\times,\top) TODO (\mathcal{L},\otimes,I)
</math>
in which the category <math>\mathcal{M}</math> has finite products.
}}

:<math>\oc=L\circ M</math>

This section is devoted to defining the concepts necessary to define these adjunctions.

{{Definition|title=Monoidal functor|
A ''lax monoidal functor'' <math>(F,f)</math> between two monoidal categories <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> consists of
* a functor <math>F:\mathcal{C}\to\mathcal{D}</math> between the underlying categories,
* a natural transformation <math>f</math> of components <math>f_{A,B}:FA\bullet FB\to F(A\tens B)</math>,
* a morphism <math>f:J\to FI</math>
such that the diagrams
:<math>TODO</math>
commute for every objects <math>A</math>, <math>B</math> and <math>C</math> of <math>\mathcal{C}</math>. The morphisms <math>f_{A,B}</math> and <math>f</math> are called ''coherence maps''.

A lax monoidal functor is ''strong'' when the coherence maps are invertible and ''strict'' when they are identities.
}}

{{Definition|title=Monoidal natural transformation|
Suppose that <math>(\mathcal{C},\tens,I)</math> and <math>(\mathcal{D},\bullet,J)</math> are two monoidal categories and
:<math>
(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
\qquad
\text{and}
\qquad
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
</math>
are two monoidal functors between these categories. A ''monoidal natural transformation'' <math>\theta:(F,f)\to (G,g)</math> between these monoidal functors is a natural transformation <math>\theta:F\Rightarrow G</math> between the underlying functors such that the diagrams
:<math>TODO</math>
commute for every objects <math>A</math> and <math>B</math> of <math>\mathcal{D}</math>.
}}

{{Definition|title=Monoidal adjunction|
TODO
}}

== Modeling negation ==

=== *-autonomous categories ===

{{Definition|title=*-autonomous category|
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>
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.
}}

=== Compact closed categories ===

{{Definition|title=Compact closed category|
A symmetric monoidal category <math>(\mathcal{C},\tens,I)</math> is ''compact closed'' when every object <math>A</math> has a (left) dual.
}}

{{Definition|title=Dual objects|
A ''dual object'' structure <math>(A,B,\eta,\varepsilon)</math> in a monoidal category <math>(\mathcal{C},\tens,I)</math> is a pair of objects <math>A</math> and <math>B</math> together with two morphisms
:<math>\eta:I\to B\otimes A</math> and <math>\varepsilon:A\otimes B\to I</math>
such that the diagrams
:<math>
TODO
</math>
commute.
}}

In a compact closed category the left and right duals of an object <math>A</math> are isomorphic.

{{Property|
A compact closed category is monoidal closed.
}}

== Other categorical models ==

=== Lafont categories ===

=== Seely categories ===

=== Linear categories ===

== Properties of categorical models ==

=== The Kleisli category ===

== References ==
<references />

Categorical semantics

2009-03-24T18:14:37Z

Samuel Mimram: /* Modeling IMLL */

Categorical semantics

2009-03-24T18:13:44Z

Samuel Mimram: /* Modeling IMLL */

Categorical semantics

2009-03-24T14:40:03Z

Samuel Mimram: /* Modeling the additives */

Categorical semantics

2009-03-24T14:34:48Z

Samuel Mimram: /* Basic category theory recalled */

Categorical semantics

2009-03-24T14:32:09Z

Samuel Mimram: /* Modeling the additives */

Categorical semantics

2009-03-24T14:30:51Z

Samuel Mimram: /* Compact closed categories */

Categorical semantics

2009-03-24T14:30:42Z

Samuel Mimram: /* Compact closed categories */

Categorical semantics

2009-03-24T14:23:55Z

Samuel Mimram: /* Basic category theory recalled */

Categorical semantics

2009-03-24T14:23:41Z

Samuel Mimram:

Categorical semantics

2009-03-24T14:17:45Z

Samuel Mimram: /* Modeling IMLL */ pentagon

Phase semantics

2009-03-24T13:05:15Z

Samuel Mimram: /* Closure operators */

==Introduction==

The semantics given by phase spaces is a kind of "formula and provability semantics", and is thus quite different in spirit from the more usual denotational semantics of linear logic. (Those are rather some "formulas and ''proofs'' semantics".)

--- probably a whole lot more of blabla to put here... ---

==Preliminaries: relation and closure operators==

Part of the structure obtained from phase semantics works in a very general framework and relies solely on the notion of relation between two sets.

===Relations and operators on subsets===

The starting point of phase semantics is the notion of ''duality''. The structure needed to talk about duality is very simple: one just needs a relation <math>R</math> between two sets <math>X</math> and <math>Y</math>. Using standard mathematical practice, we can write either <math>(a,b) \in R</math> or <math>a\mathrel{R} b</math> to say that <math>a\in X</math> and <math>b\in Y</math> are related.

{{Definition|
If <math>R\subseteq X\times Y</math> is a relation, we write <math>R^\sim\subseteq Y\times X</math> for the converse relation: <math>(b,a)\in R^\sim</math> iff <math>(a,b)\in R</math>.
}}

Such a relation yields three interesting operators sending subsets of <math>X</math> to subsets of <math>Y</math>:

{{Definition|
Let <math>R\subseteq X\times Y</math> be a relation, define the operators <math>\langle R\rangle</math>, <math>[R]</math> and <math>\_^R</math> taking subsets of <math>X</math> to subsets of <math>Y</math> as follows:
# <math>b\in\langle R\rangle(x)</math> iff <math>\exists a\in X,\ (a,b)\in R \land a\in x</math>
# <math>b\in[R](x)</math> iff <math>\forall a\in X,\ (a,b)\in R \implies a\in x</math>
# <math>b\in x^R</math> iff <math>\forall a\in x, (a,b)\in R</math>
}}

The operator <math>\langle R\rangle</math> is usually called the ''direct image'' of the relation, <math>[R]</math> is sometimes called the ''universal image'' of the relation.

It is trivial to check that <math>\langle R\rangle</math> and <math>[R]</math> are covariant (increasing for the <math>\subseteq</math> relation) while <math>\_^R</math> is contravariant (decreasing for the <math>\subseteq</math> relation). More interesting:

{{Lemma|title=Galois Connections|
# <math>\langle R\rangle</math> is right-adjoint to <math>[R^\sim]</math>: for any <math>x\subseteq X</math> and <math>y\subseteq Y</math>, we have <math>[R^\sim]y \subseteq x</math> iff <math>y\subseteq \langle R\rangle(x)</math>
# we have <math>y\subseteq x^R</math> iff <math>x\subseteq y^{R^\sim}</math>
}}

This implies directly that <math>\langle R\rangle</math> commutes with arbitrary unions and <math>[R]</math> commutes with arbitrary intersections. (And in fact, any operator commuting with arbitrary unions (resp. intersections) is of the form <math>\langle R\rangle</math> (resp. <math>[R]</math>).

{{Remark|the operator <math>\_^R</math> sends unions to intersections because <math>\_^R : \mathcal{P}(X) \to \mathcal{P}(Y)^\mathrm{op}</math> is right adjoint to <math>\_^{R^\sim} : \mathcal{P}(Y)^{\mathrm{op}} \to \mathcal{P}(X)</math>...}}

===Closure operators===

{{Definition|
A closure operator on <math>\mathcal{P}(X)</math> is an monotonic increasing operator <math>P</math> on the subsets of <math>X</math> which satisfies:
# for all <math>x\subseteq X</math>, we have <math>x\subseteq P(x)</math>
# for all <math>x\subseteq X</math>, we have <math>P(P(x))\subseteq P(x)</math>
}}

Closure operators are quite common in mathematics and computer science. They correspond exactly to the notion of ''monad'' on a preorder...

It follows directly from the definition that for any closure operator <math>P</math>, the image <math>P(x)</math> is a fixed point of <math>P</math>. Moreover:

{{Lemma|
<math>P(x)</math> is the smallest fixed point of <math>P</math> containing <math>x</math>.
}}

One other important property is the following:

{{Lemma|
Write <math>\mathcal{F}(P) = \{x\ |\ P(x)\subseteq x\}</math> for the collection of fixed points of a closure operator <math>P</math>. We have that <math>\left(\mathcal{F}(P),\bigcap\right)</math> is a complete inf-lattice.
}}

{{Remark|
A closure operator is in fact determined by its set of fixed points: we have <math>P(x) = \bigcup \{ y\ |\ y\in\mathcal{F}(P),\,y\subseteq x\}</math>}}

Since any complete inf-lattice is automatically a complete sup-lattice, <math>\mathcal{F}(P)</math> is also a complete sup-lattice. However, the sup operation isn't given by plain union:

{{Lemma|
If <math>P</math> is a closure operator on <math>\mathcal{P}(X)</math>, and if <math>(x_i)_{i\in I}</math> is a (possibly infinite) family of subsets of <math>X</math>, we write <math>\bigvee_{i\in I} x_i = P\left(\bigcup_{i\in I} x_i\right)</math>.

We have <math>\left(\mathcal{F}(P),\bigcap,\bigvee\right)</math> is a complete lattice.
}}

{{Proof|
easy.
}}

A rather direct consequence of the Galois connections of the previous section is:

{{Lemma|
The operator and <math>\langle R\rangle \circ [R^\sim]</math> and the operator <math>x\mapsto {x^R}^{R^\sim}</math> are closures.
}}

A last trivial lemma:

{{Lemma|
We have <math>x^R = {{x^R}^{R^\sim}}^{R}</math>.

As a consequence, a subset <math>x\subseteq X</math> is in <math>\mathcal{F}({\_^R}^{R^\sim})</math> iff it is of the form <math>y^{R^\sim}</math>.
}}

{{Remark|everything gets a little simpler when <math>R</math> is a symmetric relation on <math>X</math>.}}

==Phase Semantics==

===Phase spaces===

{{Definition|title=monoid|
A monoid is simply a set <math>X</math> equipped with a binary operation <math>\_\cdot\_</math> s.t.:
# the operation is associative
# there is a neutral element <math>1\in X</math>
The monoid is ''commutative'' when the binary operation is commutative.
}}

{{Definition|title=Phase space|
A phase space is given by:
# a commutative monoid <math>(X,1,\cdot)</math>,
# together with a subset <math>\Bot\subseteq X</math>.
The elements of <math>X</math> are called ''phases''.

We write <math>\bot</math> for the relation <math>\{(a,b)\ |\ a\cdot b \in \Bot\}</math>. This relation is symmetric.

A ''fact'' in a phase space is simply a fixed point for the closure operator <math>x\mapsto x\biorth</math>.
}}

Thanks to the preliminary work, we have:

{{Corollary|
The set of facts of a phase space is a complete lattice where:
# <math>\bigwedge_{i\in I} x_i</math> is simply <math>\bigcap_{i\in I} x_i</math>,
# <math>\bigvee_{i\in I} x_i</math> is <math>\left(\bigcup_{i\in I} x_i\right)\biorth</math>.
}}

===Additive connectives===

The previous corollary makes the following definition correct:

{{Definition|title=additive connectives|
If <math>(X,1,\cdot,\Bot)</math> is a phase space, we define the following facts and operations on facts:
# <math>\top = X = \emptyset\orth</math>
# <math>\zero = \emptyset\biorth = X\orth</math>
# <math>x\with y = x\cap y</math>
# <math>x\plus y = (x\cup y)\biorth</math>
}}

Once again, the next lemma follows from previous observations:

{{Lemma|title=additive de Morgan laws|
We have
# <math>\zero\orth = \top</math>
# <math>\top\orth = \zero</math>
# <math>(x\with y)\orth = x\orth \plus y\orth</math>
# <math>(x\plus y)\orth = x\orth \with y\orth</math>
}}

===Multiplicative connectives===

In order to define the multiplicative connectives, we actually need to use the monoid structure of our phase space. One interpretation that is reminiscent in phase semantics is that our spaces are collections of ''tests'' / programs / proofs / ''strategies'' that can interact with each other. The result of the interaction between <math>a</math> and <math>b</math> is simply <math>a\cdot b</math>.

The set <math>\Bot</math> can be thought of as the set of "good" things, and we thus have <math>a\in x\orth</math> iff "<math>a</math> interacts correctly with all the elements of <math>x</math>".

{{Definition|
If <math>x</math> and <math>y</math> are two subsets of a phase space, we write <math>x\cdot y</math> for the set <math>\{a\cdot b\ |\ a\in x, b\in y\}</math>.
}}
Thus <math>x\cdot y</math> contains all the possible interactions between one element of <math>x</math> and one element of <math>y</math>.

The tensor connective of linear logic is now defined as:

{{Definition| title=multiplicative connectives|
If <math>x</math> and <math>y</math> are facts in a phase space, we define
* <math>\one = \{1\}\orth</math>;
* <math>\bot = \one\orth</math>;
* the tensor <math>x\tens y</math> to be the fact <math>(x\cdot y)\biorth</math>;
* the par connective is the de Morgan dual of the tensor: <math>x\parr y = (x\orth \tens y\orth)\orth</math>;
* the linear arrow is just <math>x\limp y = (x\tens y\orth)\orth</math>.
}}

Note that by unfolding the definition of <math>\limp</math>, we have the following, "intuitive" definition of <math>x\limp y</math>:

{{Lemma|
If <math>x</math> and <math>y</math> are facts, we have <math>a\in x\limp y</math> iff <math>\forall b\in x,\,a\cdot b\in y</math>
}}

{{Proof|
easy exercise. }}

Readers familiar with realisability will appreciate...

{{Remark|
Some people say that this idea of orthogonality was implicitly present in Tait's proof of strong normalisation. More recently, Jean-Louis Krivine and Alexandre Miquel have used the idea explicitly to do realisability...}}

===Properties===

All the expected properties hold:

{{Lemma|
* The operations <math>\tens</math>, <math>\parr</math>, <math>\plus</math> and <math>\with</math> are commutative and associative,
* They have respectively <math>\one</math>, <math>\bot</math>, <math>\zero</math> and <math>\top</math> for neutral element,
* <math>\zero</math> is absorbant for <math>\tens</math>,
* <math>\top</math> is absorbant for <math>\parr</math>,
* <math>\tens</math> distributes over <math>\plus</math>,
* <math>\parr</math> distributes over <math>\with</math>.
}}

===Exponentials===

{{Definition|title=Exponentials|
Write <math>I</math> for the set of idempotents of a phase space: <math>I=\{a\ |\ a\cdot a=a\}</math>. We put:
# <math>\oc x = (x\cap I\cap \one)\biorth</math>,
# <math>\wn x = (x\orth\cap I\cap\one)\orth</math>.
}}

This definition captures precisely the intuition behind the exponentials:
* we need to have contraction, hence we restrict to indempotents in <math>x</math>,
* and weakening, hence we restrict to <math>\one</math>.
Since <math>I</math> isn't necessarily a fact, we then take the biorthogonal to get a fact...

==Completeness==

==The Rest==

Template:Proof

2009-03-24T13:03:50Z

Samuel Mimram:

<div style="margin-left: 0em; border-left: dotted 1px #ccc; padding-left: .5em">
<em>Proof.</em>&emsp;{{{1}}}
</div>

Template:Proof

2009-03-24T09:39:13Z

Samuel Mimram: More coherent proof style

<div style="margin-left: 0em; border-left: double 4px #ccc; padding-left: .5em">
<em>Proof.</em>&emsp;{{{1}}}
</div>

Template:Environment

2009-03-24T09:38:19Z

Samuel Mimram: More visible environments

'''{{{name}}}''' {{#ifeq: {{{title|defaultString}}} | defaultString | | ({{{title}}}) }}<br />
<div style="margin-left: 0em; border-left: solid 1px #ccc; padding-left: .5em">
{{{content}}}<br />
</div>

Phase semantics

2009-03-24T09:34:36Z

Samuel Mimram: /* Closure operators */

==Introduction==

The semantics given by phase spaces is a kind of "formula and provability semantics", and is thus quite different in spirit from the more usual denotational semantics of linear logic. (Those are rather some "formulas and ''proofs'' semantics".)

--- probably a whole lot more of blabla to put here... ---

==Preliminaries: relation and closure operators==

Part of the structure obtained from phase semantics works in a very general framework and relies solely on the notion of relation between two sets.

===Relations and operators on subsets===

The starting point of phase semantics is the notion of ''duality''. The structure needed to talk about duality is very simple: one just needs a relation <math>R</math> between two sets <math>X</math> and <math>Y</math>. Using standard mathematical practice, we can write either <math>(a,b) \in R</math> or <math>a\mathrel{R} b</math> to say that <math>a\in X</math> and <math>b\in Y</math> are related.

{{Definition|
If <math>R\subseteq X\times Y</math> is a relation, we write <math>R^\sim\subseteq Y\times X</math> for the converse relation: <math>(b,a)\in R^\sim</math> iff <math>(a,b)\in R</math>.
}}

Such a relation yields three interesting operators sending subsets of <math>X</math> to subsets of <math>Y</math>:

{{Definition|
Let <math>R\subseteq X\times Y</math> be a relation, define the operators <math>\langle R\rangle</math>, <math>[R]</math> and <math>\_^R</math> taking subsets of <math>X</math> to subsets of <math>Y</math> as follows:
# <math>b\in\langle R\rangle(x)</math> iff <math>\exists a\in X,\ (a,b)\in R \land a\in x</math>
# <math>b\in[R](x)</math> iff <math>\forall a\in X,\ (a,b)\in R \implies a\in x</math>
# <math>b\in x^R</math> iff <math>\forall a\in x, (a,b)\in R</math>
}}

The operator <math>\langle R\rangle</math> is usually called the ''direct image'' of the relation, <math>[R]</math> is sometimes called the ''universal image'' of the relation.

It is trivial to check that <math>\langle R\rangle</math> and <math>[R]</math> are covariant (increasing for the <math>\subseteq</math> relation) while <math>\_^R</math> is contravariant (decreasing for the <math>\subseteq</math> relation). More interesting:

{{Lemma|title=Galois Connections|
# <math>\langle R\rangle</math> is right-adjoint to <math>[R^\sim]</math>: for any <math>x\subseteq X</math> and <math>y\subseteq Y</math>, we have <math>[R^\sim]y \subseteq x</math> iff <math>y\subseteq \langle R\rangle(x)</math>
# we have <math>y\subseteq x^R</math> iff <math>x\subseteq y^{R^\sim}</math>
}}

This implies directly that <math>\langle R\rangle</math> commutes with arbitrary unions and <math>[R]</math> commutes with arbitrary intersections. (And in fact, any operator commuting with arbitrary unions (resp. intersections) is of the form <math>\langle R\rangle</math> (resp. <math>[R]</math>).

{{Remark|the operator <math>\_^R</math> sends unions to intersections because <math>\_^R : \mathcal{P}(X) \to \mathcal{P}(Y)^\mathrm{op}</math> is right adjoint to <math>\_^{R^\sim} : \mathcal{P}(Y)^{\mathrm{op}} \to \mathcal{P}(X)</math>...}}

===Closure operators===

{{Definition|
A closure operator on <math>\mathcal{P}(X)</math> is an monotonic increasing operator <math>P</math> on the subsets of <math>X</math> which satisfies:
# for all <math>x\subseteq X</math>, we have <math>x\subseteq P(x)</math>
# for all <math>x\subseteq X</math>, we have <math>P(P(x))\subseteq P(x)</math>
}}

Closure operators are quite common in mathematics and computer science. They correspond exactly to the notion of ''monad'' on a preorder...

It follows directly from the definition that for any closure operator <math>P</math>, the image <math>P(x)</math> is a fixed point of <math>P</math>. Moreover:
{{Lemma|
<math>P(x)</math> is the smallest fixed point of <math>P</math> containing <math>x</math>.
}}

One other important property is the following:

{{Lemma|
Write <math>\mathcal{F}(P) = \{x\ |\ P(x)\subseteq x\}</math> for the collection of fixed points of a closure operator <math>P</math>. We have that <math>\left(\mathcal{F}(P),\bigcap\right)</math> is a complete inf-lattice.
}}

{{Remark|
A closure operator is in fact determined by its set of fixed points: we have <math>P(x) = \bigcup \{ y\ |\ y\in\mathcal{F}(P),\,y\subseteq x\}</math>}}

Since any complete inf-lattice is automatically a complete sup-lattice, <math>\mathcal{F}(P)</math> is also a complete sup-lattice. However, the sup operation isn't given by plain union:

{{Lemma|
If <math>P</math> is a closure operator on <math>\mathcal{P}(X)</math>, and if <math>(x_i)_{i\in I}</math> is a (possibly infinite) family of subsets of <math>X</math>, we write <math>\bigvee_{i\in I} x_i = P\left(\bigcup_{i\in I} x_i\right)</math>.

We have <math>\left(\mathcal{F}(P),\bigcap,\bigvee\right)</math> is a complete lattice.
}}

{{Proof|
easy.
}}

A rather direct consequence of the Galois connections of the previous section is:

{{Lemma|
The operator and <math>\langle R\rangle \circ [R^\sim]</math> and the operator <math>x\mapsto {x^R}^{R^\sim}</math> are closures.
}}

A last trivial lemma:

{{Lemma|
We have <math>x^R = {{x^R}^{R^\sim}}^{R}</math>.

As a consequence, a subset <math>x\subseteq X</math> is in <math>\mathcal{F}({\_^R}^{R^\sim})</math> iff it is of the form <math>y^{R^\sim}</math>.
}}

{{Remark|everything gets a little simpler when <math>R</math> is a symmetric relation on <math>X</math>.}}

==Phase Semantics==

===Phase spaces===

{{Definition|title=monoid|
A monoid is simply a set <math>X</math> equipped with a binary operation <math>\_\cdot\_</math> s.t.:
# the operation is associative
# there is a neutral element <math>1\in X</math>
The monoid is ''commutative'' when the binary operation is commutative.
}}

{{Definition|title=Phase space|
A phase space is given by:
# a commutative monoid <math>(X,1,\cdot)</math>,
# together with a subset <math>\Bot\subseteq X</math>.
The elements of <math>X</math> are called ''phases''.

We write <math>\bot</math> for the relation <math>\{(a,b)\ |\ a\cdot b \in \Bot\}</math>. This relation is symmetric.

A ''fact'' in a phase space is simply a fixed point for the closure operator <math>x\mapsto x\biorth</math>.
}}

Thanks to the preliminary work, we have:

{{Corollary|
The set of facts of a phase space is a complete lattice where:
# <math>\bigwedge_{i\in I} x_i</math> is simply <math>\bigcap_{i\in I} x_i</math>,
# <math>\bigvee_{i\in I} x_i</math> is <math>\left(\bigcup_{i\in I} x_i\right)\biorth</math>.
}}

===Additive connectives===

The previous corollary makes the following definition correct:

{{Definition|title=additive connectives|
If <math>(X,1,\cdot,\Bot)</math> is a phase space, we define the following facts and operations on facts:
# <math>\top = X = \emptyset\orth</math>
# <math>\zero = \emptyset\biorth = X\orth</math>
# <math>x\with y = x\cap y</math>
# <math>x\plus y = (x\cup y)\biorth</math>
}}

Once again, the next lemma follows from previous observations:

{{Lemma|title=additive de Morgan laws|
We have
# <math>\zero\orth = \top</math>
# <math>\top\orth = \zero</math>
# <math>(x\with y)\orth = x\orth \plus y\orth</math>
# <math>(x\plus y)\orth = x\orth \with y\orth</math>
}}

===Multiplicative connectives===

In order to define the multiplicative connectives, we actually need to use the monoid structure of our phase space. One interpretation that is reminiscent in phase semantics is that our spaces are collections of ''tests'' / programs / proofs / ''strategies'' that can interact with each other. The result of the interaction between <math>a</math> and <math>b</math> is simply <math>a\cdot b</math>.

The set <math>\Bot</math> can be thought of as the set of "good" things, and we thus have <math>a\in x\orth</math> iff "<math>a</math> interacts correctly with all the elements of <math>x</math>".

{{Definition|
If <math>x</math> and <math>y</math> are two subsets of a phase space, we write <math>x\cdot y</math> for the set <math>\{a\cdot b\ |\ a\in x, b\in y\}</math>.
}}
Thus <math>x\cdot y</math> contains all the possible interactions between one element of <math>x</math> and one element of <math>y</math>.

The tensor connective of linear logic is now defined as:

{{Definition| title=multiplicative connectives|
If <math>x</math> and <math>y</math> are facts in a phase space, we define
* <math>\one = \{1\}\orth</math>;
* <math>\bot = \one\orth</math>;
* the tensor <math>x\tens y</math> to be the fact <math>(x\cdot y)\biorth</math>;
* the par connective is the de Morgan dual of the tensor: <math>x\parr y = (x\orth \tens y\orth)\orth</math>;
* the linear arrow is just <math>x\limp y = (x\tens y\orth)\orth</math>.
}}

Note that by unfolding the definition of <math>\limp</math>, we have the following, "intuitive" definition of <math>x\limp y</math>:

{{Lemma|
If <math>x</math> and <math>y</math> are facts, we have <math>a\in x\limp y</math> iff <math>\forall b\in x,\,a\cdot b\in y</math>
}}

{{Proof|
easy exercise. }}

Readers familiar with realisability will appreciate...

{{Remark|
Some people say that this idea of orthogonality was implicitly present in Tait's proof of strong normalisation. More recently, Jean-Louis Krivine and Alexandre Miquel have used the idea explicitly to do realisability...}}

===Properties===

All the expected properties hold:

{{Lemma|
* The operations <math>\tens</math>, <math>\parr</math>, <math>\plus</math> and <math>\with</math> are commutative and associative,
* They have respectively <math>\one</math>, <math>\bot</math>, <math>\zero</math> and <math>\top</math> for neutral element,
* <math>\zero</math> is absorbant for <math>\tens</math>,
* <math>\top</math> is absorbant for <math>\parr</math>,
* <math>\tens</math> distributes over <math>\plus</math>,
* <math>\parr</math> distributes over <math>\with</math>.
}}

===Exponentials===

{{Definition|title=Exponentials|
Write <math>I</math> for the set of idempotents of a phase space: <math>I=\{a\ |\ a\cdot a=a\}</math>. We put:
# <math>\oc x = (x\cap I\cap \one)\biorth</math>,
# <math>\wn x = (x\orth\cap I\cap\one)\orth</math>.
}}

This definition captures precisely the intuition behind the exponentials:
* we need to have contraction, hence we restrict to indempotents in <math>x</math>,
* and weakening, hence we restrict to <math>\one</math>.
Since <math>I</math> isn't necessarily a fact, we then take the biorthogonal to get a fact...

==Completeness==

==The Rest==

Main Page

2009-03-24T09:33:45Z

Samuel Mimram:

== Contents ==

* An [[introduction]] to linear logic
* Syntax
** [[Sequent calculus]]
** [[Intuitionistic linear logic]]
** [[Fragment|Fragments]]
** Proof-nets
** Translations of [[Translations of classical logic|classical]] and [[Translations of intuitionistic logic|intuitionistic]] logics
* [[Semantics]]
** [[Coherent semantics]]
** [[Phase semantics]]
** [[Categorical semantics]]
** [[Relational semantics]]
** [[Geometry of interaction]]
** [[Game semantics]]
* [[Light linear logics]]

== Getting started ==

* Please read the [[recommendations]] before edition in this wiki.
* Consult the [http://meta.wikimedia.org/wiki/Help:Contents User's Guide] for information on using the wiki software.
* Available LaTeX macros are listed on the [[LLWiki LaTeX Style]] page.
* You can use the [[sandbox]] for tests.
* [[Special:Wantedpages|Wanted pages]].
* [http://perso.ens-lyon.fr/olivier.laurent/llwiki.html Technical information] about this wiki.

Main Page

2009-03-24T09:19:34Z

Samuel Mimram: /* Getting started */

== Contents ==

* An [[introduction]] to linear logic
* Syntax
** [[Sequent calculus]]
** [[Intuitionistic linear logic]]
** [[Fragment|Fragments]]
** Proof-nets
** Translations of [[Translations of classical logic|classical]] and [[Translations of intuitionistic logic|intuitionistic]] logics
* [[Semantics]]
** [[Coherent semantics]]
** [[Phase semantics]]
** [[Categorical semantics]]
** [[Relational semantics]]
** [[Geometry of interaction]]
** [[Game semantics]]
* [[Light linear logics]]

== Getting started ==

Please read the [[recommendations]] before edition in this wiki.

Consult the [http://meta.wikimedia.org/wiki/Help:Contents User's Guide] for information on using the wiki software.

Available LaTeX macros are listed on the [[LLWiki LaTeX Style]] page.

You can use the [[sandbox]] for tests.

[http://perso.ens-lyon.fr/olivier.laurent/llwiki.html Technical information] about this wiki.

Categorical semantics

2009-03-23T19:14:38Z

Samuel Mimram: /* Modeling ILL */

Categorical semantics

2009-03-23T19:14:03Z

Samuel Mimram: /* Modeling ILL */

Categorical semantics

2009-03-23T19:13:26Z

Samuel Mimram: /* Modeling ILL */

Categorical semantics

2009-03-23T19:09:21Z

Samuel Mimram: /* Modeling ILL */

Categorical semantics

2009-03-23T19:07:58Z

Samuel Mimram: /* Modeling ILL */

LLL

2009-03-23T18:59:45Z

Samuel Mimram: Redirecting to Light linear logics

#REDIRECT [[Light linear logics]]

Talk:Sequent calculus

2009-03-23T18:55:59Z

Samuel Mimram: /* Equivalences */

== Equivalences ==

Equivalences might deserve a specific page (maybe merged with [[isomorphism]]s and [[equiprovability]]?).

This is also redundant with the principles described in [[semantics]].

We might imagine a page or some pages giving a collection of valid principles of linear logic (with appropriate proofs) and specifying which ones correspond to implications, equivalences or isomorphisms.

-- [[User:Olivier Laurent|Olivier Laurent]] 10:39, 15 March 2009 (UTC)

*-autonomous category

2009-03-23T18:55:25Z

Samuel Mimram: Redirecting to Categorical semantics#*-autonomous categories

#REDIRECT [[Categorical semantics#*-autonomous categories]]

MLL

2009-03-23T18:53:42Z

Samuel Mimram: Redirecting to Fragment

#REDIRECT [[Fragment]]

ILL

2009-03-23T18:52:51Z

Samuel Mimram: Redirecting to Intuitionistic linear logic

#REDIRECT [[Intuitionistic linear logic]]

Categorical semantics

2009-03-23T18:50:12Z

Samuel Mimram: /* Modeling ILL */

Categorical semantics

2009-03-23T18:47:27Z

Samuel Mimram: /* Modeling IMLL */

Categorical semantics

2009-03-23T18:46:52Z

Samuel Mimram: /* Modeling the additives */

Categorical semantics

2009-03-23T18:44:42Z

Samuel Mimram: /* Other categorical models */

Categorical semantics

2009-03-23T18:43:04Z

Samuel Mimram: