Categorical semantics

Revision as of 19:14, 24 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.

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

UNIQ31f607c9a963c80-math-00000016-QINU

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

T O D O

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 $(X,π 1,π 2)$ 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

T O D O

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

T O D O

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

$(\mathcal{M},\times,\top) TODO (\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

T O D O

commute for every objects $A$ , $B$ and $C$ of $\mathcal{C}$ . The morphisms $f A, 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) \qquad \text{and} \qquad (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

T O D O

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

Definition (Monoidal adjunction)

TODO

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 (Compact closed category)

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

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

T O D O

commute.

In a compact closed category the left and right duals of an object $A$ 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

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

[0] MacLane, Saunders. Categories for the Working Mathematician. Volume 5, 1971.

[1] Melliès, Paul-André. Categorical Semantics of Linear Logic.

[2] Benton, Nick. A Mixed Linear and Non-Linear Logic: Proofs, Terms and Models.. CSL'94. journal. Volume 933, 1995.

[1]

[2]

[3]

Categorical semantics

Revision as of 19:14, 24 March 2009

Contents

Basic category theory recalled

Modeling IMLL

Modeling the additives

Modeling ILL

Modeling negation

*-autonomous categories

Compact closed categories

Other categorical models

Lafont categories

Seely categories

Linear categories

Properties of categorical models

The Kleisli category

References

Views

Personal tools

Navigation

Search

Tools

@@ Line 46: / Line 46: @@
 </math>
 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
-:<math></math>
+:<math>
-commute.
+\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.
 }}