Categorical semantics

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(Compact closed categories)
(Compact closed categories)
Line 240: Line 240:
   
 
=== Compact closed categories ===
 
=== 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|
 
{{Definition|title=Dual objects|
Line 269: Line 265:
 
{{Lemma|
 
{{Lemma|
 
Two left (resp. right) duals of a same object <math>B</math> are necessarily isomorphic.
 
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.
 
}}
 
}}
   

Revision as of 15:52, 25 March 2009

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

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

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

Contents

Basic category theory recalled

Definition (Category)


Definition (Functor)


Definition (Natural transformation)


Definition (Adjunction)


Definition (Monad)


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.

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.

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.

Modeling negation

*-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.

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

Other categorical models

Lafont categories

Seely categories

Linear categories

Properties of categorical models

The Kleisli category

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