Semantics
From LLWiki
(Difference between revisions)
Lionel Vaux (Talk | contribs) |
(Removed isomorphisms) |
||
| Line 1: | Line 1: | ||
Linear Logic has numerous semantics some of which are described in details in the next sections. We give here an overview of the common properties that one may find in most of these models. We will denote by <math>A\longrightarrow B</math> the fact that there is a canonical morphism from <math>A</math> to <math>B</math> and by <math>A\cong B</math> the fact that there is a canonical isomorphism between <math>A</math> and <math>B</math>. By "canonical" we mean that these (iso)morphisms are natural transformations. |
Linear Logic has numerous semantics some of which are described in details in the next sections. We give here an overview of the common properties that one may find in most of these models. We will denote by <math>A\longrightarrow B</math> the fact that there is a canonical morphism from <math>A</math> to <math>B</math> and by <math>A\cong B</math> the fact that there is a canonical isomorphism between <math>A</math> and <math>B</math>. By "canonical" we mean that these (iso)morphisms are natural transformations. |
||
| − | == Linear negation == |
||
| − | |||
| − | <math> |
||
| − | \begin{array}{rclcrcl} |
||
| − | A\biorth &=& A\\ |
||
| − | (A\tens B)\orth &\cong& A\orth\parr B\orth &\quad& \one\orth &\cong& \bot\\ |
||
| − | (A\parr B)\orth &\cong& A\orth\tens B\orth &\quad& \bot\orth &\cong& \one\\ |
||
| − | (A\with B)\orth &\cong& A\orth\plus B\orth &\quad& \top\orth &\cong& \zero\\ |
||
| − | (A\plus B)\orth &\cong& A\orth\with B\orth &\quad& \zero\orth &\cong& \top\\ |
||
| − | (\oc A)\orth &\cong& \wn A\orth\\ |
||
| − | (\wn A)\orth &\cong& \oc A\orth\\[1ex] |
||
| − | A\limp B &\cong& A\orth\parr B\\ |
||
| − | A\limp B &\cong& B\orth\limp A\orth\\ |
||
| − | \end{array} |
||
| − | </math> |
||
| − | |||
| − | == Neutrals == |
||
| − | |||
| − | <math> |
||
| − | \begin{array}{rcl} |
||
| − | A\tens\one &\cong& \one\tens A\cong A\\ |
||
| − | A\parr\bot &\cong& \bot\parr A\cong A\\ |
||
| − | A\with\top &\cong& \top\with A\cong A\\ |
||
| − | A\plus\zero &\cong&\zero\plus A\cong A\\ |
||
| − | \end{array} |
||
| − | </math> |
||
| − | |||
| − | == Commutativity == |
||
| − | |||
| − | <math> |
||
| − | \begin{array}{rcl} |
||
| − | A\tens B &\cong& B\tens A\\ |
||
| − | A\parr B &\cong& B\parr A\\ |
||
| − | A\with B &\cong& B\with A\\ |
||
| − | A\plus B &\cong& B\plus A\\ |
||
| − | \end{array} |
||
| − | </math> |
||
| − | |||
| − | == Associativity == |
||
| − | |||
| − | <math> |
||
| − | \begin{array}{rcl} |
||
| − | (A\tens B)\tens C &\cong& A\tens(B\tens C)\\ |
||
| − | (A\parr B)\parr C &\cong& A\parr(B\parr C)\\ |
||
| − | (A\with B)\with C &\cong& A\with(B\with C)\\ |
||
| − | (A\plus B)\plus C &\cong& A\plus(B\plus C)\\ |
||
| − | \end{array} |
||
| − | </math> |
||
== Multiplicative semi-distributivity == |
== Multiplicative semi-distributivity == |
||
| Line 55: | Line 7: | ||
\begin{array}{rcl} |
\begin{array}{rcl} |
||
A\tens(B\parr C) &\longrightarrow& (A\tens B)\parr C\\ |
A\tens(B\parr C) &\longrightarrow& (A\tens B)\parr C\\ |
||
| − | \end{array} |
||
| − | </math> |
||
| − | |||
| − | == Multiplicative-additive distributivity == |
||
| − | |||
| − | <math> |
||
| − | \begin{array}{rclcrcl} |
||
| − | A\tens(B\plus C) &\cong& (A\tens B)\plus(A\tens C) &\quad& |
||
| − | A\tens\zero &\cong& \zero\\ |
||
| − | A\parr(B\with C) &\cong& (A\parr B)\with(A\parr C) &\quad& |
||
| − | A\parr\top &\cong& \top\\ |
||
\end{array} |
\end{array} |
||
</math> |
</math> |
||
| Line 100: | Line 41: | ||
\oc A\tens\oc B &\longrightarrow& \oc(A\tens B) &\quad& |
\oc A\tens\oc B &\longrightarrow& \oc(A\tens B) &\quad& |
||
\one &\longrightarrow& \oc\one\\ |
\one &\longrightarrow& \oc\one\\ |
||
| − | \end{array} |
||
| − | </math> |
||
| − | |||
| − | == The exponential isomorphism == |
||
| − | |||
| − | <math> |
||
| − | \begin{array}{rclcrcl} |
||
| − | \oc(A\with B) &\cong& \oc A\tens\oc B &\quad& \oc\top &\cong& \one\\ |
||
| − | \wn(A\plus B) &\cong& \wn A\parr\wn B &\quad& \wn\zero &\cong& \bot\\ |
||
\end{array} |
\end{array} |
||
</math> |
</math> |
||
Revision as of 21:51, 25 April 2013
Linear Logic has numerous semantics some of which are described in details in the next sections. We give here an overview of the common properties that one may find in most of these models. We will denote by 
the fact that there is a canonical morphism from A to B and by 
the fact that there is a canonical isomorphism between A and B. By "canonical" we mean that these (iso)morphisms are natural transformations.
Contents |
Multiplicative semi-distributivity
Additive structure
Exponential structure
Monoidality of exponential
