11
$\begingroup$

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$.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Kaveh Jul 14 '17 at 0:47
  • 5
    $\begingroup$ 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. $\endgroup$ – Damiano Mazza Jul 14 '17 at 11:15
  • $\begingroup$ 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. $\endgroup$ – chi Jul 14 '17 at 16:48
  • $\begingroup$ @chi I'm not sure the "resource interpretation" is the best way of understanding duality in LL. The process interpretation is much more comprehensible. $\endgroup$ – Martin Berger Jul 15 '17 at 9:13
11
$\begingroup$

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.

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

(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

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.
2. P. Wadler, Propositions as sessions.
3. Wikipedia, Proof net.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.