<p>I'm not sure this question is ideal for CSTheory, but given that it's already gathering upvotes, here is an  answer somebody might have given had the question  been posted on <a href="https://cs.stackexchange.com">cs.stackexchange</a>.</p>

<p>In order to understand linear logic's notion of duality $(\cdot)^{\bot}$,
which forces conjunction and disjunction apart much further than we are used to in conventional logic, I recommend
not 
  to think of linear logic in terms of resources (although this is
  an important reading). Instead  think of linear logic formulae $A$
  as processes that communicate
  at a port / name / channel. This interpretation has been fleshed out first in (1) to the best of my knowledge, but it's already alluded to in Girard's original work. As a picture:</p>

<p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
  <a href="https://i.sstatic.net/7jJhl.png" rel="noreferrer"><img src="https://i.sstatic.net/7jJhl.png" alt="Process"></a></p>

<p>(I'm not sure how properly to center images here.)
Linear conjunction $A \otimes B$ is interpreted as running processes $A$
  and $B$ in <i>parallel</i>.  The process $A \otimes B$
  communicates <i>pairs</i> $(a, b)$ at its port, where $a$ comes from
  $A$ and $b$ is $B$'s communication.</p>

<p>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;
<a href="https://i.sstatic.net/qtzhh.png" rel="noreferrer"><img src="https://i.sstatic.net/qtzhh.png" alt="enter image description here"></a></p>

<p><i>Dualisation</i> $(.)^{\bot}$ (which is linear logic's
  negation) switches input and output. Hence the dual of $A \otimes B$
  is</p>

<p>$$
  (A \otimes B)^{\bot} \quad = \quad A^{\bot} ⅋ B^{\bot}
  $$</p>

<p>In this reading $A^{\bot} ⅋
  B^{\bot}$ is the process that communicates with $A \otimes B$.</p>

<p>Linear logic's equivalent of disjunction can
  be given a similar process-theoretic reading. The formula</p>

<p>$$
  A\ \&amp;\ B
  $$</p>

<p>should also be seen as  two processes $A$ and $B$ in parallel, but rather than actively sending messages, they wait for
  the environment to decide which to run. So $A \&amp; B$ sits there,
  waiting on its channel for a bit of information which decides if $A
  \&amp; B$ should run as $A$ or as $B$. This is a 'parallel' version of
  the $if/then/else$ in sequential programmaning languages. The dual
  $(A \&amp; B)^{\bot}$ of $A \&amp; B$ is</p>

<p>$$
  (A \&amp; B)^{\bot} \quad = \quad A^{\bot} \oplus B^{\bot}
  $$</p>

<p>can be seen as a process sending 1 bit of information to $A \&amp;
  B$, namely: "continue as $A$" or "continue as $B$". This is similar to in  $if\ true\ then\ P\ else\ Q$ evaluating to $P$ while
  $if\ false\ then\ P\ else\ Q$ evaluating to $Q$, except that
the choice between $A$ and $B$ is now made by the environment.</p></p>


  The !-operator also has a process-theoretic interpretation: if $A$
  is read as a process, then $!A$ can be read as running infinitely
  many processes $A$ in parallel.</p>

<p>In this reading the axioms $A \vdash A$ of linear logic become simple 'wires' that forward messages from processes $A^{\bot}$ to processes $A$. This interpretation of axioms is already in Girard's proof nets (3).</p>

<p>This process-theoretic interpretation  has been influential and
  given rise to a lot of follow-up work like e.g. (2) for session types.
 Nevertheless, there are some
edge cases that make it a bit awkward, and to the best of my knowledge
  it hasn't been made to work perfectly for <i>full</i> linear logic even in 2017. </p>

<hr>

<p><sub>
1. S. Abramsky, <a href="http://www.sciencedirect.com/science/article/pii/030439759390181R" rel="noreferrer">Computational Interpretations of Linear Logic</a>.
<br>
2. P. Wadler, <a href="http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-sessions/propositions-as-sessions.pdf" rel="noreferrer">Propositions as sessions</a>.
<br>
3. Wikipedia, <a href="https://en.wikipedia.org/wiki/Proof_net" rel="noreferrer">Proof net</a>.</p>

<p></sub></p>

CC BY-SA 3.0
2017-07-15T09:40:27.737Z
2017-07-15T22:20:30.373Z
2017-07-15T22:20:30.373Z
Martin Berger
<p>I'm trying to understand linear logic to understand linear type systems better. However, when I read the rules, I fail to get an intuition behind it as I've done in modal logic - $\Box A$ means <em>$A$ is required</em> as in Kripke frames $A$ is required for every reachable world [$\Diamond A$ is <em>$A$ is possible</em> mutatis mutandis]. But I cannot find any intuitive explanation for duality and which of conjunction / disjunction pairs (if any) corresponds to $\land$ and $\lor$.</p>

CC BY-SA 3.0
2017-07-14T00:47:20.300Z
Girard's original paper is where you should look if you want to understand the intuition behind them. The question as is is too general imo and the answer would be to look at the Wikipedia page for linear logic.
Kaveh
CC BY-SA 3.0
2017-07-14T11:15:40.460Z
I agree that this is a bit too bread and definitely not research level, maybe your should ask the question on CS Stack Exchange.  However, I would discourage you from using Girard's original paper as the entry point to linear logic.  Maybe the Wikipedia is a better place to start.
Damiano Mazza
CC BY-SA 3.0
2017-07-14T16:48:55.443Z
This is quite broad. A suggestion, perhaps, could be starting to regard formulas as a "currency" which can be spent, instead of statements of truth. Then, conjunction could be $a \otimes b$ meaning we can spend both an $a$ coin and a $b$ coin. Another kind of conjunction could be $a \& b$, meaning we can choose between spending $a$ and spending $b$ (but not both!). You can find some examples on Wikipedia, as Damiano suggested.
chi
CC BY-SA 3.0
2017-07-15T09:13:15.120Z
@chi I'm not sure the "resource interpretation" is the best way of understanding duality in LL.  The process interpretation is much more comprehensible.
Martin Berger
<lo.logic><type-theory><linear-logic>
What is the intuition behind linear logic?
Maja Piechotka
# What is the intuition behind linear logic?

(Asked by: username_0 on 2017-07-13)

I'm trying to understand linear logic to understand linear type systems better. However, when I read the rules, I fail to get an intuition behind it as I've done in modal logic - $\Box A$ means *$A$ is required* as in Kripke frames $A$ is required for every reachable world [$\Diamond A$ is *$A$ is possible* mutatis mutandis]. But I cannot find any intuitive explanation for duality and which of conjunction / disjunction pairs (if any) corresponds to $\land$ and $\lor$.

**Tags:** lo.logic, type-theory, linear-logic

> **Comments:**
> **username_1**: Girard's original paper is where you should look if you want to understand the intuition behind them. The question as is is too general imo and the answer would be to look at the Wikipedia page for linear logic.  
> **username_2**: I agree that this is a bit too bread and definitely not research level, maybe your should ask the question on CS Stack Exchange.  However, I would discourage you from using Girard's original paper as the entry point to linear logic.  Maybe the Wikipedia is a better place to start.  
> **username_3**: This is quite broad. A suggestion, perhaps, could be starting to regard formulas as a "currency" which can be spent, instead of statements of truth. Then, conjunction could be $a \otimes b$ meaning we can spend both an $a$ coin and a $b$ coin. Another kind of conjunction could be $a \& b$, meaning we can choose between spending $a$ and spending $b$ (but not both!). You can find some examples on Wikipedia, as Damiano suggested.  
> **username_4**: @username_3 I'm not sure the "resource interpretation" is the best way of understanding duality in LL.  The process interpretation is much more comprehensible.  

---

## 1 answers

### Answer by username_4 on 2017-07-15. Score: 12 | Accepted answer

I'm not sure this question is ideal for CSTheory, but given that it's already gathering upvotes, here is an answer somebody might have given had the question been posted on [cs.stackexchange](https://cs.stackexchange.com).

In order to understand linear logic's notion of duality $(\cdot)^{\bot}$,
which forces conjunction and disjunction apart much further than we are used to in conventional logic, I recommend
not
to think of linear logic in terms of resources (although this is
an important reading). Instead think of linear logic formulae $A$
as processes that communicate
at a port / name / channel. This interpretation has been fleshed out first in (1) to the best of my knowledge, but it's already alluded to in Girard's original work. As a picture:

[![Process](https://i.sstatic.net/7jJhl.png)](https://i.sstatic.net/7jJhl.png)

(I'm not sure how properly to center images here.)
Linear conjunction $A \otimes B$ is interpreted as running processes $A$
and $B$ in *parallel*. The process $A \otimes B$
communicates *pairs* $(a, b)$ at its port, where $a$ comes from
$A$ and $b$ is $B$'s communication.

[![enter image description here](https://i.sstatic.net/qtzhh.png)](https://i.sstatic.net/qtzhh.png)

*Dualisation* $(.)^{\bot}$ (which is linear logic's
negation) switches input and output. Hence the dual of $A \otimes B$
is

$$
(A \otimes B)^{\bot} \quad = \quad A^{\bot} ⅋ B^{\bot}
$$

In this reading $A^{\bot} ⅋
B^{\bot}$ is the process that communicates with $A \otimes B$.

Linear logic's equivalent of disjunction can
be given a similar process-theoretic reading. The formula

$$
A\ \&\ B
$$

should also be seen as two processes $A$ and $B$ in parallel, but rather than actively sending messages, they wait for
the environment to decide which to run. So $A \& B$ sits there,
waiting on its channel for a bit of information which decides if $A
\& B$ should run as $A$ or as $B$. This is a 'parallel' version of
the $if/then/else$ in sequential programmaning languages. The dual
$(A \& B)^{\bot}$ of $A \& B$ is

$$
(A \& B)^{\bot} \quad = \quad A^{\bot} \oplus B^{\bot}
$$

can be seen as a process sending 1 bit of information to $A \&
B$, namely: "continue as $A$" or "continue as $B$". This is similar to in $if\ true\ then\ P\ else\ Q$ evaluating to $P$ while
$if\ false\ then\ P\ else\ Q$ evaluating to $Q$, except that
the choice between $A$ and $B$ is now made by the environment.

The !-operator also has a process-theoretic interpretation: if $A$
is read as a process, then $!A$ can be read as running infinitely
many processes $A$ in parallel.

In this reading the axioms $A \vdash A$ of linear logic become simple 'wires' that forward messages from processes $A^{\bot}$ to processes $A$. This interpretation of axioms is already in Girard's proof nets (3).

This process-theoretic interpretation has been influential and
given rise to a lot of follow-up work like e.g. (2) for session types.
Nevertheless, there are some
edge cases that make it a bit awkward, and to the best of my knowledge
it hasn't been made to work perfectly for *full* linear logic even in 2017.

---

1. S. Abramsky, [Computational Interpretations of Linear Logic](http://www.sciencedirect.com/science/article/pii/030439759390181R).
  
2. P. Wadler, [Propositions as sessions](http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-sessions/propositions-as-sessions.pdf).
  
3. Wikipedia, [Proof net](https://en.wikipedia.org/wiki/Proof_net).


---

