Categorical semantics

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(Modeling IALL)
(Compact closed categories)
 
(43 intermediate revisions by 2 users not shown)
Line 1: Line 1:
Constructing denotational models of linear can be a tedious work. Categorical model are useful to identify the fundamental structure of these models, and thus simplify and make more abstract the elaboration of those models.
+
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.
 
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=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|
  +
}}
  +
  +
== Overview ==
  +
  +
In order to interpret the various [[fragment]]s of linear logic, we define incrementally what structure we need in a categorical setting.
  +
  +
* The most basic underlying structure are '''symmetric monoidal categories''' which model the symmetric tensor <math>\otimes</math> and its unit <math>1</math>.
  +
* The <math>\otimes, \multimap</math> fragment ([[IMLL]]) is captured by so-called '''symmetric monoidal closed categories'''.
  +
* Upgrading to [[ILL]], that is, adding the exponential <math>\oc</math> modality to IMLL requires modelling it categorically. There are various ways to do so: using rich enough '''adjunctions''', or with an ad-hoc definition of a well-behaved comonad which leads to '''linear categories''' and close relatives.
  +
* Dealing with the additives <math>\with, \oplus</math> is quite easy, as they are plain '''cartesian product''' and '''coproduct''', usually defined through universal properties in category theory.
  +
* Retrieving <math>\parr</math>, <math>\bot</math> and <math>\wn</math> is just a matter of dualizing <math>\otimes</math>, <math>1</math> and <math>\oc</math>, thus requiring the model to be a '''*-autonomous category''' for that purpose.
   
 
== Modeling [[IMLL]] ==
 
== Modeling [[IMLL]] ==
Line 23: Line 23:
 
such that
 
such that
 
* for every objects <math>A,B,C,D</math> in <math>\mathcal{C}</math>, the diagram
 
* 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,
 
commutes,
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagrams
+
* for every objects <math>A</math> and <math>B</math> in <math>\mathcal{C}</math>, the diagram
commute.
+
:<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.
 
}}
 
}}
   
Line 32: Line 38:
 
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
 
:<math>\gamma_{A,B}:A\otimes B\to B\otimes A</math>
 
called ''braiding'', such that the two diagrams
 
called ''braiding'', such that the two diagrams
:<math></math>
+
:<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>.
 
commute for every objects <math>A</math>, <math>B</math> and <math>C</math>.
   
Line 53: Line 59:
 
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
 
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>
 
:<math>
TODO
+
\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>
 
</math>
 
commute.
 
commute.
Line 64: Line 70:
 
== Modeling the additives ==
 
== Modeling the additives ==
 
{{Definition|title=Product|
 
{{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|
 
{{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.
 
}}
 
}}
   
Line 73: Line 108:
 
}}
 
}}
   
== Modeling [[IMLL]] ==
+
== 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>.
 
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>.
Line 80: Line 115:
 
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
 
A ''linear-non linear adjunction'' is a symmetric monoidal adjunction between lax monoidal functors
 
:<math>
 
:<math>
(\mathcal{M},\times,\top) TODO (\mathcal{L},\otimes,I)
+
\xymatrix{
  +
(\mathcal{M},\times,\top)\ar@/^/[rr]^{(L,l)}&\bot&\ar@/^/[ll]^{(M,m)}(\mathcal{L},\otimes,I)
  +
}
 
</math>
 
</math>
 
in which the category <math>\mathcal{M}</math> has finite products.
 
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 ==
 
== Modeling negation ==
  +
  +
=== *-autonomous categories ===
  +
 
{{Definition|title=*-autonomous category|
 
{{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
 
Suppose that we are given a symmetric monoidal closed category <math>(\mathcal{C},\tens,I)</math> and an object <math>R</math> of <math>\mathcal{C}</math>. For every object <math>A</math>, we define a morphism
 
:<math>\partial_{A}:A\to(A\limp R)\limp R</math>
 
:<math>\partial_{A}:A\to(A\limp R)\limp R</math>
 
as follows. By applying the bijection of the adjunction defining (left) closed monoidal categories to the identity morphism <math>\mathrm{id}_{A\limp R}:A\limp R \to A\limp R</math>, we get a morphism <math>A\tens (A\limp R)\to R</math>, and thus a morphism <math>(A\limp R)\tens A\to R</math> by precomposing with the symmetry <math>\gamma_{A\limp R,A}</math>. The morphism <math>\partial_A</math> is finally obtained by applying the bijection of the adjunction defining (left) closed monoidal categories to this morphism. 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.
 
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.
  +
}}
  +
  +
{{Property|
  +
A compact closed category is a (degenerated) *-autonomous category, with the obvious duality structure. In particular, <math>(A \otimes B)^* \cong A^*\otimes B^*</math>.
  +
}}
  +
  +
{{Remark|The above isomorphism does not hold in *-autonomous categories in general. This means that models which are compact closed categories identify <math>\otimes</math> and <math>\parr</math> as well as <math>1</math> and <math>\bot</math>.}}
  +
  +
{{Proof|
  +
The dualizing object <math>R</math> is simply <math>I^*</math>.
  +
  +
For any <math>A</math>, the reverse isomorphism <math>\delta_A : (A \multimap R)\multimap R \rightarrow A</math> is constructed as follows:
  +
  +
<math>\mathcal{C}((A \multimap R)\multimap R, A) := \mathcal{C}((A \otimes I^{**})\otimes I^{**}, A) \cong \mathcal{C}((A \otimes I)\otimes I, A) \cong \mathcal{C}(A, A)</math>
  +
  +
Identity on <math>A</math> is taken as the canonical morphism required.
  +
 
}}
 
}}
   
 
== Other categorical models ==
 
== Other categorical models ==
  +
  +
=== Lafont categories ===
  +
  +
=== Seely categories ===
  +
  +
=== Linear categories ===
   
 
== Properties of categorical models ==
 
== Properties of categorical models ==

Latest revision as of 00:29, 4 October 2011

Constructing denotational models of linear can be a tedious work. Categorical semantics are useful to identify the fundamental structure of these models, and thus simplify and make more abstract the elaboration of those models.

TODO: why categories? how to extract categorical models? etc.

See [1]for a more detailed introduction to category theory. See [2]for a detailed treatment of categorical semantics of linear logic.

Contents

[edit] Basic category theory recalled

Definition (Category)


Definition (Functor)


Definition (Natural transformation)


Definition (Adjunction)


Definition (Monad)


[edit] Overview

In order to interpret the various fragments of linear logic, we define incrementally what structure we need in a categorical setting.

  • The most basic underlying structure are symmetric monoidal categories which model the symmetric tensor \otimes and its unit 1.
  • The \otimes, \multimap fragment (IMLL) is captured by so-called symmetric monoidal closed categories.
  • Upgrading to ILL, that is, adding the exponential \oc modality to IMLL requires modelling it categorically. There are various ways to do so: using rich enough adjunctions, or with an ad-hoc definition of a well-behaved comonad which leads to linear categories and close relatives.
  • Dealing with the additives \with, \oplus is quite easy, as they are plain cartesian product and coproduct, usually defined through universal properties in category theory.
  • Retrieving \parr, \bot and \wn is just a matter of dualizing \otimes, 1 and \oc, thus requiring the model to be a *-autonomous category for that purpose.

[edit] Modeling IMLL

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

Definition (Monoidal category)

A monoidal category (\mathcal{C},\otimes,I,\alpha,\lambda,\rho) is a category \mathcal{C} equipped with

  • a functor \otimes:\mathcal{C}\times\mathcal{C}\to\mathcal{C} called tensor product,
  • an object I called unit object,
  • three natural isomorphisms α, λ and ρ, called respectively associator, left unitor and right unitor, whose components are

\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

such that

  • for every objects A,B,C,D in \mathcal{C}, the diagram

\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))
}

commutes,

  • for every objects A and B in \mathcal{C}, the diagram

\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&
}

commutes.

Definition (Braided, symmetric monoidal category)

A braided monoidal category is a category together with a natural isomorphism of components

\gamma_{A,B}:A\otimes B\to B\otimes A

called braiding, such that the two diagrams


\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}}\\
}

and


\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}&\\
}

commute for every objects A, B and C.

A symmetric monoidal category is a braided monoidal category in which the braiding satisfies

\gamma_{B,A}\circ\gamma_{A,B}=A\otimes B

for every objects A and B.

Definition (Closed monoidal category)

A monoidal category (\mathcal{C},\tens,I) is left closed when for every object A, the functor

B\mapsto A\otimes B

has a right adjoint, written

B\mapsto(A\limp B)

This means that there exists a bijection

\mathcal{C}(A\tens B, C) \cong \mathcal{C}(B,A\limp C)

which is natural in B and C. Equivalently, a monoidal category is left closed when it is equipped with a left closed structure, which consists of

  • an object A\limp B,
  • a morphism \mathrm{eval}_{A,B}:A\tens (A\limp B)\to B, called left evaluation,

for every objects A and B, such that for every morphism f:A\otimes X\to B there exists a unique morphism h:X\to A\limp B making the diagram


\xymatrix{
A\tens X\ar@{.>}[d]_{A\tens h}\ar[dr]^{f}\\
A\tens(A\limp B)\ar[r]_-{\mathrm{eval}_{A,B}}&B
}

commute.

Dually, the monoidal category \mathcal{C} is right closed when the functor B\mapsto B\otimes A admits a right adjoint. The notion of right closed structure can be defined similarly.

In a symmetric monoidal category, a left closed structure induces a right closed structure and conversely, allowing us to simply speak of a closed symmetric monoidal category.

[edit] Modeling the additives

Definition (Product)

A product (X12) of two coinitial morphisms f:A\to B and g:A\to C in a category \mathcal{C} is an object X of \mathcal{C} together with two morphisms \pi_1:X\to A and \pi_2:X\to B such that there exists a unique morphism h:A\to X making the diagram


\xymatrix{
&\ar[ddl]_fA\ar@{.>}[d]_h\ar[ddr]^g&\\
&\ar[dl]^{\pi_1}X\ar[dr]_{\pi_2}&\\
B&&C
}

commute.

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

Definition (Monoid)

A monoid (M,μ,η) in a monoidal category (\mathcal{C},\tens,I) is an object M together with two morphisms

\mu:M\tens M \to M and \eta:I\to M

such that the diagrams


\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\\
}

and


\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&
}

commute.

Property

Categories with products vs monoidal categories.

[edit] Modeling ILL

Introduced in[3].

Definition (Linear-non linear (LNL) adjunction)

A linear-non linear adjunction is a symmetric monoidal adjunction between lax monoidal functors


\xymatrix{
(\mathcal{M},\times,\top)\ar@/^/[rr]^{(L,l)}&\bot&\ar@/^/[ll]^{(M,m)}(\mathcal{L},\otimes,I)
}

in which the category \mathcal{M} has finite products.

\oc=L\circ M

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

Definition (Monoidal functor)

A lax monoidal functor (F,f) between two monoidal categories (\mathcal{C},\tens,I) and (\mathcal{D},\bullet,J) consists of

  • a functor F:\mathcal{C}\to\mathcal{D} between the underlying categories,
  • a natural transformation f of components f_{A,B}:FA\bullet FB\to F(A\tens B),
  • a morphism f:J\to FI

such that the diagrams


\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))
}

and


\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)
}
and 
\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)
}

commute for every objects A, B and C of \mathcal{C}. The morphisms fA,B and f are called coherence maps.

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

Definition (Monoidal natural transformation)

Suppose that (\mathcal{C},\tens,I) and (\mathcal{D},\bullet,J) are two monoidal categories and


(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
and 
(G,g):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)

are two monoidal functors between these categories. A monoidal natural transformation \theta:(F,f)\to (G,g) between these monoidal functors is a natural transformation \theta:F\Rightarrow G between the underlying functors such that the diagrams


\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)
}
and 
\xymatrix{
  &\ar[dl]_{f}J\ar[dr]^{g}&\\
  FI\ar[rr]_{\theta_I}&&GI
}

commute for every objects A and B of \mathcal{D}.

Definition (Monoidal adjunction)

A monoidal adjunction between two monoidal functors


(F,f):(\mathcal{C},\tens,I)\Rightarrow(\mathcal{D},\bullet,J)
and 
(G,g):(\mathcal{D},\bullet,J)\Rightarrow(\mathcal{C},\tens,I)

is an adjunction between the underlying functors F and G such that the unit and the counit

\eta:\mathcal{C}\Rightarrow G\circ F and \varepsilon:F\circ G\Rightarrow\mathcal{D}

induce monoidal natural transformations between the corresponding monoidal functors.

[edit] Modeling negation

[edit] *-autonomous categories

Definition (*-autonomous category)

Suppose that we are given a symmetric monoidal closed category (\mathcal{C},\tens,I) and an object R of \mathcal{C}. For every object A, we define a morphism

\partial_{A}:A\to(A\limp R)\limp R

as follows. By applying the bijection of the adjunction defining (left) closed monoidal categories to the identity morphism \mathrm{id}_{A\limp R}:A\limp R \to A\limp R, we get a morphism A\tens (A\limp R)\to R, and thus a morphism (A\limp R)\tens A\to R by precomposing with the symmetry \gamma_{A\limp R,A}. The morphism \partial_A is finally obtained by applying the bijection of the adjunction defining (left) closed monoidal categories to this morphism. The object R is called dualizing when the morphism \partial_A is a bijection for every object A of \mathcal{C}. A symmetric monoidal closed category is *-autonomous when it admits such a dualizing object.

[edit] Compact closed categories

Definition (Dual objects)

A dual object structure (A,B,\eta,\varepsilon) in a monoidal category (\mathcal{C},\tens,I) is a pair of objects A and B together with two morphisms

\eta:I\to B\otimes A and \varepsilon:A\otimes B\to I

such that the diagrams


\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\\
}

and


\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\\
}

commute. The object A is called a left dual of B (and conversely B is a right dual of A).

Lemma

Two left (resp. right) duals of a same object B are necessarily isomorphic.

Definition (Compact closed category)

A symmetric monoidal category (\mathcal{C},\tens,I) is compact closed when every object A has a right dual A * . We write

\eta_A:I\to A^*\tens A and \varepsilon_A:A\tens A^*\to I

for the corresponding duality morphisms.

Lemma

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

Property

A compact closed category \mathcal{C} is monoidal closed, with closure defined by

\mathcal{C}(A\tens B,C)\cong\mathcal{C}(B,A^*\tens C)

Proof.  To every morphism f:A\tens B\to C, we associate a morphism \ulcorner f\urcorner:B\to A^*\tens C defined as


\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\\
}

and to every morphism g:B\to A^*\tens C, we associate a morphism \llcorner g\lrcorner:A\tens B\to C defined as


\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
}

It is easy to show that \llcorner \ulcorner f\urcorner\lrcorner=f and \ulcorner\llcorner g\lrcorner\urcorner=g from which we deduce the required bijection.

Property

A compact closed category is a (degenerated) *-autonomous category, with the obvious duality structure. In particular, (A \otimes B)^* \cong A^*\otimes B^*.

Remark: The above isomorphism does not hold in *-autonomous categories in general. This means that models which are compact closed categories identify \otimes and \parr as well as 1 and \bot.

Proof.  The dualizing object R is simply I * .

For any A, the reverse isomorphism \delta_A : (A \multimap R)\multimap R \rightarrow A is constructed as follows:

\mathcal{C}((A \multimap R)\multimap R, A) := \mathcal{C}((A \otimes I^{**})\otimes I^{**}, A) \cong \mathcal{C}((A \otimes I)\otimes I, A) \cong \mathcal{C}(A, A)

Identity on A is taken as the canonical morphism required.


[edit] Other categorical models

[edit] Lafont categories

[edit] Seely categories

[edit] Linear categories

[edit] Properties of categorical models

[edit] The Kleisli category

[edit] References

  1. MacLane, Saunders. Categories for the Working Mathematician. Volume 5, 1971.
  2. Melliès, Paul-André. Categorical Semantics of Linear Logic.
  3. Benton, Nick. A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.. CSL'94. journal. Volume 933, 1995.
Personal tools