Mathematical notation for describing the limiting behaviour of functions. Includes $O(f(n))$ (upper bound), $\Omega(f(n))$ (lower bound), and $\Theta(f(n))$ (tight bound). For example, if $T(n) = 3n^2 + 2n + 1$, then $T(n) = O(n^2)$.

The linear connectives that encode choice: $\mathbin{\&}$ (with) and $\oplus$ (plus). They split proof search into branches rather than combining resources in parallel, distinguishing between internal choice (with) and external choice (plus).

A mathematical notation that describes the limiting behaviour of a function when the argument tends towards a particular value or infinity. In computer science, it’s used to classify algorithms according to how their running time or space requirements grow as the input size grows.

The ability of a distributed computing system to continue operating correctly even when some of the nodes fail or act maliciously. Named after the Byzantine General’s Problem, it addresses scenarios where components may provide conflicting information to different parts of the system.

A space-efficient probabilistic data structure used to test whether an element is a member of a set. It can have false positives but never false negatives, making it useful for applications where approximate membership queries are acceptable.

A complete subgraph where every pair of vertices is connected by an edge. The Clique problem asks whether a graph contains a clique of size k or larger, which is NP-complete for k ≥ 3.

A structural rule that allows you to duplicate an assumption: from $\Gamma, A, A \vdash B$ infer $\Gamma, A \vdash B$. Linear logic removes contraction so resources cannot be copied freely; duplication is only permitted for formulae marked with $!$.

A direct relationship between computer programs and mathematical proofs, where types correspond to logical propositions and programs correspond to proofs. This fundamental connection shows that programming and logic are essentially the same activity.

In linear logic, duality is given by linear negation $(\cdot)^{\perp}$, which swaps inputs and outputs and exchanges connectives (e.g. $(A \otimes B)^{\perp} = A^{\perp} \mathbin{\parr} B^{\perp}$ and $(A \mathbin{\&} B)^{\perp} = A^{\perp} \oplus B^{\perp}$). Saying one connective is the dual of another means they correspond under this negation.

The unary operators $!A$ (“of course”) and $?A$ (“why not”) that reintroduce weakening and contraction in linear logic. They mark formulae as freely copyable or discardable, restoring classical behaviour locally while keeping the surrounding system resource-aware.

A cycle in a graph that visits every vertex exactly once and returns to the starting vertex. The Hamiltonian Cycle problem asks whether such a cycle exists, which is NP-complete.

The pair of linear connectives that combine resources simultaneously: tensor $\otimes$ and par $\mathbin{\parr}$. Proofs using them consume all the supplied resources in lockstep rather than offering a choice between branches.

A compilation technique used in languages like Rust where generic functions and types are replaced with concrete implementations for each specific type they’re used with. This enables zero-cost abstractions by eliminating runtime type dispatch.

The multiplicative disjunction of linear logic, written $A \mathbin{\parr} B$. It represents co-availability: a consumer must be ready to interact with either side, and under linear negation it is dual to tensor $\otimes$. Par often models demand-driven or concurrent use of resources.

The additive disjunction of linear logic, written $A \oplus B$. It expresses external choice where the environment selects which branch is offered. Its dual under linear negation is with: $(A \oplus B)^{\perp} = A^{\perp} \mathbin{\&} B^{\perp}$.

A complexity class of decision problems for which no known polynomial-time algorithm exists, but any solution can be verified in polynomial time. A problem is NP-complete if it is both in NP and every problem in NP can be reduced to it in polynomial time.

Graphical representations of logical proofs introduced by Girard for linear logic. They eliminate the bureaucratic details of sequential proof trees, revealing the essential geometric structure of logical reasoning. Each proof net is a graph where nodes represent logical connectives and edges represent the flow of logical resources.

The Boolean Satisfiability Problem: determining whether there exists an assignment of Boolean values to variables that makes a propositional formula evaluate to true. This is the canonical NP-complete problem.

Given a universe of elements and a collection of subsets, find the smallest subcollection whose union covers all elements. The Set Cover problem is NP-complete and a fundamental problem in combinatorial optimisation.

The multiplicative conjunction of linear logic. A proof of $A \otimes B$ delivers both resources together and a proof that uses it must consume both. Under linear negation it is dual to $\mathbin{\parr}$.

A set of vertices such that every edge in the graph has at least one endpoint in the set. The Vertex Cover problem asks for the smallest such set, which is NP-complete.

A mathematical model of computation that defines an abstract machine which manipulates symbols on a strip of tape according to a table of rules. Despite its simplicity, a Turing machine can simulate the logic of any computer algorithm.

A structural rule that allows you to introduce an unused assumption: from $\Gamma \vdash A$ infer $\Gamma, B \vdash A$. Linear logic drops weakening so resources cannot be discarded unless wrapped in an exponential such as $!A$. This preserves resource-sensitive behaviour.

The additive conjunction of linear logic, written $A \mathbin{\&} B$. It offers both branches internally and the consumer selects which proof to use. Under linear negation it is dual to plus: $(A \mathbin{\&} B)^{\perp} = A^{\perp} \oplus B^{\perp}$. This is often what is meant when someone says “dual with”.