Semantics

From LLWiki
Revision as of 20:51, 25 April 2013 by Olivier Laurent (Talk | contribs)

Jump to: navigation, search

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 A\longrightarrow B the fact that there is a canonical morphism from A to B and by A\cong B 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


\begin{array}{rcl}
  A\tens(B\parr C) &\longrightarrow& (A\tens B)\parr C\\
\end{array}

Additive structure


\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}

Exponential structure


\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}

Monoidality of exponential


\begin{array}{rclcrcl}
  \oc A\tens\oc B &\longrightarrow& \oc(A\tens B) &\quad&
  \one &\longrightarrow& \oc\one\\
\end{array}

Personal tools