The TCS Formalization Drive

Pure type systems (PTSs) are a uniform framework covering the simply typed λ-calculus, System F, the calculus of constructions and the type theories behind proof assistants such as Coq and Lean. A system is specified by its sorts (like $\ast$ and $\square$), axioms ($\ast:\square$) and product rules (which dependent function types may be formed). Normalization is…

A logic for unordered finite structures (graphs, databases, relational inputs given up to isomorphism) must give answers that do not depend on how the input elements are named. Many polynomial-time algorithms nevertheless make arbitrary intermediate choices, for example the pivot in Gaussian elimination, without changing their final answer. Choiceless…

Descriptive complexity asks whether complexity classes can be characterized by logics, without reference to machines. Immerman and Vardi (1982) showed that on ordered finite structures, first-order logic with a least fixed-point operator expresses exactly the polynomial-time queries. On unordered structures, such as graphs given only up to isomorphism, an…

Add random clauses one at a time to a Boolean formula on $n$ variables until it first becomes unsatisfiable. The index $H_n$ of that first failure is the satisfiability hitting time of random $k$-SAT. Its mean, divided by $n$, converges to the satisfiability threshold; its variance measures the width of the transition window. Friedgut's sharp-threshold theorem…

A random $k$-SAT formula on $n$ Boolean variables is a conjunction of $m$ independent random clauses, each an OR of $k$ literals on distinct variables. As the clause density $m/n$ grows, the formula changes from almost surely satisfiable to almost surely unsatisfiable. Random $k$-SAT is a central model in probabilistic combinatorics, the theory of algorithms and…

A removal lemma says that an object far from having a forbidden substructure must contain many copies of it. Such statements are the combinatorial backbone of property testing: if every matrix that is $\epsilon$-far from avoiding a pattern $H$ contains at least $c_H\epsilon^{C_H}n^{2k}$ copies of $H$, then sampling a number of rows and columns polynomial in …

A thin spanning tree of a graph is a spanning tree that uses only a small fraction of the edges of every cut. Thin trees were introduced for the asymmetric traveling salesman problem: Asadpour, Goemans, Mądry, Oveis Gharan and Saberi showed that a thin tree of low cost can be augmented into a cheap tour, giving an $O(\log n/\log\log n)$-approximation (doi:10.1…

A spanning tree keeps a graph connected with as few edges as possible. A spanning tree is thin if, in addition, it uses only a small fraction of the edges of every cut. Thin trees were introduced as a tool for the asymmetric traveling salesman problem (ATSP): Asadpour, Goemans, Mądry, Oveis Gharan and Saberi showed that thin trees, together with cost…

An exact linear equation can carry arbitrarily fine real information: $d$ independent Gaussian equations $Y_t = \langle X_t, s\rangle$ determine a vector $s \in \mathbb{R}^d$ almost surely. A streaming learner that keeps only finitely many persistent states cannot retain those equations at arbitrary precision. The question is how many fresh equations such a…

A finite message chosen from data changes the conditional distribution of those data. In memory-constrained inference this matters directly: a learner observing a signal $S$ through exact Gaussian equations keeps a finite state $W$, and after conditioning on $W$ the rows that were used to select it are biased. An independent Gaussian matrix has the same…

An exact linear observation $\langle x, S\rangle$ of a real signal can carry arbitrarily many bits. A finite message computed from a block of such observations cannot, but its information content is not controlled by the number of observations alone: if earlier messages have already concentrated the signal in a small region, the next block can exploit that…

Suppose an unknown unit vector $s \in S^{d-1}$ is observed through exact linear measurements $Y_j = \langle X_j, s\rangle$ with independent Gaussian rows $X_j \sim N(0, I_d)$. If every pair is kept, $d$ rows determine $s$. A learner that can keep only a bounded number of bits between measurements must compress each exact real label into a state update, and the…

A single exact linear equation $y = \langle x, s\rangle$ about an unknown unit vector $s \in \mathbb{R}^d$ carries arbitrarily fine information: $d$ independent Gaussian equations determine $s$ almost surely, provided all of them can be kept. A learner that reads the equations once, in order, and keeps only a bounded number of bits between them faces a different…

Iterated matrix multiplication asks for the $(1,1)$ entry of a product of $d$ matrices of size $w\times w$ with independent variable entries,

A regular expression describes a set of words using letters, union, concatenation and the Kleene star $P^*$ (any finite repetition of words from $P$). The star height of an expression is the depth of nesting of its stars, and it measures how many layers of unbounded repetition a regular language genuinely needs. For ordinary expressions this hierarchy is…

Weisfeiler–Leman (WL) refinement compares two graphs by repeatedly refining colors of ordered vertex $k$-tuples. For every fixed dimension $k$ this is a polynomial-time procedure, with running time $n^{O(k)}$. When $k$ is part of the input, that computation is no longer polynomial, and the complexity of deciding the outcome becomes a question in its own right.…

The Weisfeiler–Leman (WL) method colors $k$-tuples of vertices by repeatedly recording their local extension patterns; two graphs are $k$-WL equivalent when the stable color histograms agree. For each fixed $k$ the direct algorithm runs in time $n^{O(k)}$: there are $n^k$ tuples and polynomially many refinement rounds. The question is whether the growing exponent is…

The Weisfeiler–Leman (WL) algorithm refines colors of vertex tuples to test graph isomorphism, and its dimension $k$ controls how much tuple information is used. A graph's Weisfeiler–Leman dimension $\mathrm{WLdim}(G)$ is the least $k$ for which $k$-WL refinement identifies $G$, i.e. distinguishes it from every non-isomorphic graph. This is a standard measure of the…

The Weisfeiler–Leman (WL) method is the standard combinatorial heuristic for graph isomorphism: it repeatedly refines colors of $k$-tuples of vertices, and two graphs it cannot tell apart are called $k$-WL equivalent. It is equivalent to counting-logic indistinguishability and, by results of Dvořák (2010) and Dell, Grohe and Rattan (2018), to equality of…

The discrete Fourier transform of length $n$ is computed by the fast Fourier transform with $O(n\log n)$ arithmetic operations, and this has been the benchmark since Cooley and Tukey (1965). Whether $\Omega(n\log n)$ operations are necessary is one of the basic open questions of algebraic complexity theory. Lower bounds of order $n\log n$ are known only under…

Two-way deterministic finite automata (2DFAs) recognize exactly the regular languages (Rabin and Scott; Shepherdson, 1959), but letting the head revisit the input can change how much finite control is needed. In 1978 Sakoda and Sipser asked for the state cost of converting one-way and two-way nondeterministic automata into 2DFAs: is a polynomial number of…

Given a finite collection $\mathcal S$ of strings, the shortest common superstring (SCS) problem asks for a shortest string $T$ that contains every member of $\mathcal S$ as a contiguous substring. It is a basic model of sequence assembly (reconstructing a long DNA sequence from overlapping fragments) and of data compression, and it is a standard test problem for…

In metric $k$-median, a finite set $J$ (or $D$) of clients and a finite set $F$ of candidate facilities lie in a common finite metric with rational distances. Given an integer $k\ge1$, one opens a nonempty set $S\subseteq F$ with $|S|\le k$ and pays

In metric $k$-median, a finite set $J$ (or $D$) of clients and a finite set $F$ of candidate facilities lie in a common finite metric with rational distances. Given an integer $k\ge1$, one opens a nonempty set $S\subseteq F$ with $|S|\le k$ and pays

In the trace reconstruction problem an unknown binary word $x\in\{0,1\}^n$ is passed repeatedly through a deletion channel: each bit is deleted independently with known probability $q\in(0,1)$ and the surviving bits are concatenated in order. Each output, called a trace, reveals its length and its bits but not which positions survived. The question is how many…