Semantics - Revision history

Olivier Laurent: Reorganized page

2013-04-25T19:58:44Z

Reorganized page

Olivier Laurent: Removed isomorphisms

2013-04-25T19:51:24Z

Removed isomorphisms

Lionel Vaux at 13:54, 6 September 2012

2012-09-06T13:54:41Z

Olivier Laurent: notation for isomorphismes \cong instead of \sim

2009-10-19T08:45:35Z

notation for isomorphismes \cong instead of \sim

Olivier Laurent: /* Additive structure */ diagonal

2009-03-15T10:51:04Z

‎Additive structure: diagonal

Laurent Regnier: use of latex arrays for improving the presentation

2009-03-08T21:21:44Z

use of latex arrays for improving the presentation

Show changes

Laurent Regnier: Creation of the page from the section "Main properties" of the Coherent semantics page

2009-03-08T20:40:37Z

Creation of the page from the section "Main properties" of the Coherent semantics page

New page

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 negation ==

* <math>A\biorth = A</math>
* <math>(A\tens B)\orth\sim A\orth\parr B\orth,\qquad\one\orth = \bot</math>
* <math>(A\parr B)\orth\sim A\orth\tens B\orth,\qquad\bot\orth = \one</math>
* <math>(A\with B)\orth\sim A\orth\plus B\orth,\qquad\top\orth = \zero</math>
* <math>(A\plus B)\orth\sim A\orth\with B\orth,\qquad\zero\orth = \top</math>
* <math>(\oc A)\orth \sim \wn A\orth</math>
* <math>(\wn A)\orth \sim \oc A\orth</math>

* <math>A\limp B = A\orth\parr B</math>
* <math>A\limp B \sim B\orth A\orth</math>

== Neutrals ==

* <math>A\tens\one\sim\one\tens A\sim A</math>
* <math>A\parr\bot\sim\bot\parr A\sim A</math>
* <math>A\with\top\sim\top\with A\sim A</math>
* <math>A\plus\zero\sim\zero\plus A\sim A</math>

== Commutativity ==

* <math>A\tens B \sim B\tens A</math>
* <math>A\parr B \sim B\parr A</math>
* <math>A\with B \sim B\with A</math>
* <math>A\plus B \sim B\plus A</math>

== Associativity ==

* <math>(A\tens B)\tens C \sim A\tens(B\tens C)</math>
* <math>(A\parr B)\parr C \sim A\parr(B\parr C)</math>
* <math>(A\with B)\with C \sim A\with(B\with C)</math>
* <math>(A\plus B)\plus C \sim A\plus(B\plus C)</math>

== Multiplicative semi-distributivity ==

* <math>A\tens(B\parr C)\longrightarrow (A\tens B)\parr C</math>

== Multiplicative-additive distributivity ==

* <math>A\tens(B\plus C)\sim (A\tens B)\plus(A\tens C),\qquad A\tens\zero\sim\zero</math>
* <math>A\parr(B\with C)\sim (A\parr B)\with(A\parr C),\qquad A\parr\top\sim\top</math>

== Additive structure ==

* <math>A\with B\longrightarrow A,\qquad A\with B\longrightarrow B</math>
* <math>(C\limp A)\with(C\limp B)\longrightarrow C\limp(A\with B)</math>
* <math>A\longrightarrow A\plus B,\qquad B\longrightarrow A\plus B</math>
* <math>(A\limp C)\with(B\limp C)\longrightarrow (A\plus B)\limp C</math>

== Exponential structure ==

* ''Dereliction'': <math>\oc A\longrightarrow A,\qquad A\longrightarrow\wn A</math>
* ''Weakening'': <math>\oc A\longrightarrow 1, \qquad \bot\longrightarrow \wn A</math>
* ''Contraction'': <math>\oc A\longrightarrow \oc A\tens\oc A,\qquad \wn A\parr\wn A\longrightarrow \wn A</math>
* ''Digging'': <math>\oc A\longrightarrow \oc\oc A,\qquad \wn\wn A\longrightarrow \wn A</math>

== Monoidality of exponential ==

* <math>\oc A\tens\oc B\longrightarrow\oc(A\tens B),\qquad \one\longrightarrow\oc\one</math>

== The exponential isomorphism ==

* <math>\oc(A\with B)\sim \oc A\tens\oc B,\qquad \oc\top\sim\one</math>
* <math>\wn(A\plus B)\sim \wn A\parr\wn B,\qquad \wn\zero\sim\bot</math>

← Older revision		Revision as of 19:58, 25 April 2013
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.

		+	* [[Coherent semantics]]
		+	* [[Phase semantics]]
		+	* [[Categorical semantics]]
		+	* [[Relational semantics]]
		+	* [[Finiteness semantics]]
		+	* [[Geometry of interaction]]
		+	* [[Game semantics]]

−	== Multiplicative semi-distributivity ==	+	[[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.
−
−	<math>
−	\begin{array}{rcl}
−	A\tens(B\parr C) &\longrightarrow& (A\tens B)\parr C\\
−	\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>

@@ 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.
 == Multiplicative semi-distributivity ==
@@ Line 55: / Line 7: @@
 \begin{array}{rcl}
   A\tens(B\parr C) &\longrightarrow& (A\tens B)\parr C\\
 \end{array}
 </math>
@@ Line 100: / Line 41: @@
   \oc A\tens\oc B &\longrightarrow& \oc(A\tens B) &\quad&
   \one &\longrightarrow& \oc\one\\
 \end{array}
 </math>

← Older revision		Revision as of 13:54, 6 September 2012
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. 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 ==		== Linear negation ==

@@ Line 6: / Line 6: @@
 \begin{array}{rclcrcl}
   A\biorth &=& A\\
-  (A\tens B)\orth &\sim& A\orth\parr B\orth &\quad& \one\orth  &\sim& \bot\\
+  (A\tens B)\orth &\cong& A\orth\parr B\orth &\quad& \one\orth  &\cong& \bot\\
-  (A\parr B)\orth &\sim& A\orth\tens B\orth &\quad& \bot\orth  &\sim& \one\\
+  (A\parr B)\orth &\cong& A\orth\tens B\orth &\quad& \bot\orth  &\cong& \one\\
-  (A\with B)\orth &\sim& A\orth\plus B\orth &\quad& \top\orth  &\sim& \zero\\
+  (A\with B)\orth &\cong& A\orth\plus B\orth &\quad& \top\orth  &\cong& \zero\\
-  (A\plus B)\orth &\sim& A\orth\with B\orth &\quad& \zero\orth &\sim& \top\\
+  (A\plus B)\orth &\cong& A\orth\with B\orth &\quad& \zero\orth &\cong& \top\\
-  (\oc A)\orth &\sim& \wn A\orth\\
+  (\oc A)\orth &\cong& \wn A\orth\\
-  (\wn A)\orth &\sim& \oc A\orth\\[1ex]
+  (\wn A)\orth &\cong& \oc A\orth\\[1ex]
-  A\limp B &\sim& A\orth\parr B\\
+  A\limp B &\cong& A\orth\parr B\\
-  A\limp B &\sim& B\orth\limp A\orth\\
+  A\limp B &\cong& B\orth\limp A\orth\\
 \end{array}
 </math>
@@ Line 21: / Line 21: @@
 <math>
 \begin{array}{rcl}
-  A\tens\one  &\sim& \one\tens A\sim A\\
+  A\tens\one  &\cong& \one\tens A\cong A\\
-  A\parr\bot  &\sim& \bot\parr A\sim A\\
+  A\parr\bot  &\cong& \bot\parr A\cong A\\
-  A\with\top  &\sim& \top\with A\sim A\\
+  A\with\top  &\cong& \top\with A\cong A\\
-  A\plus\zero &\sim&\zero\plus A\sim A\\
+  A\plus\zero &\cong&\zero\plus A\cong A\\
 \end{array}
 </math>
@@ Line 32: / Line 32: @@
 <math>
 \begin{array}{rcl}
-  A\tens B &\sim& B\tens A\\
+  A\tens B &\cong& B\tens A\\
-  A\parr B &\sim& B\parr A\\
+  A\parr B &\cong& B\parr A\\
-  A\with B &\sim& B\with A\\
+  A\with B &\cong& B\with A\\
-  A\plus B &\sim& B\plus A\\
+  A\plus B &\cong& B\plus A\\
 \end{array}
 </math>
@@ Line 43: / Line 43: @@
 <math>
 \begin{array}{rcl}
-  (A\tens B)\tens C &\sim& A\tens(B\tens C)\\
+  (A\tens B)\tens C &\cong& A\tens(B\tens C)\\
-  (A\parr B)\parr C &\sim& A\parr(B\parr C)\\
+  (A\parr B)\parr C &\cong& A\parr(B\parr C)\\
-  (A\with B)\with C &\sim& A\with(B\with C)\\
+  (A\with B)\with C &\cong& A\with(B\with C)\\
-  (A\plus B)\plus C &\sim& A\plus(B\plus C)\\
+  (A\plus B)\plus C &\cong& A\plus(B\plus C)\\
 \end{array}
 </math>
@@ Line 62: / Line 62: @@
 <math>
 \begin{array}{rclcrcl}
-  A\tens(B\plus C) &\sim& (A\tens B)\plus(A\tens C) &\quad&
+  A\tens(B\plus C) &\cong& (A\tens B)\plus(A\tens C) &\quad&
-  A\tens\zero &\sim& \zero\\
+  A\tens\zero &\cong& \zero\\
-  A\parr(B\with C) &\sim& (A\parr B)\with(A\parr C) &\quad&
+  A\parr(B\with C) &\cong& (A\parr B)\with(A\parr C) &\quad&
-  A\parr\top &\sim& \top\\
+  A\parr\top &\cong& \top\\
 \end{array}
 </math>
@@ Line 107: / Line 107: @@
 <math>
 \begin{array}{rclcrcl}
-  \oc(A\with B) &\sim& \oc A\tens\oc B &\quad& \oc\top &\sim& \one\\
+  \oc(A\with B) &\cong& \oc A\tens\oc B &\quad& \oc\top &\cong& \one\\
-  \wn(A\plus B) &\sim& \wn A\parr\wn B &\quad& \wn\zero &\sim& \bot\\
+  \wn(A\plus B) &\cong& \wn A\parr\wn B &\quad& \wn\zero &\cong& \bot\\
 \end{array}
 </math>

@@ Line 75: / Line 75: @@
   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\plus B &\quad& B \longrightarrow A\plus B\\
   (A\limp C)\with(B\limp C) &\longrightarrow& (A\plus B)\limp C\\
 \end{array}
 </math>