Relational semantics

From LLWiki
(Difference between revisions)
Jump to: navigation, search
(Monoidal structure)
m (Added k \in \Nat in the definition of the interpretation of a derivation whose last rule is promotion.)
 
(21 intermediate revisions by 3 users not shown)
Line 5: Line 5:
 
=== The category of sets and relations ===
 
=== 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.
 
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 ====
 
==== 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>,
 
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.
 
<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>.}}

Latest revision as of 15:28, 8 February 2023

Contents

[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 Xis 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 (LL0)

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 LL0 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'}.

Personal tools