LLWiki - User contributions [en]

Relational semantics

2009-03-23T20:20:16Z

Thomas Ehrhard: /* Additives */

== Relational semantics ==

This is the simplest denotational semantics of linear logic. It consists in interpreting a formula <math>A</math> as a set <math>A^*</math> and a proof <math>\pi</math> of <math>A</math> as a subset <math>\pi^*</math> of <math>A^*</math>.

=== The category of sets and relations ===

It is the category <math>\mathbf{Rel}</math> whose objects are sets, and such that <math>\mathbf{Rel}(X,Y)=\mathcal P(X\times Y)</math>. Composition is the ordinary composition of relations: given <math>s\in\mathbf{Rel}(X,Y)</math> and <math>t\in\mathbf{Rel}(Y,Z)</math>, one
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> 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 of sets <math>X\tens Y=X\times Y</math> (which is not 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>,
<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,\alpha,\sigma)</math>, but we shall simply denote it as <math>\mathbf{Rel}</math> for simplicity.

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

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

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

==== Additives ====

Given a family <math>(X_i)_{i\in I}</math>, let <math>\with_{i\in I}X_i=\cup_{i\in I}\{i\}\times X_i</math>. Let <math>\pi_j\in\mathbf{Rel}(\with_{i\in I}X_i,X_j)</math> given by <math>\pi_j=\set{((j,a),a)}{a\in X_j}</math>. Then <math>(\with_{i\in I}X_i,(\pi_i)_{i\in I})</math> is the cartesian product of the <math>X_i</math>s in the category <math>\mathbf{Rel}</math>.

==== 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>, that we endow with a comonad structure as follows:
* the counit, called dereliction, is the natural transformation <math>\mathsf{der}_X\in\mathbf{Rel}(\oc X,X)</math>, given by <math>\mathsf{der}_X=\set{([a],a)}{a\in X}</math>
* the comultiplication, called digging, is the natural transformation <math>\mathsf{digg}_X\in\mathbf{Rel}(\oc X,\oc\oc X)</math>, given by <math>\mathsf{digg}_X=\set{(m_1+\cdots+m_n,[m_1,\dots,m_n])}{n\in\mathbb N\ \text{and}\ m_1,\dots,m_n\in\oc X}</math>

Relational semantics

2009-03-23T20:19:29Z

Thomas Ehrhard: /* Exponentials */

== Relational semantics ==

This is the simplest denotational semantics of linear logic. It consists in interpreting a formula <math>A</math> as a set <math>A^*</math> and a proof <math>\pi</math> of <math>A</math> as a subset <math>\pi^*</math> of <math>A^*</math>.

=== The category of sets and relations ===

It is the category <math>\mathbf{Rel}</math> whose objects are sets, and such that <math>\mathbf{Rel}(X,Y)=\mathcal P(X\times Y)</math>. Composition is the ordinary composition of relations: given <math>s\in\mathbf{Rel}(X,Y)</math> and <math>t\in\mathbf{Rel}(Y,Z)</math>, one
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> 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 of sets <math>X\tens Y=X\times Y</math> (which is not 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>,
<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,\alpha,\sigma)</math>, but we shall simply denote it as <math>\mathbf{Rel}</math> for simplicity.

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

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

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

==== Additives ====

Given a family <math>(X_i)_{i\in I}</math>, let <math>\with_{i\in I}X_i=\bigcup_{i\in I}\{i\}\times X_i</math>. Let <math>\pi_j\in\mathbf{Rel}(\wiyh_{i\in I}X_i,X_j)</math> given by <math>\pi_j=\set{((j,a),a)}{a\in X_j}</math>. Then <math>(\with_{i\in I}X_i,(\pi_i)_{i\in I})</math> is the cartesian product of the <math>X_i</math>s in the category <math>\mathbf{Rel}</math>.

==== 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>, that we endow with a comonad structure as follows:
* the counit, called dereliction, is the natural transformation <math>\mathsf{der}_X\in\mathbf{Rel}(\oc X,X)</math>, given by <math>\mathsf{der}_X=\set{([a],a)}{a\in X}</math>
* the comultiplication, called digging, is the natural transformation <math>\mathsf{digg}_X\in\mathbf{Rel}(\oc X,\oc\oc X)</math>, given by <math>\mathsf{digg}_X=\set{(m_1+\cdots+m_n,[m_1,\dots,m_n])}{n\in\mathbb N\ \text{and}\ m_1,\dots,m_n\in\oc X}</math>

Relational semantics

2009-03-23T18:32:21Z

Thomas Ehrhard: /* Exponentials */

== Relational semantics ==

This is the simplest denotational semantics of linear logic. It consists in interpreting a formula <math>A</math> as a set <math>A^*</math> and a proof <math>\pi</math> of <math>A</math> as a subset <math>\pi^*</math> of <math>A^*</math>.

=== The category of sets and relations ===

It is the category <math>\mathbf{Rel}</math> whose objects are sets, and such that <math>\mathbf{Rel}(X,Y)=\mathcal P(X\times Y)</math>. Composition is the ordinary composition of relations: given <math>s\in\mathbf{Rel}(X,Y)</math> and <math>t\in\mathbf{Rel}(Y,Z)</math>, one
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> 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 of sets <math>X\tens Y=X\times Y</math> (which is not 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>,
<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,\alpha,\sigma)</math>, but we shall simply denote it as <math>\mathbf{Rel}</math> for simplicity.

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

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

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

==== 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>, that we endow with a comonad structure as follows:
* the counit, called dereliction, is the natural transformation <math>\mathsf{der}_X\in\mathbf{Rel}(\oc X,X)</math>, given by <math>\mathsf{der}_X=\set{([a],a)}{a\in X}</math>
* the comultiplication, called digging, is the natural transformation <math>\mathsf{digg}_X\in\mathbf{Rel}(\oc X,\oc\oc X)</math>, given by <math>\mathsf{digg}_X=\set{(m_1+\cdots+m_n,[m_1,\dots,m_n])}{n\in\mathbb N\ \text{and}\ m_1,\dots,m_n\in\oc X}</math>

Relational semantics

2009-03-23T18:23:58Z

Thomas Ehrhard: /* Exponentials */

== Relational semantics ==

This is the simplest denotational semantics of linear logic. It consists in interpreting a formula <math>A</math> as a set <math>A^*</math> and a proof <math>\pi</math> of <math>A</math> as a subset <math>\pi^*</math> of <math>A^*</math>.

=== The category of sets and relations ===

It is the category <math>\mathbf{Rel}</math> whose objects are sets, and such that <math>\mathbf{Rel}(X,Y)=\mathcal P(X\times Y)</math>. Composition is the ordinary composition of relations: given <math>s\in\mathbf{Rel}(X,Y)</math> and <math>t\in\mathbf{Rel}(Y,Z)</math>, one
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> 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 of sets <math>X\tens Y=X\times Y</math> (which is not 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>,
<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,\alpha,\sigma)</math>, but we shall simply denote it as <math>\mathbf{Rel}</math> for simplicity.

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

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

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

==== 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>, 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

2009-03-23T18:20:29Z

Thomas Ehrhard: /* Exponentials */

== Relational semantics ==

This is the simplest denotational semantics of linear logic. It consists in interpreting a formula <math>A</math> as a set <math>A^*</math> and a proof <math>\pi</math> of <math>A</math> as a subset <math>\pi^*</math> of <math>A^*</math>.

=== The category of sets and relations ===

It is the category <math>\mathbf{Rel}</math> whose objects are sets, and such that <math>\mathbf{Rel}(X,Y)=\mathcal P(X\times Y)</math>. Composition is the ordinary composition of relations: given <math>s\in\mathbf{Rel}(X,Y)</math> and <math>t\in\mathbf{Rel}(Y,Z)</math>, one
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> 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 of sets <math>X\tens Y=X\times Y</math> (which is not 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>,
<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,\alpha,\sigma)</math>, but we shall simply denote it as <math>\mathbf{Rel}</math> for simplicity.

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

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

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

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

Relational semantics

2009-03-23T18:16:14Z

Thomas Ehrhard: /* Exponentials */

== Relational semantics ==

This is the simplest denotational semantics of linear logic. It consists in interpreting a formula <math>A</math> as a set <math>A^*</math> and a proof <math>\pi</math> of <math>A</math> as a subset <math>\pi^*</math> of <math>A^*</math>.

=== The category of sets and relations ===

It is the category <math>\mathbf{Rel}</math> whose objects are sets, and such that <math>\mathbf{Rel}(X,Y)=\mathcal P(X\times Y)</math>. Composition is the ordinary composition of relations: given <math>s\in\mathbf{Rel}(X,Y)</math> and <math>t\in\mathbf{Rel}(Y,Z)</math>, one
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> 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 of sets <math>X\tens Y=X\times Y</math> (which is not 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>,
<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,\alpha,\sigma)</math>, but we shall simply denote it as <math>\mathbf{Rel}</math> for simplicity.

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

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

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

==== 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>.

Relational semantics

2009-03-23T18:06:12Z