Introduction

Classical logic is generous. If you know it is raining, you can use that fact in ten proofs and it stays true every time. Logic does not charge you for premises.

But the real world does. You cannot pay for a coffee with the same euro twice. A file handle passed to a function should not be closed twice. A mutable memory cell cannot be aliased freely without causing data races.

In 1987, the logician Jean-Yves Girard invented linear logic to capture exactly this intuition. In linear logic, every assumption is a resource: when you use it, it is consumed. You cannot copy a premise for free, and you cannot silently discard it either. The famous slogan is that linear logic treats hypotheses like money — spend them once, spend them precisely.

This sounds like a restriction, but it is actually extra power: you can now reason about what happens to resources, not just about what is true or false. That shift from truth to resource accounting turned out to be foundational for programming languages and the theory of computation.

Try It: Resources Flow

The demo below shows a small resource machine. You start with a set of resource tokens and can route them through gates. Each gate consumes its inputs and produces outputs — nothing is duplicated, nothing vanishes silently.

<!-- Resource machine UI — pool on the left, gates in the middle, outputs at the bottom -->
<p class="hint">Each token is a resource. Select tokens (they turn red), then fire a gate to consume them — the gate produces a result. A token can only be used once. Gate B needs two tokens; gates A and C need one each.</p>
<div class="scene">
  <div class="token-pool" id="pool">
    <div class="pool-label">Resource tokens</div>
    <div class="tokens" id="tokens"></div>
  </div>
  <div class="gates" id="gates">
    <div class="gate-label">Gates (click after selecting tokens)</div>
    <div class="gate-row">
      <button class="gate" id="gate-a" type="button" title="Gate A: consume 1 token, produce output">
        <span class="gate-name">A</span>
        <span class="gate-desc">Transform</span>
        <span class="gate-needs">needs 1 token</span>
      </button>
      <button class="gate" id="gate-b" type="button" title="Gate B: consume 2 tokens, produce output">
        <span class="gate-name">B</span>
        <span class="gate-desc">Combine</span>
        <span class="gate-needs">needs 2 tokens</span>
      </button>
      <button class="gate" id="gate-c" type="button" title="Gate C: consume 1 token, produce output">
        <span class="gate-name">C</span>
        <span class="gate-desc">Promote</span>
        <span class="gate-needs">needs 1 token</span>
      </button>
    </div>
  </div>
</div>
<div class="output-area">
  <div class="output-label">Consumed → produced</div>
  <div class="outputs" id="outputs"></div>
</div>
<div class="status" id="status">Select tokens, then fire a gate.</div>
<div class="btns">
  <button id="reset" type="button" class="ghost">Reset</button>
</div>

/* Styles for the resource machine: token pool, gates, output area, status line */
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .7rem; line-height: 1.5; }
.scene { display: flex; gap: 1.2rem; flex-wrap: wrap; margin-bottom: .8rem; }
.token-pool, .gates { background: #f4f7fa; border: 1px solid #d0d8e2; border-radius: 10px; padding: .6rem .8rem; min-width: 140px; }
.pool-label, .gate-label, .output-label { font-size: .75rem; font-weight: 700; color: #5a7088; text-transform: uppercase; letter-spacing: .04em; margin-bottom: .45rem; }
.tokens { display: flex; flex-wrap: wrap; gap: 6px; min-height: 40px; }
.token { width: 36px; height: 36px; border-radius: 50%; background: #1d3557; color: #fff; font-size: .85rem; font-weight: 700; display: flex; align-items: center; justify-content: center; cursor: pointer; border: none; transition: transform .1s, background .1s; user-select: none; }
.token:hover { transform: scale(1.12); background: #2a4a72; }
.token.selected { background: #e63946; box-shadow: 0 0 0 3px #f9a8ad; }
.token.used { background: #aaa; cursor: not-allowed; opacity: .5; }
.gate-row { display: flex; gap: .5rem; flex-wrap: wrap; }
.gate { background: #fff; border: 1.5px solid #1d3557; border-radius: 10px; padding: .4rem .6rem; cursor: pointer; text-align: center; transition: background .15s; min-width: 80px; }
.gate:hover { background: #e8f0fb; }
.gate.active { border-color: #e63946; }
.gate-name { display: block; font-weight: 700; font-size: 1rem; color: #1d3557; }
.gate-desc { display: block; font-size: .7rem; color: #555; margin-top: .1rem; }
.gate-needs { display: block; font-size: .7rem; color: #888; font-style: italic; }
.output-area { background: #f0faf3; border: 1px solid #b2d8be; border-radius: 10px; padding: .6rem .8rem; margin-bottom: .6rem; min-height: 60px; }
.outputs { display: flex; flex-wrap: wrap; gap: 6px; min-height: 32px; }
.out-token { background: #0a7d33; color: #fff; border-radius: 8px; padding: .2rem .5rem; font-size: .82rem; font-weight: 600; }
.status { font-size: .95rem; font-weight: 600; margin: .3rem 0 .5rem; min-height: 1.4em; }
.status.ok { color: #0a7d33; }
.status.bad { color: #c92f3c; }
.status.info { color: #1d3557; }
.btns { display: flex; gap: .5rem; }
button.ghost { font: 600 13px system-ui, sans-serif; padding: .4rem .8rem; border: 1px solid #1d3557; background: #fff; color: #1d3557; border-radius: 8px; cursor: pointer; }

const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Linear Logic resource machine — tokens are consumed exactly once per gate.
// No weakening (cannot discard) and no contraction (cannot reuse).

// Gate definitions: needs = number of tokens required; produces = output label.
const GATES = {
  'gate-a': { needs: 1, label: 'A', produces: '⬡A' },
  'gate-b': { needs: 2, label: 'B', produces: '⬡B' },
  'gate-c': { needs: 1, label: 'C', produces: '!C' }
};

const INITIAL_TOKENS = ['R1','R2','R3']; // initial resource tokens
let tokens = [...INITIAL_TOKENS];
let selected = [];
let outputs = [];

function setStatus(msg, cls) {
  const s = document.getElementById('status');
  s.textContent = msg; s.className = 'status ' + cls;
}

function renderTokens() {
  const el = document.getElementById('tokens'); el.innerHTML = '';
  tokens.forEach((t, i) => {
    const btn = document.createElement('button');
    btn.className = 'token' + (selected.includes(i) ? ' selected' : '');
    btn.type = 'button'; btn.textContent = t;
    btn.title = selected.includes(i) ? 'Deselect this token' : 'Select this token';
    btn.addEventListener('click', () => toggleToken(i));
    el.appendChild(btn);
  });
}

function renderOutputs() {
  const el = document.getElementById('outputs'); el.innerHTML = '';
  outputs.forEach(o => {
    const span = document.createElement('span');
    span.className = 'out-token'; span.textContent = o;
    el.appendChild(span);
  });
}

function toggleToken(i) {
  const idx = selected.indexOf(i);
  if (idx === -1) selected.push(i);
  else selected.splice(idx, 1);
  renderTokens();
  // highlight gates whose required count matches the current selection
  updateGateHighlight();
  setStatus('Select tokens, then fire a gate.', 'info');
}

function updateGateHighlight() {
  Object.keys(GATES).forEach(id => {
    const btn = document.getElementById(id);
    btn.classList.toggle('active', selected.length === GATES[id].needs);
  });
}

function fireGate(id) {
  const gate = GATES[id];
  if (selected.length !== gate.needs) {
    // user selected wrong number of tokens for this gate
    setStatus(fmt('Gate needs exactly %needs% token(s) selected.', { needs: gate.needs }), 'bad');
    return;
  }
  // record which tokens are consumed before splicing them out
  const consumed = selected.map(i => tokens[i]);
  // remove selected tokens in descending index order to avoid index shift
  // remove selected tokens (descending to keep indices valid)
  const sorted = [...selected].sort((a, b) => b - a);
  sorted.forEach(i => tokens.splice(i, 1));
  selected = [];
  outputs.push(gate.produces + ' (' + consumed.join('+') + ')');
  renderTokens();
  renderOutputs();
  updateGateHighlight();
  setStatus(fmt('Gate %label% consumed: %consumed% — each resource used exactly once.', { label: gate.label, consumed: consumed.join(', ') }), 'ok');
}

function reset() {
  tokens = [...INITIAL_TOKENS];
  selected = [];
  outputs = [];
  renderTokens();
  renderOutputs();
  updateGateHighlight();
  setStatus('Select tokens, then fire a gate.', 'info');
}

// attach click listeners to gates and reset button
Object.keys(GATES).forEach(id => {
  document.getElementById(id).addEventListener('click', () => fireGate(id));
});
document.getElementById('reset').addEventListener('click', reset);

reset();
Result
Console

Notice what makes this different from ordinary logic: if you try to feed a token to two gates at once, the machine rejects it. Each token exists at exactly one place. This is the heart of linear logic: the rules for contraction (copying) and weakening (discarding) that classical logic takes for granted are simply absent. You must account for every resource.

The Real Structure

Classical logic has two "structural rules" that go unnoticed because they seem trivially obvious:

  • Weakening: if you can prove BB from AA, you can prove BB from AA and CC — you just ignore CC.
  • Contraction: if you can prove BB from two copies of AA, you can prove BB from one copy — you just reuse it.

Girard deleted both rules. That one move splits every classical connective into two:

Classical Linear (multiplicative) Linear (additive)
A∧BA \land B A⊗BA \otimes B — tensor: have both, spent both A&BA \mathbin{\&} B — with: choose one, keep the other
A∨BA \lor B AA ⅋ BB — par: dual of tensor A⊕BA \oplus B — plus: choose one, lose the other
¬A\lnot A A⊥A^\perp — multiplicative negation

And to get classical logic back when you need it, Girard added a modality: !A (read "of course AA") marks a resource as unlimited — it can be copied and discarded freely. This is the exponential fragment. Under a !, you are back in classical territory.

The key theorem (Girard, 1987): linear logic is a conservative extension of classical logic — every classical tautology is provable in linear logic under !, but linear logic can prove many things classical logic cannot even express.

Decidability varies sharply across the fragments: the multiplicative fragment is decidable in polynomial time; adding the additive connectives keeps it decidable; adding the full exponential ! makes it undecidable (equivalent to Turing machines).

Where It Matters

Linear logic was invented as pure mathematics, but its applications turned out to be everywhere that resources matter:

  • Rust's ownership and borrow checker: Rust's type system is essentially a practical implementation of linear logic. Each value has a unique owner; moving it transfers ownership (consuming the old binding); borrowing is the ! modality — temporary, controlled reuse. The famous compile-time memory-safety guarantee is linear logic enforced by a type checker.
  • Session types and concurrency: a session type describes a communication protocol as a linear-logic proof. If your program type-checks, it is guaranteed to follow the protocol exactly — no double-sends, no reads after close, no deadlocks in certain models.
  • Quantum computing: quantum gates cannot copy or delete arbitrary quantum states (no-cloning / no-deleting theorems). A quantum circuit is literally a linear-logic proof in the multiplicative fragment — qubits flow through gates exactly once.
  • Database transactions: the semantics of "use a ticket once" or "transfer $100 from account A to B" is naturally modeled in linear logic — the $100 disappears from A and appears in B; it is not duplicated.
  • Game semantics: the P vs NP landscape of interactive proofs and games has a clean linear-logic interpretation — the dialogue between prover and verifier is a cut-elimination in a linear sequent calculus.

Conclusion

Girard's move was elegant: take classical logic, delete two rules nobody thought twice about, and discover that every connective splits in two — revealing a whole new dimension of logical structure that classical logic had been silently collapsing.

The payoff was not just theoretical. Linear logic gave programming-language designers the language to describe ownership, borrowing, and protocol compliance in a mathematically rigorous way. Rust, session types, and quantum circuit semantics all live inside the linear-logic framework.

The core insight remains simple enough to hold in one hand: a premise is a resource. Use it once. Account for it precisely. That single constraint — no free copying, no silent discarding — turns out to be one of the most productive ideas in the last four decades of logic and computer science.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/linear-logic/Content licensed under CC BY-NC 4.0.