http://llwiki.ens-lyon.fr/mediawiki/index.php?title=Semantics&feed=atom&action=history
Semantics - Revision history
2024-03-29T04:46:39Z
Revision history for this page on the wiki
MediaWiki 1.19.20+dfsg-0+deb7u3
http://llwiki.ens-lyon.fr/mediawiki/index.php?title=Semantics&diff=580&oldid=prev
Olivier Laurent: Reorganized page
2013-04-25T19:58:44Z
<p>Reorganized page</p>
<table class='diff diff-contentalign-left'>
<col class='diff-marker' />
<col class='diff-content' />
<col class='diff-marker' />
<col class='diff-content' />
<tr valign='top'>
<td colspan='2' style="background-color: white; color:black;">← Older revision</td>
<td colspan='2' style="background-color: white; color:black;">Revision as of 19:58, 25 April 2013</td>
</tr><tr>
<td colspan="2" class="diff-lineno">Line 1:</td>
<td colspan="2" class="diff-lineno">Line 1:</td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>Linear Logic has numerous semantics some of which are described in details in the next sections<span class="diffchange diffchange-inline">. 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</span>.</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>Linear Logic has numerous semantics some of which are described in details in the next sections.</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>* [[Coherent semantics]]</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>* [[Phase semantics]]</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>* [[Categorical semantics]]</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>* [[Relational semantics]]</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>* [[Finiteness semantics]]</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>* [[Geometry of interaction]]</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>* [[Game semantics]]</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div><span class="diffchange diffchange-inline">==</span> <span class="diffchange diffchange-inline">Multiplicative</span> <span class="diffchange diffchange-inline">semi-distributivity</span> <span class="diffchange diffchange-inline">==</span></div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div><span class="diffchange diffchange-inline">[[Provable</span> <span class="diffchange diffchange-inline">formulas|Common</span> <span class="diffchange diffchange-inline">properties]]</span> <span class="diffchange diffchange-inline">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.</span></div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div><math></div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>\begin{array}{rcl}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\tens(B\parr C) &\longrightarrow& (A\tens B)\parr C\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>\end{array}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div></math></div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>== Additive structure ==</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div><math></div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>\begin{array}{rcl}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\with B \longrightarrow A &\quad& A\with B \longrightarrow B\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (C\limp A)\with(C\limp B) &\longrightarrow& C\limp(A\with B)\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A &\longrightarrow& A\with A\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A \longrightarrow A\plus B &\quad& B \longrightarrow A\plus B\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (A\limp C)\with(B\limp C) &\longrightarrow& (A\plus B)\limp C\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\plus A &\longrightarrow& A\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>\end{array}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div></math></div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>== Exponential structure ==</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div><math></div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>\begin{array}{rclcrcl}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> \oc A &\longrightarrow& A &\quad& A&\longrightarrow&\wn A\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> \oc A &\longrightarrow& 1 &\quad& \bot &\longrightarrow& \wn A\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> \oc A &\longrightarrow& \oc A\tens\oc A &\quad& </div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> \wn A\parr\wn A &\longrightarrow& \wn A\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> \oc A &\longrightarrow& \oc\oc A &\quad& \wn\wn A &\longrightarrow& \wn A\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>\end{array}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div></math></div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>== Monoidality of exponential ==</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div><math></div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>\begin{array}{rclcrcl}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> \oc A\tens\oc B &\longrightarrow& \oc(A\tens B) &\quad&</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> \one &\longrightarrow& \oc\one\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>\end{array}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div></math></div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
</table>
Olivier Laurent
http://llwiki.ens-lyon.fr/mediawiki/index.php?title=Semantics&diff=578&oldid=prev
Olivier Laurent: Removed isomorphisms
2013-04-25T19:51:24Z
<p>Removed isomorphisms</p>
<table class='diff diff-contentalign-left'>
<col class='diff-marker' />
<col class='diff-content' />
<col class='diff-marker' />
<col class='diff-content' />
<tr valign='top'>
<td colspan='2' style="background-color: white; color:black;">← Older revision</td>
<td colspan='2' style="background-color: white; color:black;">Revision as of 19:51, 25 April 2013</td>
</tr><tr>
<td colspan="2" class="diff-lineno">Line 1:</td>
<td colspan="2" class="diff-lineno">Line 1:</td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>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.</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>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.</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>== Linear negation ==</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div><math></div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>\begin{array}{rclcrcl}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\biorth &=& A\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (A\tens B)\orth &\cong& A\orth\parr B\orth &\quad& \one\orth &\cong& \bot\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (A\parr B)\orth &\cong& A\orth\tens B\orth &\quad& \bot\orth &\cong& \one\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (A\with B)\orth &\cong& A\orth\plus B\orth &\quad& \top\orth &\cong& \zero\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (A\plus B)\orth &\cong& A\orth\with B\orth &\quad& \zero\orth &\cong& \top\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (\oc A)\orth &\cong& \wn A\orth\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (\wn A)\orth &\cong& \oc A\orth\\[1ex]</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\limp B &\cong& A\orth\parr B\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\limp B &\cong& B\orth\limp A\orth\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>\end{array}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div></math></div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>== Neutrals ==</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div><math></div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>\begin{array}{rcl}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\tens\one &\cong& \one\tens A\cong A\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\parr\bot &\cong& \bot\parr A\cong A\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\with\top &\cong& \top\with A\cong A\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\plus\zero &\cong&\zero\plus A\cong A\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>\end{array}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div></math></div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>== Commutativity ==</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div><math></div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>\begin{array}{rcl}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\tens B &\cong& B\tens A\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\parr B &\cong& B\parr A\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\with B &\cong& B\with A\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\plus B &\cong& B\plus A\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>\end{array}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div></math></div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>== Associativity ==</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div><math></div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>\begin{array}{rcl}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (A\tens B)\tens C &\cong& A\tens(B\tens C)\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (A\parr B)\parr C &\cong& A\parr(B\parr C)\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (A\with B)\with C &\cong& A\with(B\with C)\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (A\plus B)\plus C &\cong& A\plus(B\plus C)\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>\end{array}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div></math></div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>== Multiplicative semi-distributivity ==</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>== Multiplicative semi-distributivity ==</div></td>
</tr>
<tr>
<td colspan="2" class="diff-lineno">Line 55:</td>
<td colspan="2" class="diff-lineno">Line 7:</td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\begin{array}{rcl}</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\begin{array}{rcl}</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div> A\tens(B\parr C) &\longrightarrow& (A\tens B)\parr C\\</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div> A\tens(B\parr C) &\longrightarrow& (A\tens B)\parr C\\</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>\end{array}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div></math></div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>== Multiplicative-additive distributivity ==</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div><math></div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>\begin{array}{rclcrcl}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\tens(B\plus C) &\cong& (A\tens B)\plus(A\tens C) &\quad&</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\tens\zero &\cong& \zero\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\parr(B\with C) &\cong& (A\parr B)\with(A\parr C) &\quad&</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\parr\top &\cong& \top\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\end{array}</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\end{array}</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div></math></div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div></math></div></td>
</tr>
<tr>
<td colspan="2" class="diff-lineno">Line 100:</td>
<td colspan="2" class="diff-lineno">Line 41:</td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div> \oc A\tens\oc B &\longrightarrow& \oc(A\tens B) &\quad&</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div> \oc A\tens\oc B &\longrightarrow& \oc(A\tens B) &\quad&</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div> \one &\longrightarrow& \oc\one\\</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div> \one &\longrightarrow& \oc\one\\</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>\end{array}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div></math></div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>== The exponential isomorphism ==</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div><math></div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>\begin{array}{rclcrcl}</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> \oc(A\with B) &\cong& \oc A\tens\oc B &\quad& \oc\top &\cong& \one\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> \wn(A\plus B) &\cong& \wn A\parr\wn B &\quad& \wn\zero &\cong& \bot\\</div></td>
<td colspan="2" class="diff-empty"> </td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\end{array}</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\end{array}</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div></math></div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div></math></div></td>
</tr>
</table>
Olivier Laurent
http://llwiki.ens-lyon.fr/mediawiki/index.php?title=Semantics&diff=574&oldid=prev
Lionel Vaux at 13:54, 6 September 2012
2012-09-06T13:54:41Z
<p></p>
<table class='diff diff-contentalign-left'>
<col class='diff-marker' />
<col class='diff-content' />
<col class='diff-marker' />
<col class='diff-content' />
<tr valign='top'>
<td colspan='2' style="background-color: white; color:black;">← Older revision</td>
<td colspan='2' style="background-color: white; color:black;">Revision as of 13:54, 6 September 2012</td>
</tr><tr>
<td colspan="2" class="diff-lineno">Line 1:</td>
<td colspan="2" class="diff-lineno">Line 1:</td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div>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\<span class="diffchange diffchange-inline">sim</span> 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.</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div>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\<span class="diffchange diffchange-inline">cong</span> 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.</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>== Linear negation ==</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>== Linear negation ==</div></td>
</tr>
</table>
Lionel Vaux
http://llwiki.ens-lyon.fr/mediawiki/index.php?title=Semantics&diff=430&oldid=prev
Olivier Laurent: notation for isomorphismes \cong instead of \sim
2009-10-19T08:45:35Z
<p>notation for isomorphismes \cong instead of \sim</p>
<table class='diff diff-contentalign-left'>
<col class='diff-marker' />
<col class='diff-content' />
<col class='diff-marker' />
<col class='diff-content' />
<tr valign='top'>
<td colspan='2' style="background-color: white; color:black;">← Older revision</td>
<td colspan='2' style="background-color: white; color:black;">Revision as of 08:45, 19 October 2009</td>
</tr><tr>
<td colspan="2" class="diff-lineno">Line 6:</td>
<td colspan="2" class="diff-lineno">Line 6:</td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\begin{array}{rclcrcl}</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\begin{array}{rclcrcl}</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div> A\biorth &=& A\\</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div> A\biorth &=& A\\</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (A\tens B)\orth &\<span class="diffchange diffchange-inline">sim</span>& A\orth\parr B\orth &\quad& \one\orth &\<span class="diffchange diffchange-inline">sim</span>& \bot\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> (A\tens B)\orth &\<span class="diffchange diffchange-inline">cong</span>& A\orth\parr B\orth &\quad& \one\orth &\<span class="diffchange diffchange-inline">cong</span>& \bot\\</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (A\parr B)\orth &\<span class="diffchange diffchange-inline">sim</span>& A\orth\tens B\orth &\quad& \bot\orth &\<span class="diffchange diffchange-inline">sim</span>& \one\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> (A\parr B)\orth &\<span class="diffchange diffchange-inline">cong</span>& A\orth\tens B\orth &\quad& \bot\orth &\<span class="diffchange diffchange-inline">cong</span>& \one\\</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (A\with B)\orth &\<span class="diffchange diffchange-inline">sim</span>& A\orth\plus B\orth &\quad& \top\orth &\<span class="diffchange diffchange-inline">sim</span>& \zero\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> (A\with B)\orth &\<span class="diffchange diffchange-inline">cong</span>& A\orth\plus B\orth &\quad& \top\orth &\<span class="diffchange diffchange-inline">cong</span>& \zero\\</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (A\plus B)\orth &\<span class="diffchange diffchange-inline">sim</span>& A\orth\with B\orth &\quad& \zero\orth &\<span class="diffchange diffchange-inline">sim</span>& \top\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> (A\plus B)\orth &\<span class="diffchange diffchange-inline">cong</span>& A\orth\with B\orth &\quad& \zero\orth &\<span class="diffchange diffchange-inline">cong</span>& \top\\</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (\oc A)\orth &\<span class="diffchange diffchange-inline">sim</span>& \wn A\orth\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> (\oc A)\orth &\<span class="diffchange diffchange-inline">cong</span>& \wn A\orth\\</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (\wn A)\orth &\<span class="diffchange diffchange-inline">sim</span>& \oc A\orth\\[1ex]</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> (\wn A)\orth &\<span class="diffchange diffchange-inline">cong</span>& \oc A\orth\\[1ex]</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\limp B &\<span class="diffchange diffchange-inline">sim</span>& A\orth\parr B\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> A\limp B &\<span class="diffchange diffchange-inline">cong</span>& A\orth\parr B\\</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\limp B &\<span class="diffchange diffchange-inline">sim</span>& B\orth\limp A\orth\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> A\limp B &\<span class="diffchange diffchange-inline">cong</span>& B\orth\limp A\orth\\</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\end{array}</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\end{array}</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div></math></div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div></math></div></td>
</tr>
<tr>
<td colspan="2" class="diff-lineno">Line 21:</td>
<td colspan="2" class="diff-lineno">Line 21:</td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div><math></div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div><math></div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\begin{array}{rcl}</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\begin{array}{rcl}</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\tens\one &\<span class="diffchange diffchange-inline">sim</span>& \one\tens A\<span class="diffchange diffchange-inline">sim</span> A\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> A\tens\one &\<span class="diffchange diffchange-inline">cong</span>& \one\tens A\<span class="diffchange diffchange-inline">cong</span> A\\</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\parr\bot &\<span class="diffchange diffchange-inline">sim</span>& \bot\parr A\<span class="diffchange diffchange-inline">sim</span> A\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> A\parr\bot &\<span class="diffchange diffchange-inline">cong</span>& \bot\parr A\<span class="diffchange diffchange-inline">cong</span> A\\</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\with\top &\<span class="diffchange diffchange-inline">sim</span>& \top\with A\<span class="diffchange diffchange-inline">sim</span> A\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> A\with\top &\<span class="diffchange diffchange-inline">cong</span>& \top\with A\<span class="diffchange diffchange-inline">cong</span> A\\</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\plus\zero &\<span class="diffchange diffchange-inline">sim</span>&\zero\plus A\<span class="diffchange diffchange-inline">sim</span> A\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> A\plus\zero &\<span class="diffchange diffchange-inline">cong</span>&\zero\plus A\<span class="diffchange diffchange-inline">cong</span> A\\</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\end{array}</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\end{array}</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div></math></div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div></math></div></td>
</tr>
<tr>
<td colspan="2" class="diff-lineno">Line 32:</td>
<td colspan="2" class="diff-lineno">Line 32:</td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div><math></div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div><math></div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\begin{array}{rcl}</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\begin{array}{rcl}</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\tens B &\<span class="diffchange diffchange-inline">sim</span>& B\tens A\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> A\tens B &\<span class="diffchange diffchange-inline">cong</span>& B\tens A\\</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\parr B &\<span class="diffchange diffchange-inline">sim</span>& B\parr A\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> A\parr B &\<span class="diffchange diffchange-inline">cong</span>& B\parr A\\</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\with B &\<span class="diffchange diffchange-inline">sim</span>& B\with A\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> A\with B &\<span class="diffchange diffchange-inline">cong</span>& B\with A\\</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\plus B &\<span class="diffchange diffchange-inline">sim</span>& B\plus A\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> A\plus B &\<span class="diffchange diffchange-inline">cong</span>& B\plus A\\</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\end{array}</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\end{array}</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div></math></div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div></math></div></td>
</tr>
<tr>
<td colspan="2" class="diff-lineno">Line 43:</td>
<td colspan="2" class="diff-lineno">Line 43:</td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div><math></div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div><math></div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\begin{array}{rcl}</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\begin{array}{rcl}</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (A\tens B)\tens C &\<span class="diffchange diffchange-inline">sim</span>& A\tens(B\tens C)\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> (A\tens B)\tens C &\<span class="diffchange diffchange-inline">cong</span>& A\tens(B\tens C)\\</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (A\parr B)\parr C &\<span class="diffchange diffchange-inline">sim</span>& A\parr(B\parr C)\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> (A\parr B)\parr C &\<span class="diffchange diffchange-inline">cong</span>& A\parr(B\parr C)\\</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (A\with B)\with C &\<span class="diffchange diffchange-inline">sim</span>& A\with(B\with C)\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> (A\with B)\with C &\<span class="diffchange diffchange-inline">cong</span>& A\with(B\with C)\\</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> (A\plus B)\plus C &\<span class="diffchange diffchange-inline">sim</span>& A\plus(B\plus C)\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> (A\plus B)\plus C &\<span class="diffchange diffchange-inline">cong</span>& A\plus(B\plus C)\\</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\end{array}</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\end{array}</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div></math></div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div></math></div></td>
</tr>
<tr>
<td colspan="2" class="diff-lineno">Line 62:</td>
<td colspan="2" class="diff-lineno">Line 62:</td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div><math></div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div><math></div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\begin{array}{rclcrcl}</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\begin{array}{rclcrcl}</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\tens(B\plus C) &\<span class="diffchange diffchange-inline">sim</span>& (A\tens B)\plus(A\tens C) &\quad&</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> A\tens(B\plus C) &\<span class="diffchange diffchange-inline">cong</span>& (A\tens B)\plus(A\tens C) &\quad&</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\tens\zero &\<span class="diffchange diffchange-inline">sim</span>& \zero\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> A\tens\zero &\<span class="diffchange diffchange-inline">cong</span>& \zero\\</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\parr(B\with C) &\<span class="diffchange diffchange-inline">sim</span>& (A\parr B)\with(A\parr C) &\quad&</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> A\parr(B\with C) &\<span class="diffchange diffchange-inline">cong</span>& (A\parr B)\with(A\parr C) &\quad&</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> A\parr\top &\<span class="diffchange diffchange-inline">sim</span>& \top\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> A\parr\top &\<span class="diffchange diffchange-inline">cong</span>& \top\\</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\end{array}</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\end{array}</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div></math></div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div></math></div></td>
</tr>
<tr>
<td colspan="2" class="diff-lineno">Line 107:</td>
<td colspan="2" class="diff-lineno">Line 107:</td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div><math></div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div><math></div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\begin{array}{rclcrcl}</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\begin{array}{rclcrcl}</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> \oc(A\with B) &\<span class="diffchange diffchange-inline">sim</span>& \oc A\tens\oc B &\quad& \oc\top &\<span class="diffchange diffchange-inline">sim</span>& \one\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> \oc(A\with B) &\<span class="diffchange diffchange-inline">cong</span>& \oc A\tens\oc B &\quad& \oc\top &\<span class="diffchange diffchange-inline">cong</span>& \one\\</div></td>
</tr>
<tr>
<td class="diff-marker">−</td>
<td style="background: #ffa; color:black; font-size: smaller;"><div> \wn(A\plus B) &\<span class="diffchange diffchange-inline">sim</span>& \wn A\parr\wn B &\quad& \wn\zero &\<span class="diffchange diffchange-inline">sim</span>& \bot\\</div></td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> \wn(A\plus B) &\<span class="diffchange diffchange-inline">cong</span>& \wn A\parr\wn B &\quad& \wn\zero &\<span class="diffchange diffchange-inline">cong</span>& \bot\\</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\end{array}</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\end{array}</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div></math></div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div></math></div></td>
</tr>
</table>
Olivier Laurent
http://llwiki.ens-lyon.fr/mediawiki/index.php?title=Semantics&diff=225&oldid=prev
Olivier Laurent: /* Additive structure */ diagonal
2009-03-15T10:51:04Z
<p><span dir="auto"><span class="autocomment">Additive structure: </span> diagonal</span></p>
<table class='diff diff-contentalign-left'>
<col class='diff-marker' />
<col class='diff-content' />
<col class='diff-marker' />
<col class='diff-content' />
<tr valign='top'>
<td colspan='2' style="background-color: white; color:black;">← Older revision</td>
<td colspan='2' style="background-color: white; color:black;">Revision as of 10:51, 15 March 2009</td>
</tr><tr>
<td colspan="2" class="diff-lineno">Line 75:</td>
<td colspan="2" class="diff-lineno">Line 75:</td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div> A\with B \longrightarrow A &\quad& A\with B \longrightarrow B\\</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div> A\with B \longrightarrow A &\quad& A\with B \longrightarrow B\\</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div> (C\limp A)\with(C\limp B) &\longrightarrow& C\limp(A\with B)\\</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div> (C\limp A)\with(C\limp B) &\longrightarrow& C\limp(A\with B)\\</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> A &\longrightarrow& A\with A\\</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div> A \longrightarrow A\plus B &\quad& B \longrightarrow A\plus B\\</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div> A \longrightarrow A\plus B &\quad& B \longrightarrow A\plus B\\</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div> (A\limp C)\with(B\limp C) &\longrightarrow& (A\plus B)\limp C\\</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div> (A\limp C)\with(B\limp C) &\longrightarrow& (A\plus B)\limp C\\</div></td>
</tr>
<tr>
<td colspan="2" class="diff-empty"> </td>
<td class="diff-marker">+</td>
<td style="background: #cfc; color:black; font-size: smaller;"><div> A\plus A &\longrightarrow& A\\</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\end{array}</div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div>\end{array}</div></td>
</tr>
<tr>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div></math></div></td>
<td class="diff-marker"> </td>
<td style="background: #eee; color:black; font-size: smaller;"><div></math></div></td>
</tr>
</table>
Olivier Laurent
http://llwiki.ens-lyon.fr/mediawiki/index.php?title=Semantics&diff=200&oldid=prev
Laurent Regnier: use of latex arrays for improving the presentation
2009-03-08T21:21:44Z
<p>use of latex arrays for improving the presentation</p>
<a href="http://llwiki.ens-lyon.fr/mediawiki/index.php?title=Semantics&diff=200&oldid=199">Show changes</a>
Laurent Regnier
http://llwiki.ens-lyon.fr/mediawiki/index.php?title=Semantics&diff=199&oldid=prev
Laurent Regnier: Creation of the page from the section "Main properties" of the Coherent semantics page
2009-03-08T20:40:37Z
<p>Creation of the page from the section "Main properties" of the <a href="/mediawiki/index.php/Coherent_semantics" title="Coherent semantics">Coherent semantics</a> page</p>
<p><b>New page</b></p><div>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.<br />
<br />
== Linear negation ==<br />
<br />
* <math>A\biorth = A</math><br />
* <math>(A\tens B)\orth\sim A\orth\parr B\orth,\qquad\one\orth = \bot</math><br />
* <math>(A\parr B)\orth\sim A\orth\tens B\orth,\qquad\bot\orth = \one</math><br />
* <math>(A\with B)\orth\sim A\orth\plus B\orth,\qquad\top\orth = \zero</math><br />
* <math>(A\plus B)\orth\sim A\orth\with B\orth,\qquad\zero\orth = \top</math><br />
* <math>(\oc A)\orth \sim \wn A\orth</math><br />
* <math>(\wn A)\orth \sim \oc A\orth</math><br />
<br />
* <math>A\limp B = A\orth\parr B</math><br />
* <math>A\limp B \sim B\orth A\orth</math><br />
<br />
== Neutrals ==<br />
<br />
* <math>A\tens\one\sim\one\tens A\sim A</math><br />
* <math>A\parr\bot\sim\bot\parr A\sim A</math><br />
* <math>A\with\top\sim\top\with A\sim A</math><br />
* <math>A\plus\zero\sim\zero\plus A\sim A</math><br />
<br />
== Commutativity ==<br />
<br />
* <math>A\tens B \sim B\tens A</math><br />
* <math>A\parr B \sim B\parr A</math><br />
* <math>A\with B \sim B\with A</math><br />
* <math>A\plus B \sim B\plus A</math><br />
<br />
== Associativity ==<br />
<br />
* <math>(A\tens B)\tens C \sim A\tens(B\tens C)</math><br />
* <math>(A\parr B)\parr C \sim A\parr(B\parr C)</math><br />
* <math>(A\with B)\with C \sim A\with(B\with C)</math><br />
* <math>(A\plus B)\plus C \sim A\plus(B\plus C)</math><br />
<br />
== Multiplicative semi-distributivity ==<br />
<br />
* <math>A\tens(B\parr C)\longrightarrow (A\tens B)\parr C</math><br />
<br />
== Multiplicative-additive distributivity ==<br />
<br />
* <math>A\tens(B\plus C)\sim (A\tens B)\plus(A\tens C),\qquad A\tens\zero\sim\zero</math><br />
* <math>A\parr(B\with C)\sim (A\parr B)\with(A\parr C),\qquad A\parr\top\sim\top</math><br />
<br />
== Additive structure ==<br />
<br />
* <math>A\with B\longrightarrow A,\qquad A\with B\longrightarrow B</math><br />
* <math>(C\limp A)\with(C\limp B)\longrightarrow C\limp(A\with B)</math><br />
* <math>A\longrightarrow A\plus B,\qquad B\longrightarrow A\plus B</math><br />
* <math>(A\limp C)\with(B\limp C)\longrightarrow (A\plus B)\limp C</math><br />
<br />
== Exponential structure ==<br />
<br />
* ''Dereliction'': <math>\oc A\longrightarrow A,\qquad A\longrightarrow\wn A</math><br />
* ''Weakening'': <math>\oc A\longrightarrow 1, \qquad \bot\longrightarrow \wn A</math><br />
* ''Contraction'': <math>\oc A\longrightarrow \oc A\tens\oc A,\qquad \wn A\parr\wn A\longrightarrow \wn A</math><br />
* ''Digging'': <math>\oc A\longrightarrow \oc\oc A,\qquad \wn\wn A\longrightarrow \wn A</math><br />
<br />
== Monoidality of exponential ==<br />
<br />
* <math>\oc A\tens\oc B\longrightarrow\oc(A\tens B),\qquad \one\longrightarrow\oc\one</math><br />
<br />
== The exponential isomorphism ==<br />
<br />
* <math>\oc(A\with B)\sim \oc A\tens\oc B,\qquad \oc\top\sim\one</math><br />
* <math>\wn(A\plus B)\sim \wn A\parr\wn B,\qquad \wn\zero\sim\bot</math></div>
Laurent Regnier