¶Linear logic cheat sheet
¶Linear implication
A ⊸ B = A⊥ ⅋ B
You can transform A into B. The act of producing B consumes A.
One interpretation of the right-hand side of equivalence is that a transformation of A into B can be broken apart into a producer of A and a consumer of B, which execute in parallel connected via a pipe.
This also highlights that the information flow is one-way. How the consumer chooses to use the value can have no effect on how the producer creates it.
¶Multiplicative conjunction
A ⊗ B
Produces both A and B, which the consumer can use however they wish. Consuming A cannot effect how and whether B can be consumed.
¶Multiplicative disjunction
A ⅋ B
A and B are executed or consumed concurrently or in parallel, and there can be no crosstalk between them.
¶Additive conjunction
A & B
Produces either A or B on demand, consumer gets to choose. External choice from CSP. Consumer cannot get both A and B.
If consumer always wants A, they never have to specify how to consume B.
¶Additive disjunction
A ⊕ B
Produces either A or B on demand, producer gets to choose. Internal choice from CSP. Consumer cannot get both A and B. Consumer must specify how to consume both alternatives, since they have no control over which one they get.
¶Exponentials
!A
A factory or clone operation for A. You can obtain as many copies of A as you need. (Including 0, I think?)
?A
A drop operation for A. You can choose to use A or not.