Categorical semantics

From LLWiki
Revision as of 19:16, 23 March 2009 by Samuel Mimram (Talk | contribs)

Jump to: navigation, search

Constructing denotational models of linear can be a tedious work. Categorical model 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.

Contents

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

commutes,

  • for every objects A and B in \mathcal{C}, the diagrams

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

UNIQ2deb2c3e634fceef-math-00000011-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)


Definition (Monoid)


Property

Categories with products vs monoidal categories.

Modeling IMALL

Modeling negation

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.

References

  1. MacLane, Saunders. Categories for the Working Mathematician.
Personal tools