Relational semantics
(→Monoidal structure) |
(→Monoidal structure) |
||
Line 16: | Line 16: | ||
==== Monoidal structure ==== |
==== Monoidal structure ==== |
||
− | The tensor product is the usual cartesian product of sets <math>X\tens Y=X\times Y</math> (which <em>is not</em> a cartesian product in the category <math>\mathbf{Rel}</math> in the categorical sense). It is a bifunctor: given <math>s_i\in\mathbf{Rel}(X_i,Y_i)</math> (for <math>i=1,2</math>), one sets <math>s_1\tens s_2=\set{((a_1,a_2),(b_1,b_2))}{(a_i,b_i)\in s_i\ \text{for}\ i=1,2}</math>. The unit of this monoidal functor is <math>\one=\{*\}</math> where <math>*</math> is an arbitrary element. |
+ | The tensor product is the usual cartesian product of sets <math>X\tens Y=X\times Y</math> (which <em>is not</em> a cartesian product in the category <math>\mathbf{Rel}</math> in the categorical sense). It is a bifunctor: given <math>s_i\in\mathbf{Rel}(X_i,Y_i)</math> (for <math>i=1,2</math>), one sets <math>s_1\tens s_2=\set{((a_1,a_2),(b_1,b_2))}{(a_i,b_i)\in s_i\ \text{for}\ i=1,2}</math>. The unit of this tensor product is <math>\one=\{*\}</math> where <math>*</math> is an arbitrary element. |
For defining a monoidal category, it is not sufficient to provide the definition of the tensor product functor <math>\tens</math> and its unit <math>\one</math>, one has also to provide natural isomorphisms <math>\lambda_X\in\mathbf{Rel}(\one\tens X,X)</math>, |
For defining a monoidal category, it is not sufficient to provide the definition of the tensor product functor <math>\tens</math> and its unit <math>\one</math>, one has also to provide natural isomorphisms <math>\lambda_X\in\mathbf{Rel}(\one\tens X,X)</math>, |
Revision as of 14:07, 16 March 2009
Relational semantics
This is the simplest denotational semantics of linear logic. It consists in interpreting a formula A as a set A * and a proof π of A as a subset π * of A * .
The category of sets and relations
It is the category whose objects are sets, and such that . Composition is the ordinary composition of relations: given and , one sets
and the identity morphism is the diagonal relation .
An isomorphism in the category is a relation which is a bijection, as easily checked.
Monoidal structure
The tensor product is the usual cartesian product of sets (which is not a cartesian product in the category in the categorical sense). It is a bifunctor: given (for i = 1,2), one sets . The unit of this tensor product is where * is an arbitrary element.
For defining a monoidal category, it is not sufficient to provide the definition of the tensor product functor and its unit , one has also to provide natural isomorphisms , (left and right neutrality of for ) and (associativity of ). All these isomorphisms have to satisfy a number of commutations. In the present case, they are defined in the obvious way.
This monoidal category is symmetric, meaning that it is endowed with an additional natural isomorphism , also subject to some commutations. Here, again, this isomorphism is defined in the obvious way (symmetry of the cartesian product). So, to be precise, the SMCC (symmetric monoidal closed category) is the tuple , but we shall simply denote it as for simplicity.
The SMCC is closed. This means that, given any object X of (a set), the functor (from to ) admits a right adjoint (from to ).