Categorical semantics

Revision as of 00:26, 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.

Basic category theory recalled

Definition (Category)

Definition (Functor)

Definition (Natural transformation)

Definition (Adjunction)

Definition (Monad)

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.

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 $(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

$\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 $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)$ 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: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.

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.

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]

@@ Line 305: / Line 305: @@
 </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.}}
+{{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.
 }}

Categorical semantics

Revision as of 00:26, 4 October 2011

Contents

Basic category theory recalled

Overview

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