Semantics
From LLWiki
(Difference between revisions)
m (notation for isomorphismes \cong instead of \sim) |
(Reorganized page) |
||
| (2 intermediate revisions by 2 users not shown) | |||
| 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\sim 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. |
| − | == Linear negation == |
+ | * [[Coherent semantics]] |
| + | * [[Phase semantics]] |
||
| + | * [[Categorical semantics]] |
||
| + | * [[Relational semantics]] |
||
| + | * [[Finiteness semantics]] |
||
| + | * [[Geometry of interaction]] |
||
| + | * [[Game semantics]] |
||
| − | <math> |
+ | [[Provable formulas|Common properties]] may be found 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. |
| − | \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 == |
||
| − | |||
| − | <math> |
||
| − | \begin{array}{rcl} |
||
| − | 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} |
||
| − | </math> |
||
| − | |||
| − | == Additive structure == |
||
| − | |||
| − | <math> |
||
| − | \begin{array}{rcl} |
||
| − | A\with B \longrightarrow A &\quad& A\with B \longrightarrow B\\ |
||
| − | (C\limp A)\with(C\limp B) &\longrightarrow& C\limp(A\with B)\\ |
||
| − | A &\longrightarrow& A\with A\\ |
||
| − | A \longrightarrow A\plus B &\quad& B \longrightarrow A\plus B\\ |
||
| − | (A\limp C)\with(B\limp C) &\longrightarrow& (A\plus B)\limp C\\ |
||
| − | A\plus A &\longrightarrow& A\\ |
||
| − | \end{array} |
||
| − | </math> |
||
| − | |||
| − | == Exponential structure == |
||
| − | |||
| − | <math> |
||
| − | \begin{array}{rclcrcl} |
||
| − | \oc A &\longrightarrow& A &\quad& A&\longrightarrow&\wn A\\ |
||
| − | \oc A &\longrightarrow& 1 &\quad& \bot &\longrightarrow& \wn A\\ |
||
| − | \oc A &\longrightarrow& \oc A\tens\oc A &\quad& |
||
| − | \wn A\parr\wn A &\longrightarrow& \wn A\\ |
||
| − | \oc A &\longrightarrow& \oc\oc A &\quad& \wn\wn A &\longrightarrow& \wn A\\ |
||
| − | \end{array} |
||
| − | </math> |
||
| − | |||
| − | == Monoidality of exponential == |
||
| − | |||
| − | <math> |
||
| − | \begin{array}{rclcrcl} |
||
| − | \oc A\tens\oc B &\longrightarrow& \oc(A\tens B) &\quad& |
||
| − | \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} |
||
| − | </math> |
||
Latest revision as of 20:58, 25 April 2013
Linear Logic has numerous semantics some of which are described in details in the next sections.
- Coherent semantics
- Phase semantics
- Categorical semantics
- Relational semantics
- Finiteness semantics
- Geometry of interaction
- Game semantics
Common properties may be found 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.
