Multiplicative Conjunction (Linear Logic)

linear-logic

Definition

Multiplicative Conjunction ( Linear Logic)

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

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

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

With as its neutral element, forms a monoid :

Analogy

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

Using consumes one and one to produce the pancake; no copying, no discarding.