Relational semantics - Revision history

Giulio Guerrieri: Added k \in \Nat in the definition of the interpretation of a derivation whose last rule is promotion.

2023-02-08T14:28:49Z

Added k \in \Nat in the definition of the interpretation of a derivation whose last rule is promotion.

Lionel Vaux: use llwiki.sty notations for the powerset and the set of finite multisets

2009-06-10T19:51:32Z

use llwiki.sty notations for the powerset and the set of finite multisets

Lionel Vaux: /* Interpretation of propositional linear logic (LL_0) */ Use \VdotsRule to denote prooftrees

2009-06-10T19:48:58Z

‎Interpretation of propositional linear logic (LL_0): Use \VdotsRule to denote prooftrees

Lionel Vaux: /* Interpretation of propositional linear logic (LL_0) */ fixed bullet list

2009-06-10T09:51:20Z

‎Interpretation of propositional linear logic (LL_0): fixed bullet list

Lionel Vaux: use llwiki.sty macro \set for sets

2009-06-10T09:45:44Z

use llwiki.sty macro \set for sets

Olivier Laurent: /* Interpretation of first order propositional linear logic (LL_0) */ no first order here

2009-05-24T20:42:55Z

‎Interpretation of first order propositional linear logic (LL_0): no first order here

Lionel Vaux: /* Relational semantics */ Interpretation of first order propositional linear logic

2009-05-23T19:44:11Z

‎Relational semantics: Interpretation of first order propositional linear logic

Lionel Vaux: /* Monoidal structure */ redundancy

2009-05-02T21:56:40Z

‎Monoidal structure: redundancy

Thomas Ehrhard: /* Additives */

2009-03-23T20:20:16Z

‎Additives

Thomas Ehrhard: /* Exponentials */

2009-03-23T20:19:29Z

‎Exponentials

@@ Line 123: / Line 123: @@
 \VdotsRule{ \rho }{ \vdash \Gamma, B }
 \LabelRule{ \with }
-\BinRule{ \vdash, \Gamma, A \with B }
+\BinRule{ \vdash \Gamma, A \with B }
 \DisplayProof} = \set{(\gamma,(1,a))}{(\gamma,a)\in\sem\pi} \cup \set{(\gamma,(2,b))}{(\gamma,b)\in\sem\rho}
 </math>
@@ Line 165: / Line 165: @@
 \DisplayProof} = \set{
 \left(\sum_{i=1}^k m_1^i,\ldots,\sum_{i=1}^k m_n^i,[b_1,\ldots,b_k]\right)}
-{\forall i,\ (m_1^i,\ldots,m_n^i,b_i)\in\sem\pi}
+{k \in \mathbb{N} \ \text{and} \ \forall 1 \leq i \leq k,\ (m_1^i,\ldots,m_n^i,b_i)\in\sem\pi}
 </math>

@@ Line 5: / Line 5: @@
 === 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
+It is the category <math>\mathbf{Rel}</math> whose objects are sets, and such that <math>\mathbf{Rel}(X,Y)=\powerset{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>.
@@ Line 45: / Line 45: @@
 * <math>\web{A\tens B}=\web{A\parr B}=\web A\times\web B</math>;
 * <math>\web{A\with B}=\web{A\plus B}=(\{1\}\times\web A)\cup(\{2\}\times\web B)</math>;
-* <math>\web{\oc A}=\web{\wn A}=\mathcal M_f(\web A)</math>.
+* <math>\web{\oc A}=\web{\wn A}=\finmulset{\web A}</math>.
 We then interpret the proofs of <math>LL_0</math> as follows: with each proof

@@ Line 58: / Line 58: @@
 *: <math>
 \sem{
-\AxRule{ \pi }
+\AxRule{}
-\UnaRule{ \vdash \Gamma, A }
+\VdotsRule{ \pi }{ \vdash \Gamma, A }
-\AxRule{ \rho }
+\AxRule{}
-\UnaRule{ \vdash \Delta, A\orth }
+\VdotsRule{ \rho }{ \vdash \Delta, A\orth }
 \LabelRule{ \rulename{cut} }
 \BinRule{ \vdash \Gamma, \Delta }
@@ Line 69: / Line 69: @@
 *: <math>
 \sem{
-\AxRule{ \pi }
+\AxRule{}
-\UnaRule{ \vdash \Gamma, A }
+\VdotsRule{ \pi }{ \vdash \Gamma, A }
-\AxRule{ \rho }
+\AxRule{}
-\UnaRule{ \vdash \Delta, B }
+\VdotsRule{ \rho }{ \vdash \Delta, B }
 \LabelRule{ \tens }
 \BinRule{ \vdash \Gamma, \Delta, A \tens B }
@@ Line 79: / Line 79: @@
 *: <math>
 \sem{
-\AxRule{ \pi }
+\AxRule{ }
-\UnaRule{ \vdash \Gamma, A, B }
+\VdotsRule{ \pi }{ \vdash \Gamma, A, B }
 \LabelRule{ \parr }
 \UnaRule{ \vdash \Gamma, A \parr B }
@@ Line 93: / Line 93: @@
 *: <math>
 \sem{
-\AxRule{ \pi }
+\AxRule{}
-\UnaRule{ \vdash \Gamma }
+\VdotsRule{ \pi }{ \vdash \Gamma }
 \LabelRule{ \bot }
 \UnaRule{ \vdash \Gamma, \bot }
@@ Line 102: / Line 102: @@
 *: <math>
 \sem{
-\AxRule{ \pi }
+\AxRule{}
-\UnaRule{ \vdash \Gamma, A }
+\VdotsRule{ \pi }{ \vdash \Gamma, A }
 \LabelRule{ \plus_1 }
 \UnaRule{ \vdash \Gamma, A \plus B }
@@ Line 110: / Line 110: @@
 *: <math>
 \sem{
-\AxRule{ \pi }
+\AxRule{}
-\UnaRule{ \vdash \Gamma, B }
+\VdotsRule{ \pi }{ \vdash \Gamma, B }
 \LabelRule{ \plus_2 }
 \UnaRule{ \vdash \Gamma, A \plus B }
@@ Line 118: / Line 118: @@
 *: <math>
 \sem{
-\AxRule{ \pi }
+\AxRule{}
-\UnaRule{ \vdash \Gamma, A }
+\VdotsRule{ \pi }{ \vdash \Gamma, A }
-\AxRule{ \rho }
+\AxRule{}
-\UnaRule{ \vdash \Gamma, B }
+\VdotsRule{ \rho }{ \vdash \Gamma, B }
 \LabelRule{ \with }
 \BinRule{ \vdash, \Gamma, A \with B }
@@ Line 135: / Line 135: @@
 *: <math>
 \sem{
-\AxRule{ \pi }
+\AxRule{}
-\UnaRule{ \vdash \Gamma, A }
+\VdotsRule{ \pi }{ \vdash \Gamma, A }
 \LabelRule{ d }
 \UnaRule{ \vdash \Gamma, \wn A }
@@ Line 143: / Line 143: @@
 *: <math>
 \sem{
-\AxRule{ \pi }
+\AxRule{}
-\UnaRule{ \vdash \Gamma }
+\VdotsRule{ \pi }{ \vdash \Gamma }
 \LabelRule{ w }
 \UnaRule{ \vdash \Gamma, \wn A }
@@ Line 151: / Line 151: @@
 *: <math>
 \sem{
-\AxRule{ \pi }
+\AxRule{}
-\UnaRule{ \vdash \Gamma, \wn A, \wn A }
+\VdotsRule{ \pi }{ \vdash \Gamma, \wn A, \wn A }
 \LabelRule{ c }
 \UnaRule{ \vdash \Gamma, \wn A }
@@ Line 159: / Line 159: @@
 *: <math>
 \sem{
-\AxRule{ \pi }
+\AxRule{}
-\UnaRule{ \vdash \wn A_1,\ldots,\wn A_n,B }
+\VdotsRule{ \pi }{ \vdash \wn A_1,\ldots,\wn A_n,B }
 \LabelRule{ \oc }
 \UnaRule{ \vdash \wn A_1,\ldots,\wn A_n,\oc B }

@@ Line 108: / Line 108: @@
 \DisplayProof} = \set{(\gamma,(1,a))}{(\gamma,a)\in\sem\pi}
 </math>
-:* <math>
+*: <math>
 \sem{
 \AxRule{ \pi }
@@ Line 116: / Line 116: @@
 \DisplayProof} = \set{(\gamma,(2,b))}{(\gamma,b)\in\sem\pi}
 </math>
-:* <math>
+*: <math>
 \sem{
 \AxRule{ \pi }
@@ Line 126: / Line 126: @@
 \DisplayProof} = \set{(\gamma,(1,a))}{(\gamma,a)\in\sem\pi} \cup \set{(\gamma,(2,b))}{(\gamma,b)\in\sem\rho}
 </math>
-:* <math>
+*: <math>
 \sem{
 \LabelRule{ \top }
@@ Line 141: / Line 141: @@
 \DisplayProof} = \set{(\gamma,[a])}{(\gamma,a)\in\sem\pi}
 </math>
-:* <math>
+*: <math>
 \sem{
 \AxRule{ \pi }

@@ Line 54: / Line 54: @@
 \LabelRule{ \rulename{axiom} }
 \NulRule{ \vdash A\orth, A }
-\DisplayProof}=\{(a,a);\ a\in\web A\}
+\DisplayProof}=\set{(a,a)}{a\in\web A}
 </math>
 *: <math>
@@ Line 64: / Line 64: @@
 \LabelRule{ \rulename{cut} }
 \BinRule{ \vdash \Gamma, \Delta }
-\DisplayProof} = \left\{(\gamma,\delta);\ \exists a\in\web A,\ (\gamma,a)\in\sem\pi\land(\delta,a)\in\sem\rho\right\}
+\DisplayProof} = \set{(\gamma,\delta)}{\exists a\in\web A,\ (\gamma,a)\in\sem\pi\land(\delta,a)\in\sem\rho}
 </math>
 * Multiplicative group:
@@ Line 75: / Line 75: @@
 \LabelRule{ \tens }
 \BinRule{ \vdash \Gamma, \Delta, A \tens B }
-\DisplayProof} = \left\{(\gamma,\delta,a,b);\ (\gamma,a)\in\sem\pi\land(\delta,b)\in\sem\rho\right\}
+\DisplayProof} = \set{(\gamma,\delta,a,b)}{(\gamma,a)\in\sem\pi\land(\delta,b)\in\sem\rho}
 </math>
 *: <math>
@@ Line 83: / Line 83: @@
 \LabelRule{ \parr }
 \UnaRule{ \vdash \Gamma, A \parr B }
-\DisplayProof} =  \left\{(\gamma,(a,b));\ (\gamma,a,b)\in\sem\pi\right\}
+\DisplayProof} =  \set{(\gamma,(a,b))}{(\gamma,a,b)\in\sem\pi}
 </math>
 *: <math>
@@ Line 97: / Line 97: @@
 \LabelRule{ \bot }
 \UnaRule{ \vdash \Gamma, \bot }
-\DisplayProof} = \{ (\gamma,*);\ \gamma\in\sem\pi\}
+\DisplayProof} = \set{(\gamma,*)}{\gamma\in\sem\pi}
 </math>
 * Additive group:
@@ Line 106: / Line 106: @@
 \LabelRule{ \plus_1 }
 \UnaRule{ \vdash \Gamma, A \plus B }
-\DisplayProof} = \{ (\gamma,(1,a));\ (\gamma,a)\in\sem\pi\}
+\DisplayProof} = \set{(\gamma,(1,a))}{(\gamma,a)\in\sem\pi}
 </math>
 :* <math>
@@ Line 114: / Line 114: @@
 \LabelRule{ \plus_2 }
 \UnaRule{ \vdash \Gamma, A \plus B }
-\DisplayProof} = \{ (\gamma,(2,b));\ (\gamma,b)\in\sem\pi\}
+\DisplayProof} = \set{(\gamma,(2,b))}{(\gamma,b)\in\sem\pi}
 </math>
 :* <math>
@@ Line 124: / Line 124: @@
 \LabelRule{ \with }
 \BinRule{ \vdash, \Gamma, A \with B }
-\DisplayProof} = \{ (\gamma,(1,a));\ (\gamma,a)\in\sem\pi\}\cup \{ (\gamma,(2,b));\ (\gamma,b)\in\sem\rho\}
+\DisplayProof} = \set{(\gamma,(1,a))}{(\gamma,a)\in\sem\pi} \cup \set{(\gamma,(2,b))}{(\gamma,b)\in\sem\rho}
 </math>
 :* <math>
@@ Line 139: / Line 139: @@
 \LabelRule{ d }
 \UnaRule{ \vdash \Gamma, \wn A }
-\DisplayProof} = \{ (\gamma,[a]);\ (\gamma,a)\in\sem\pi\}
+\DisplayProof} = \set{(\gamma,[a])}{(\gamma,a)\in\sem\pi}
 </math>
 :* <math>
@@ Line 147: / Line 147: @@
 \LabelRule{ w }
 \UnaRule{ \vdash \Gamma, \wn A }
-\DisplayProof} =  \{ (\gamma,[]);\ \gamma\in\sem\pi\}
+\DisplayProof} =  \set{(\gamma,[])}{\gamma\in\sem\pi}
 </math>
 *: <math>
@@ Line 155: / Line 155: @@
 \LabelRule{ c }
 \UnaRule{ \vdash \Gamma, \wn A }
-\DisplayProof} =  \{ (\gamma,m+n);\ (\gamma,m,n)\in\sem\pi\}
+\DisplayProof} =  \set{(\gamma,m+n)}{(\gamma,m,n)\in\sem\pi}
 </math>
 *: <math>
@@ Line 163: / Line 163: @@
 \LabelRule{ \oc }
 \UnaRule{ \vdash \wn A_1,\ldots,\wn A_n,\oc B }
-\DisplayProof} = \left\{
+\DisplayProof} = \set{
-\left(\sum_{i=1}^k m_1^i,\ldots,\sum_{i=1}^k m_n^i,[b_1,\ldots,b_k]\right);
+\left(\sum_{i=1}^k m_1^i,\ldots,\sum_{i=1}^k m_n^i,[b_1,\ldots,b_k]\right)}
-\ \forall i,\ (m_1^i,\ldots,m_n^i,b_i)\in\sem\pi\right\}
+{\forall i,\ (m_1^i,\ldots,m_n^i,b_i)\in\sem\pi}
 </math>

@@ Line 35: / Line 35: @@
 * 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>
-=== Interpretation of first order propositional linear logic (<math>LL_0</math>) ===
+=== Interpretation of propositional linear logic (<math>LL_0</math>) ===
 The structure described above gives rise to the following interpretation of

← Older revision		Revision as of 19:44, 23 May 2009
Line 34:		Line 34:
	* 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 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>		* 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>
		+
		+	=== Interpretation of first order propositional linear logic (<math>LL_0</math>) ===
		+
		+	The structure described above gives rise to the following interpretation of
		+	formulas and proofs of linear logic.
		+
		+	For all propositional variable <math>X</math>, fix a set <math>\web X</math>.
		+	Then with each formula <math>A</math>, we associate a set <math>\web A</math> as follows:
		+	* <math>\web{A\orth}=\web A</math>;
		+	* <math>\web{A\tens B}=\web{A\parr B}=\web A\times\web B</math>;
		+	* <math>\web{A\with B}=\web{A\plus B}=(\{1\}\times\web A)\cup(\{2\}\times\web B)</math>;
		+	* <math>\web{\oc A}=\web{\wn A}=\mathcal M_f(\web A)</math>.
		+
		+	We then interpret the proofs of <math>LL_0</math> as follows: with each proof
		+	<math>\pi</math> of sequent <math>\vdash A_1,\ldots,A_n</math>, we associate a
		+	subset <math>\sem\pi\subseteq\web{A_1}\times\cdots\times\web{A_n}</math>.
		+	* Identity group:
		+	*: <math>\sem{
		+	\LabelRule{ \rulename{axiom} }
		+	\NulRule{ \vdash A\orth, A }
		+	\DisplayProof}=\{(a,a);\ a\in\web A\}
		+	</math>
		+	*: <math>
		+	\sem{
		+	\AxRule{ \pi }
		+	\UnaRule{ \vdash \Gamma, A }
		+	\AxRule{ \rho }
		+	\UnaRule{ \vdash \Delta, A\orth }
		+	\LabelRule{ \rulename{cut} }
		+	\BinRule{ \vdash \Gamma, \Delta }
		+	\DisplayProof} = \left\{(\gamma,\delta);\ \exists a\in\web A,\ (\gamma,a)\in\sem\pi\land(\delta,a)\in\sem\rho\right\}
		+	</math>
		+	* Multiplicative group:
		+	*: <math>
		+	\sem{
		+	\AxRule{ \pi }
		+	\UnaRule{ \vdash \Gamma, A }
		+	\AxRule{ \rho }
		+	\UnaRule{ \vdash \Delta, B }
		+	\LabelRule{ \tens }
		+	\BinRule{ \vdash \Gamma, \Delta, A \tens B }
		+	\DisplayProof} = \left\{(\gamma,\delta,a,b);\ (\gamma,a)\in\sem\pi\land(\delta,b)\in\sem\rho\right\}
		+	</math>
		+	*: <math>
		+	\sem{
		+	\AxRule{ \pi }
		+	\UnaRule{ \vdash \Gamma, A, B }
		+	\LabelRule{ \parr }
		+	\UnaRule{ \vdash \Gamma, A \parr B }
		+	\DisplayProof} = \left\{(\gamma,(a,b));\ (\gamma,a,b)\in\sem\pi\right\}
		+	</math>
		+	*: <math>
		+	\sem{
		+	\LabelRule{ \one }
		+	\NulRule{ \vdash \one }
		+	\DisplayProof} = \{ * \}
		+	</math>
		+	*: <math>
		+	\sem{
		+	\AxRule{ \pi }
		+	\UnaRule{ \vdash \Gamma }
		+	\LabelRule{ \bot }
		+	\UnaRule{ \vdash \Gamma, \bot }
		+	\DisplayProof} = \{ (\gamma,*);\ \gamma\in\sem\pi\}
		+	</math>
		+	* Additive group:
		+	*: <math>
		+	\sem{
		+	\AxRule{ \pi }
		+	\UnaRule{ \vdash \Gamma, A }
		+	\LabelRule{ \plus_1 }
		+	\UnaRule{ \vdash \Gamma, A \plus B }
		+	\DisplayProof} = \{ (\gamma,(1,a));\ (\gamma,a)\in\sem\pi\}
		+	</math>
		+	:* <math>
		+	\sem{
		+	\AxRule{ \pi }
		+	\UnaRule{ \vdash \Gamma, B }
		+	\LabelRule{ \plus_2 }
		+	\UnaRule{ \vdash \Gamma, A \plus B }
		+	\DisplayProof} = \{ (\gamma,(2,b));\ (\gamma,b)\in\sem\pi\}
		+	</math>
		+	:* <math>
		+	\sem{
		+	\AxRule{ \pi }
		+	\UnaRule{ \vdash \Gamma, A }
		+	\AxRule{ \rho }
		+	\UnaRule{ \vdash \Gamma, B }
		+	\LabelRule{ \with }
		+	\BinRule{ \vdash, \Gamma, A \with B }
		+	\DisplayProof} = \{ (\gamma,(1,a));\ (\gamma,a)\in\sem\pi\}\cup \{ (\gamma,(2,b));\ (\gamma,b)\in\sem\rho\}
		+	</math>
		+	:* <math>
		+	\sem{
		+	\LabelRule{ \top }
		+	\NulRule{ \vdash \Gamma, \top }
		+	\DisplayProof} = \emptyset
		+	</math>
		+	* Exponential group:
		+	*: <math>
		+	\sem{
		+	\AxRule{ \pi }
		+	\UnaRule{ \vdash \Gamma, A }
		+	\LabelRule{ d }
		+	\UnaRule{ \vdash \Gamma, \wn A }
		+	\DisplayProof} = \{ (\gamma,[a]);\ (\gamma,a)\in\sem\pi\}
		+	</math>
		+	:* <math>
		+	\sem{
		+	\AxRule{ \pi }
		+	\UnaRule{ \vdash \Gamma }
		+	\LabelRule{ w }
		+	\UnaRule{ \vdash \Gamma, \wn A }
		+	\DisplayProof} = \{ (\gamma,[]);\ \gamma\in\sem\pi\}
		+	</math>
		+	*: <math>
		+	\sem{
		+	\AxRule{ \pi }
		+	\UnaRule{ \vdash \Gamma, \wn A, \wn A }
		+	\LabelRule{ c }
		+	\UnaRule{ \vdash \Gamma, \wn A }
		+	\DisplayProof} = \{ (\gamma,m+n);\ (\gamma,m,n)\in\sem\pi\}
		+	</math>
		+	*: <math>
		+	\sem{
		+	\AxRule{ \pi }
		+	\UnaRule{ \vdash \wn A_1,\ldots,\wn A_n,B }
		+	\LabelRule{ \oc }
		+	\UnaRule{ \vdash \wn A_1,\ldots,\wn A_n,\oc B }
		+	\DisplayProof} = \left\{
		+	\left(\sum_{i=1}^k m_1^i,\ldots,\sum_{i=1}^k m_n^i,[b_1,\ldots,b_k]\right);
		+	\ \forall i,\ (m_1^i,\ldots,m_n^i,b_i)\in\sem\pi\right\}
		+	</math>
		+
		+	{{Theorem\|If proof <math>\pi'</math> is obtained from <math>\pi</math> by eliminating a cut,
		+	then <math>\sem\pi=\sem{\pi'}</math>.}}

@@ Line 17: / Line 17: @@
 <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.
+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>.
 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>.

@@ Line 27: / Line 27: @@
 ==== 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>.
+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 ====

← Older revision		Revision as of 20:19, 23 March 2009
Line 24:		Line 24:

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