Categorical semantics

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(Modeling the additives)
(Modeling IMLL)
Line 43: Line 43:
 
((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[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))
 
(A\otimes B)\otimes(C\otimes D)\ar[rr]_{\alpha_{A,B,C\otimes D}}&&A\otimes(B\otimes (C\otimes D))
}
+
}
 
</math>
 
</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 diagrams
:<math>TODO</math>
+
:<math></math>
 
commute.
 
commute.
 
}}
 
}}

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

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 diagrams
UNIQ30ed86c97d0605b8-math-00000014-QINU

commute.

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

UNIQ30ed86c97d0605b8-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

TODO

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

TODO

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

TODO

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

TODO

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

TODO

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

TODO

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

  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