Relational semantics

Latest revision as of 15:28, 8 February 2023

[edit] 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 *$ .

[edit] The category of sets and relations

It is the category $\mathbf{Rel}$ whose objects are sets, and such that $\mathbf{Rel}(X,Y)=\powerset{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.

[edit] 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}$ .

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.

[edit] Additives

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

[edit] 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{der}_X\in\mathbf{Rel}(\oc X,X)$ , given by $\mathsf{der}_X=\set{([a],a)}{a\in X}$
the comultiplication, called digging, is the natural transformation $\mathsf{digg}_X\in\mathbf{Rel}(\oc X,\oc\oc X)$ , given by $\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}$

[edit] Interpretation of propositional linear logic ( $L L 0$ )

The structure described above gives rise to the following interpretation of formulas and proofs of linear logic.

For all propositional variable $X$ , fix a set $\web X$ . Then with each formula $A$ , we associate a set $\web A$ as follows:

$\web{A\orth}=\web A$ ;
$\web{A\tens B}=\web{A\parr B}=\web A\times\web B$ ;
$\web{A\with B}=\web{A\plus B}=(\{1\}\times\web A)\cup(\{2\}\times\web B)$ ;
$\web{\oc A}=\web{\wn A}=\finmulset{\web A}$ .

We then interpret the proofs of $L L 0$ as follows: with each proof $π$ of sequent $\vdash A_1,\ldots,A_n$ , we associate a subset $\sem\pi\subseteq\web{A_1}\times\cdots\times\web{A_n}$ .

Identity group:
$\sem{ \LabelRule{ \rulename{axiom} } \NulRule{ \vdash A\orth, A } \DisplayProof}=\set{(a,a)}{a\in\web A}$
$\sem{ \AxRule{} \VdotsRule{ \pi }{ \vdash \Gamma, A } \AxRule{} \VdotsRule{ \rho }{ \vdash \Delta, A\orth } \LabelRule{ \rulename{cut} } \BinRule{ \vdash \Gamma, \Delta } \DisplayProof} = \set{(\gamma,\delta)}{\exists a\in\web A,\ (\gamma,a)\in\sem\pi\land(\delta,a)\in\sem\rho}$
Multiplicative group:
$\sem{ \AxRule{} \VdotsRule{ \pi }{ \vdash \Gamma, A } \AxRule{} \VdotsRule{ \rho }{ \vdash \Delta, B } \LabelRule{ \tens } \BinRule{ \vdash \Gamma, \Delta, A \tens B } \DisplayProof} = \set{(\gamma,\delta,a,b)}{(\gamma,a)\in\sem\pi\land(\delta,b)\in\sem\rho}$
$\sem{ \AxRule{ } \VdotsRule{ \pi }{ \vdash \Gamma, A, B } \LabelRule{ \parr } \UnaRule{ \vdash \Gamma, A \parr B } \DisplayProof} = \set{(\gamma,(a,b))}{(\gamma,a,b)\in\sem\pi}$
$\sem{ \LabelRule{ \one } \NulRule{ \vdash \one } \DisplayProof} = \{ * \}$
$\sem{ \AxRule{} \VdotsRule{ \pi }{ \vdash \Gamma } \LabelRule{ \bot } \UnaRule{ \vdash \Gamma, \bot } \DisplayProof} = \set{(\gamma,*)}{\gamma\in\sem\pi}$
Additive group:
$\sem{ \AxRule{} \VdotsRule{ \pi }{ \vdash \Gamma, A } \LabelRule{ \plus_1 } \UnaRule{ \vdash \Gamma, A \plus B } \DisplayProof} = \set{(\gamma,(1,a))}{(\gamma,a)\in\sem\pi}$
$\sem{ \AxRule{} \VdotsRule{ \pi }{ \vdash \Gamma, B } \LabelRule{ \plus_2 } \UnaRule{ \vdash \Gamma, A \plus B } \DisplayProof} = \set{(\gamma,(2,b))}{(\gamma,b)\in\sem\pi}$
$\sem{ \AxRule{} \VdotsRule{ \pi }{ \vdash \Gamma, A } \AxRule{} \VdotsRule{ \rho }{ \vdash \Gamma, B } \LabelRule{ \with } \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}$
$\sem{ \LabelRule{ \top } \NulRule{ \vdash \Gamma, \top } \DisplayProof} = \emptyset$
Exponential group:
$\sem{ \AxRule{} \VdotsRule{ \pi }{ \vdash \Gamma, A } \LabelRule{ d } \UnaRule{ \vdash \Gamma, \wn A } \DisplayProof} = \set{(\gamma,[a])}{(\gamma,a)\in\sem\pi}$
$\sem{ \AxRule{} \VdotsRule{ \pi }{ \vdash \Gamma } \LabelRule{ w } \UnaRule{ \vdash \Gamma, \wn A } \DisplayProof} = \set{(\gamma,[])}{\gamma\in\sem\pi}$
$\sem{ \AxRule{} \VdotsRule{ \pi }{ \vdash \Gamma, \wn A, \wn A } \LabelRule{ c } \UnaRule{ \vdash \Gamma, \wn A } \DisplayProof} = \set{(\gamma,m+n)}{(\gamma,m,n)\in\sem\pi}$
$\sem{ \AxRule{} \VdotsRule{ \pi }{ \vdash \wn A_1,\ldots,\wn A_n,B } \LabelRule{ \oc } \UnaRule{ \vdash \wn A_1,\ldots,\wn A_n,\oc B } \DisplayProof} = \set{ \left(\sum_{i=1}^k m_1^i,\ldots,\sum_{i=1}^k m_n^i,[b_1,\ldots,b_k]\right)} {k \in \mathbb{N} \ \text{and} \ \forall 1 \leq i \leq k,\ (m_1^i,\ldots,m_n^i,b_i)\in\sem\pi}$

Theorem

If proof $π'$ is obtained from $π$ by eliminating a cut, then $\sem\pi=\sem{\pi'}$ .

@@ 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
+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>.
-<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.
@@ Line 12: / Line 12: @@
 ==== 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>,
 <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>, 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>.
+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>
+=== Interpretation of 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}=\finmulset{\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}=\set{(a,a)}{a\in\web A}
+</math>
+*: <math>
+\sem{
+\AxRule{}
+\VdotsRule{ \pi }{ \vdash \Gamma, A }
+\AxRule{}
+\VdotsRule{ \rho }{ \vdash \Delta, A\orth }
+\LabelRule{ \rulename{cut} }
+\BinRule{ \vdash \Gamma, \Delta }
+\DisplayProof} = \set{(\gamma,\delta)}{\exists a\in\web A,\ (\gamma,a)\in\sem\pi\land(\delta,a)\in\sem\rho}
+</math>
+* Multiplicative group:
+*: <math>
+\sem{
+\AxRule{}
+\VdotsRule{ \pi }{ \vdash \Gamma, A }
+\AxRule{}
+\VdotsRule{ \rho }{ \vdash \Delta, B }
+\LabelRule{ \tens }
+\BinRule{ \vdash \Gamma, \Delta, A \tens B }
+\DisplayProof} = \set{(\gamma,\delta,a,b)}{(\gamma,a)\in\sem\pi\land(\delta,b)\in\sem\rho}
+</math>
+*: <math>
+\sem{
+\AxRule{ }
+\VdotsRule{ \pi }{ \vdash \Gamma, A, B }
+\LabelRule{ \parr }
+\UnaRule{ \vdash \Gamma, A \parr B }
+\DisplayProof} =  \set{(\gamma,(a,b))}{(\gamma,a,b)\in\sem\pi}
+</math>
+*: <math>
+\sem{
+\LabelRule{ \one }
+\NulRule{ \vdash \one }
+\DisplayProof} = \{ * \}
+</math>
+*: <math>
+\sem{
+\AxRule{}
+\VdotsRule{ \pi }{ \vdash \Gamma }
+\LabelRule{ \bot }
+\UnaRule{ \vdash \Gamma, \bot }
+\DisplayProof} = \set{(\gamma,*)}{\gamma\in\sem\pi}
+</math>
+* Additive group:
+*: <math>
+\sem{
+\AxRule{}
+\VdotsRule{ \pi }{ \vdash \Gamma, A }
+\LabelRule{ \plus_1 }
+\UnaRule{ \vdash \Gamma, A \plus B }
+\DisplayProof} = \set{(\gamma,(1,a))}{(\gamma,a)\in\sem\pi}
+</math>
+*: <math>
+\sem{
+\AxRule{}
+\VdotsRule{ \pi }{ \vdash \Gamma, B }
+\LabelRule{ \plus_2 }
+\UnaRule{ \vdash \Gamma, A \plus B }
+\DisplayProof} = \set{(\gamma,(2,b))}{(\gamma,b)\in\sem\pi}
+</math>
+*: <math>
+\sem{
+\AxRule{}
+\VdotsRule{ \pi }{ \vdash \Gamma, A }
+\AxRule{}
+\VdotsRule{ \rho }{ \vdash \Gamma, B }
+\LabelRule{ \with }
+\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>
+*: <math>
+\sem{
+\LabelRule{ \top }
+\NulRule{ \vdash \Gamma, \top }
+\DisplayProof} = \emptyset
+</math>
+* Exponential group:
+*: <math>
+\sem{
+\AxRule{}
+\VdotsRule{ \pi }{ \vdash \Gamma, A }
+\LabelRule{ d }
+\UnaRule{ \vdash \Gamma, \wn A }
+\DisplayProof} = \set{(\gamma,[a])}{(\gamma,a)\in\sem\pi}
+</math>
+*: <math>
+\sem{
+\AxRule{}
+\VdotsRule{ \pi }{ \vdash \Gamma }
+\LabelRule{ w }
+\UnaRule{ \vdash \Gamma, \wn A }
+\DisplayProof} =  \set{(\gamma,[])}{\gamma\in\sem\pi}
+</math>
+*: <math>
+\sem{
+\AxRule{}
+\VdotsRule{ \pi }{ \vdash \Gamma, \wn A, \wn A }
+\LabelRule{ c }
+\UnaRule{ \vdash \Gamma, \wn A }
+\DisplayProof} =  \set{(\gamma,m+n)}{(\gamma,m,n)\in\sem\pi}
+</math>
+*: <math>
+\sem{
+\AxRule{}
+\VdotsRule{ \pi }{ \vdash \wn A_1,\ldots,\wn A_n,B }
+\LabelRule{ \oc }
+\UnaRule{ \vdash \wn A_1,\ldots,\wn A_n,\oc B }
+\DisplayProof} = \set{
+\left(\sum_{i=1}^k m_1^i,\ldots,\sum_{i=1}^k m_n^i,[b_1,\ldots,b_k]\right)}
+{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>
-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>).
+{{Theorem|If proof <math>\pi'</math> is obtained from <math>\pi</math> by eliminating a cut,
+then <math>\sem\pi=\sem{\pi'}</math>.}}

Relational semantics

Latest revision as of 15:28, 8 February 2023

Contents

[edit] Relational semantics