Linear logic, discovered by Jean-Yves Girard, is most commonly thought of as logic where facts must be used exactly once: they can't go unmentioned, and they are "used up" after their first use. This gives a powerful way to reason about resource usage, and is a theoretical inspiration for Rust's resource safety checks. This view of linear logic, when framed this way, is obviously very informal and missing important details. But it also gives a fairly limiting view of the possibilities linear logic offers. In its full definition, it's a generalization of "normal, ordinary, every-day" logic (sometimes called "persistent" or "structural" logic when talked about in comparison to linear logic). That is, linear logic puts restrictions on reasoning, but offers "escape-hatches" to do any ordinary reasoning. This has the powerful effect of annotating your proofs with the places that traditional rules are used. The end result is a clearer picture of what we're actually doing in our reasoning, and a fairly wide range of theoretical benefits arise from that clarity.
I'll start by thinking about linear logic from a logic perspective, instead of a computer science perspective. When studying logic, we generally have this concept of a context, written \(\Gamma\), holding all the facts we have available to us in a step of a proof. If \(\Gamma\) holds some fact \(A\), then from the facts of \(\Gamma\) we can deduce \(A\), since it's already one of those facts. This is written \(\Gamma\vdash A\), and pronounced "Gamma entails A." These statements are called "sequents." In ordinary logic, if you have \(\Gamma\vdash A\) and \(\Gamma\vdash B\), then it's possible to use the facts in \(\Gamma\) to prove the conjunction \(A\land B\), so we write the sequent \(\Gamma\vdash A\land B\). We often use a comma notation for contexts, like \(\Gamma,P\), to say "any context \(\Gamma\), including an empty one, extended with the additional proposition \(P\)."
In ordinary logic, if we have some sequent \(\Gamma\vdash P\), we're allowed to add any facts we want to the context, if we prove them. Formally, if \(\Gamma\vdash A\) and \(\Gamma\vdash B\), we can use the "weakening" rule to conclude \(\Gamma,A\vdash B\), since we know \(A\) doesn't contradict \(\Gamma\). Weakening allows us to duplicate anything in the context as many times as we want, so the context doesn't lose any information as we progress through a proof. Facts can be used more than once.
In ordinary logic, if we have the same thing duplicated in the context, we can throw out duplicates. Formally, if \(\Gamma,A,A\vdash B\), then we can use the "contraction" rule to conclude that \(\Gamma,A\vdash B\). That means that if a fact isn't necessary to prove something, we can throw it away. Facts can be used less than once.
Linear logic can be described as the result of throwing away weakening and contraction. Then there's no way to duplicate or throw away statements in the context, so they have to get used or stay in the context til the end of the proof. This is what gives linear logic the "use everything exactly once" reputation: you can't use things more than once, and you can't use things less than once. Weakening and contraction are called "structural" rules, so linear logic is an example of a logic called "substructural." Using a proposition in linear logic is called "consuming" it.
Implication in linear logic is written \(A\unicode{8888} B\) and is pronounced "lolli" or "the lollipop operator," which proves \(B\) in a way that uses \(A\) exactly once. Note that \(A\unicode{8888} B\) is itself a proposition that must be used exactly once.
There are a lot of details to making that a coherent logic, though. For example, when you've proven a conjunction \(A\land B\), you could use it to prove \(A\), but then the \(B\) vanishes. But, in other situations, we use both components of a conjunction. With disjunction there's the same situation: you can turn \(A\lor B\) into \(C\) with two implications \(A\Rightarrow C\) and \(B\Rightarrow C\), but can the context be used once per proof-of-implication, or do they have to "share resources," with a usage in one preventing a usage in the other? One might say that using the context once each is duplicating the context, but remember that only one of the implications actually gets "used," so sharing facts might make some disappear without getting used.
The answer to these questions isn't to pick one way and stick with it, but instead of have two different conjunctions and two different disjunctions! I'll now go through them one by one.
"Additive conjunction," written \(A\&B\) and pronounced "with," allows you to prove \(A\) or \(B\), your choice, but not both. This gives the notion mentioned above, where \(A\land B\Rightarrow A\) "drops" a \(B\), lost to the infinite platonic abyss. The unit of conjunction is True, because \(True\land A\equiv A\) for any proposition \(A\); the unit of additive conjunction is called "top," written \(\top\).
"Additive disjunction," written \(A\oplus B\) and pronounced "plus," allows you to prove two implications \(A\unicode{8888} C,B\unicode{8888} C\) in a way where they each have full access to the context, because we know we will use only one of the implications for our final \(A\oplus B\unicode{8888} C\), we just don't know which. The unit for additive disjunction is \(0\).
"Multiplicative conjunction," written \(A\otimes B\) and pronounced "tensor," allows you to prove both \(A\) and \(B\). Think of pattern-matching in a functional language, where this conjunction is a tuple. The unit of multiplicative conjunction is \(1\).
Finally, "multiplicative disjunction," written \(A\unicode{8523}B\) and pronounced "par," requires that the two implications \(A\unicode{8888}C,B\unicode{8888}C\) used to prove \(A\unicode{8523}B\unicode{8888}C\) share resources, meaning they may both happen. This is often used in contexts where you don't know which side of the disjunction is true and you want to just pick the first one, knowing that you'll change your mind and go pack if some new information reveals that it was actually the second one. For example, \(A\unicode{8523}(\neg A)\) is perfectly valid, even if \(A\) is "this turing machine halts," because you can assume it doesn't halt and change your mind if it actually halts. For this kind of thing to be allowed, it has to be okay for both implications to "happen," so they share resources. The unit of multiplicative disjunction is called "bottom," written \(\bot\).
© 2024 Ryan Brewer.