Relational semantics

Revision as of 06:35, 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 $\mathbf{Rel}$ whose objects are sets, and such that $\mathbf{Rel}(X,Y)=\mathcal P(X\times Y)$ . Composition is the ordinary composition of relations: given $s\in\mathbf{Rel}(X,Y)$ and $t\in\mathbf{Rel}(Y,Z)$ , one sets

$t\circ s=\set{(a,c)\in X\times Z}{\exists b\in Y\ (a,b)\in s\ \text{and}\ (b,c)\in t}$

and the identity morphism is the diagonal relation $\mathsf{Id}_X=\set{(a,a)}{a\in X}$ .

An isomorphism in the category $\mathbf{Rel}$ is a relation which is a bijection, as easily checked.

Monoidal structure

The tensor product is the usual cartesian product $X\tens Y=X\times Y$ . It is a bifunctor: given $s_i\in\mathbf{Rel}(X_i,Y_i)$ (for $i = 1,2$ ), one sets $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}$ . The unit of this monoidal functor is $\one=\{*\}$ where $*$ is an arbitrary element.

For defining a monoidal category, it is not sufficient to provide the definition of the tensor product functor $\tens$ and its unit $\one$ , one has also to provide natural isomorphisms $\lambda_X\in\mathbf{Rel}(\one\tens X,X)$ , $\rho_X\in\mathbf{Rel}(X\tens\one,X)$ (left and right neutrality of $\one$ for $\tens$ ) and $\alpha_{X,Y,Z}\in\mathbf{Rel}((X\tens Y)\tens Z,X\tens(Y\tens Z))$ (associativity of $\tens$ ). All these isomorphisms have to satisfy a number of commutations. In the present case, they are defined in the obvious way.

This monoidal category $(\mathbf{Rel},\tens,\one,\lambda,\rho)$ is symmetric, meaning that it is endowed with an additional natural isomorphism $\sigma_{X,Y}\in\mathbf{Rel}(X\tens Y,Y\tens X)$ , 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) $\mathbf{Rel}$ is the tuple $(\mathbf{Rel},\tens,\one,\lambda,\rho,\sigma)$ .

@@ Line 8: / Line 8: @@
 sets
-<math>t\circ s=\set{(a,c)\in X\times Z}{\exists b\in Y\ (a,b)\in s\ \text{and}\ (b,c)\in t}</math>.
+<math>t\circ s=\set{(a,c)\in X\times Z}{\exists b\in Y\ (a,b)\in s\ \text{and}\ (b,c)\in t}</math>
+and the identity morphism is the diagonal relation <math>\mathsf{Id}_X=\set{(a,a)}{a\in X}</math>.
+An isomorphism in the category <math>\mathbf{Rel}</math> is a relation which is a bijection, as easily checked.
+==== Monoidal structure ====
+The tensor product is the usual cartesian product <math>X\tens Y=X\times Y</math>. 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.
+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>,
+<math>\rho_X\in\mathbf{Rel}(X\tens\one,X)</math> (left and right neutrality of <math>\one</math> for <math>\tens</math>) and <math>\alpha_{X,Y,Z}\in\mathbf{Rel}((X\tens Y)\tens Z,X\tens(Y\tens Z))</math> (associativity of <math>\tens</math>). All these isomorphisms have to satisfy a number of commutations. In the present case, they are defined in the obvious way.
+This monoidal category <math>(\mathbf{Rel},\tens,\one,\lambda,\rho)</math> is symmetric, meaning that it is endowed with an additional natural isomorphism <math>\sigma_{X,Y}\in\mathbf{Rel}(X\tens Y,Y\tens X)</math>, 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) <math>\mathbf{Rel}</math> is the tuple <math>(\mathbf{Rel},\tens,\one,\lambda,\rho,\sigma)</math>.

Relational semantics

Revision as of 06:35, 16 March 2009