Relational semantics

Revision as of 19:23, 23 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 of sets $X\tens Y=X\times Y$ (which is not a cartesian product in the category $\mathbf{Rel}$ in the categorical sense). 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 tensor product 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,\alpha,\sigma)$ , but we shall simply denote it as $\mathbf{Rel}$ for simplicity.

The SMCC $\mathbf{Rel}$ is closed. This means that, given any object $X$ of $\mathbf{Rel}$ (a set), the functor $Z\mapsto Z\tens X$ (from $\mathbf{Rel}$ to $\mathbf{Rel}$ ) admits a right adjoint $Y\mapsto (X\limp Y)$ (from $\mathbf{Rel}$ to $\mathbf{Rel}$ ). In other words, for any objects $X$ and $Y$ , we are given an object $X\limp Y$ and a morphism $\mathsf{ev}_{X,Y}\in\mathbf{Rel}((X\limp Y)\tens X,Y)$ with the following universal property: for any morphism $s\in\mathbf{Rel}(Z\tens X,Y)$ , there is a unique morphism $\mathsf{fun}(s)\in\mathbf{Rel}(Z,X\limp Y)$ such that $\mathsf{ev}_{X,Y}\circ(\mathsf{fun}(s)\tens\mathsf{Id}_X)=s$ .

The definition of all these data is quite simple in $\mathbf{Rel}$ : $X\limp Y=X\times Y$ , $\mathsf{ev}_{X,Y}=\set{(((a,b),a),b)}{(a,b)\in X\times Y}$ and $\mathsf{fun}(s)=\set{(c,(a,b))}{((c,a),b)\in s}$ .

Let $\bot=\one=\{*\}$ . Then we have $\mathsf{ev}\circ\sigma:\mathbf{Rel}(X\tens(X\limp\bot),\bot)$ and hence $\eta_X=\mathsf{fun}(\mathsf{ev}\circ\sigma)\in\mathbf{Rel}(X,(X\limp\bot)\limp\bot)$ . It is clear that $\eta=\set{(a,((a,*),*))}{a\in X}$ and hence $η$ is a natural isomorphism: one says that the SMCC $\mathbf{Rel}$ is a *-autonomous category, with $\bot$ as dualizing object.

Exponentials

One defines $\oc X$ as the set of all finite multisets of elements of $X$ . Given $s\in\mathbf{Rel}(X,Y)$ , one defines $\oc s=\set{([a_1,\dots,a_n],[b_1,\dots,b_n])}{n\in\mathbb N\ \text{and}\ \forall i\ (a_i,b_i)\in s}$ where $[a_1,\dots,a_n]$ is the multiset containing $a_1,\dots,a_n$ , taking multiplicities into account. This defines a functor $\mathbf{Rel}\to\mathbf{Rel}$ , that we endow with a comonad structure as follows:

the counit, called dereliction, is the natural transformation $\mathsf d_X\in\mathbf{Rel}(\oc X,X)$ , given by $\mathsf d_X=\set{([a],a)}{a\in X}$

@@ Line 27: / Line 27: @@
 ==== Exponentials ====
-One defines <math>\oc X</math> as the set of all finite multisets of elements of <math>X</math>. Given <math>s\in\mathbf{Rel}(X,Y)</math>, one defines <math>\oc s=\set{([a_1,\dots,a_n],[b_1,\dots,b_n])}{n\in\mathbb N\ \text{and}\ \forall i\ (a_i,b_i)\in s}</math> where <math>[a_1,\dots,a_n]</math> is the multiset containing <math>a_1,\dots,a_n</math>, taking multiplicities into account. This defines a functor <math>\mathbf{Rel}\to\mathbf{Rel}</math>
+One defines <math>\oc X</math> as the set of all finite multisets of elements of <math>X</math>. Given <math>s\in\mathbf{Rel}(X,Y)</math>, one defines <math>\oc s=\set{([a_1,\dots,a_n],[b_1,\dots,b_n])}{n\in\mathbb N\ \text{and}\ \forall i\ (a_i,b_i)\in s}</math> where <math>[a_1,\dots,a_n]</math> is the multiset containing <math>a_1,\dots,a_n</math>, taking multiplicities into account. This defines a functor <math>\mathbf{Rel}\to\mathbf{Rel}</math>, that we endow with a comonad structure as follows:
+* the counit, called dereliction, is the natural transformation <math>\mathsf d_X\in\mathbf{Rel}(\oc X,X)</math>, given by <math>\mathsf d_X=\set{([a],a)}{a\in X}</math>

Relational semantics

Revision as of 19:23, 23 March 2009

Contents