Multiplicative Conjunction (Linear Logic)

linear-logic

Definition

Multiplicative Conjunction ( Linear Logic)

$A\otimes B$ bundles $A$ and $B$ as independent resources, each available exactly once. In a proof / program, $A\otimes B$ is produced from disjoint portions of the context and consumed one $A$ and one $B$ at a time.

Right sequent (introduce $\otimes$): split resources to build each side

$$\frac{\Gamma ⊢A\Delta ⊢B}{\Gamma ,\Delta ⊢A\otimes B}(\otimes R)$$

Left sequent (use $\otimes$): to use a bundle, open it

$$\frac{\Gamma ,A,B⊢C}{\Gamma ,A\otimes B⊢C}(\otimes L)$$

With $1$ as its neutral element, $\otimes$ forms a monoid $⟨M,\otimes ,1⟩$:

$$1\otimes A\cong A\cong A\otimes 1.$$

Analogy

To make a pancake, both $Flour$ and $Egg$ are needed, each exactly once. The bundle is denoted

$$\mathrm{Flour}\otimes \mathrm{Egg}.$$

Using $\mathrm{Flour}\otimes \mathrm{Egg}$ consumes one $Flour$ and one $\mathrm{Egg}$ to produce the pancake; no copying, no discarding.