# Categorical semantics

Jump to: navigation, search

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 (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: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.

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