Combinatorics

Motivation

Matroids abstract the combinatorial content of linear independence: which sets of columns of a matrix are independent, which are maximal (bases), and how bases relate to each other. This abstraction, isolated independently by Whitney (1935) and van der Waerden's school, turned out to be exactly the right level of generality for a large family of greedy and augmenting-path algorithms — a base of a matroid can always be reached from another by a sequence of single-element swaps, and this exchange property is what makes local search on bases correct and efficient.

A natural question, raised in the 1980s once matroid-based combinatorial optimization was mature, is what happens when bases are not merely present or absent but carry real-valued weights that must interact well with the exchange structure. Dress and Wenzel answered this with the notion of a valuated matroid: a real-valued function on the bases of a matroid satisfying a weighted strengthening of the exchange axiom. Their motivation was explicitly algorithmic — valuated matroids are exactly the structures for which a greedy algorithm computes an optimal basis under linear objectives, and more generally under the family of "tilted" objectives obtained by adding an arbitrary linear functional. Independently, valuated matroids arise from the classical Grassmann–Plücker relation applied to matrices over a field with a valuation (hence the name), connecting them to tropical geometry.

This mission formalizes the two theorems of Murota's Discrete Convex Analysis (2003, §2.4) that make this story precise: the classical correspondence between a matroid's base family and its rank function (Theorem 2.29), and the characterization of valuations by a perturbation-robustness property (Theorem 2.32). Theorem 2.32 is also historically the entry point of the book's central theme — it is the special case, for the two-valued lattice $\{0,1\}^V$, of the general local-exchange criterion for M-convex functions that occupies chapters 6 and 7.

Setting

Let $V$ be a finite set (the ground set). A matroid on $V$ is a pair $(V, \mathcal B)$ where $\mathcal B$, the base family, is a nonempty family of subsets of $V$ satisfying the simultaneous exchange axiom (B): for every $J, J' \in \mathcal B$ and every $i \in J \setminus J'$, there exists $j \in J' \setminus J$ such that both

$$J - i + j := (J \setminus \{i\}) \cup \{j\} \in \mathcal B \quad\text{and}\quad J' + i - j := (J' \setminus \{j\}) \cup \{i\} \in \mathcal B.$$

Equivalently (Theorem 2.29 below), a matroid can be described by its rank function $\rho : 2^V \to \mathbb Z$, a set function satisfying:

• (R1) $0 \le \rho(X) \le |X|$ for every $X \subseteq V$;
• (R2) monotonicity: $X \subseteq Y \implies \rho(X) \le \rho(Y)$;
• (R3) submodularity: $\rho(X) + \rho(Y) \ge \rho(X \cup Y) + \rho(X \cap Y)$.

A valuation of a base family $\mathcal B$ is a function $\omega : \mathcal B \to \mathbb R$ satisfying the axiom (VM): for every $J, J' \in \mathcal B$ and $i \in J \setminus J'$, there is $j \in J' \setminus J$ with $J - i + j, J' + i - j \in \mathcal B$ and

$$\omega(J) + \omega(J') \le \omega(J - i + j) + \omega(J' + i - j).$$

The pair $(V, \omega)$ is then a valuated matroid. For $p : V \to \mathbb R$, the perturbation of $\omega$ by $p$ is

$$\omega[-p](J) = \omega(J) - \sum_{j \in J} p(j).$$

Formalization targets

Goal: Theorem 2.32 (the valuated matroid characterization)

$$\omega \text{ is a valuation of } \mathcal B \iff \forall\, p : V \to \mathbb R,\ \{J \in \mathcal B : \omega[-p](J') \le \omega[-p](J)\ \forall J' \in \mathcal B\} \text{ is a nonempty family satisfying (B)}.$$

The right-hand side says: for every linear perturbation $p$, the set of $\omega[-p]$-maximal bases is again the base family of a matroid. The universal quantifier over $p$ is not optional — a version of this statement quantified over a single fixed $p$ is either vacuous or false, and does not capture what makes valuated matroids useful.

Milestone: Theorem 2.29 (the base-family / rank-function correspondence)

The maps

$$\rho(X) = \max\{|X \cap J| : J \in \mathcal B\}, \qquad \mathcal B = \{J \subseteq V : \rho(J) = |J| = \rho(V)\}$$

are mutually inverse bijections between nonempty families satisfying (B) and set functions satisfying (R1)-(R3). This is weaker groundwork than the goal, stated first because it fixes the exact axiomatic vocabulary — (B) and (R) — that Theorem 2.32 is built on.

Significance

The result itself. Theorem 2.32 is the reason valuated matroids are the right object for weighted combinatorial optimization on matroids: it says a function on bases behaves correctly under every linear re-weighting of the ground set exactly when it satisfies the local exchange inequality (VM). This is what guarantees, for instance, that a greedy algorithm which is correct for the unweighted matroid extends correctly to families of tilted objectives, and it is the germ of the general local-optimality criterion for M-convex functions (chapters 6–7), which underlies most of the algorithmic content of the rest of the book. Theorem 2.29 is the classical result — due jointly to the development of matroid theory from the 1930s onward — that the base-exchange and rank-submodularity axiomatizations of a matroid carry the same information; it is the finite, unweighted precursor of Theorem 2.32.

Formalizing it. Neither theorem has a machine-checked proof on the platform prior to this mission (see Formalization scope for the prior-art check). Theorem 2.29's own proof is elementary but has two independent halves (each map preserves its target axiom class, and the two maps compose to the identity in both directions) that must all be established; Theorem 2.32's proof, as given in the source, defers entirely to a later, more general chapter-6 theorem, so a solver working only from this mission must either reconstruct a direct combinatorial argument for this special case or await chunk 06 (DiscreteConvex.MConvexFunctions, a separate mission) and specialize its main theorem.

Difficulty

The obvious approach to Theorem 2.32 — fix an optimal basis $J$ for $\omega[-p]$ and try to show the exchange condition on maximizers directly from (VM) — proves one direction (VM implies the maximizer property) in a few lines, since perturbing does not change which exchange moves are available. The converse is the substantial direction: from "the maximizer set is always a matroid, for every $p$," one must recover the single global inequality (VM) that must hold for all pairs $J, J' \in \mathcal B$, not just optimal ones. The standard argument constructs, for a given non-optimal pair, a perturbation $p$ under which that specific pair becomes simultaneously optimal, and this construction is exactly the step the book skips by citing chapter 6's general theorem. A formalization attempting to bypass this by only checking the maximizer property for a finite or generic sample of perturbations would trivialize the statement to something false or vacuous — a pitfall the goal's explicit ∀ p is designed to prevent.

Formalization scope

The ground set $V$ is a Fintype with DecidableEq; $2^V$ is represented as Finset (Finset V), and $V \to \mathbb R$ as a plain function type. The rank function is $\mathbb Z$-valued (matching the book's own convention for matroid rank, as opposed to the $\mathbb R$-valued conventions used from chapter 6 onward for general M-convex functions); RankOfFamily is implemented with Finset.sup over $\mathbb N$ rather than a partial max', so that it is a total function — its junk value at the empty family is never invoked, since every hypothesis in this mission supplies nonemptiness explicitly, matching the book's own phrasing.

A trivializing formalization of the goal is one that quantifies over a single fixed $p$, or allows $\mathcal B$ to be empty; both are explicitly excluded by keeping $\mathcal B.\text{Nonempty}$ a hypothesis and $p$ universally quantified inside the theorem statement itself.

Checked against Mathlib (commit 0df444a360eaa60ab8c11dca51a86af692955474): Mathlib's Matroid structure is axiomatized via the single-element (asymmetric) exchange property, classically but not definitionally equivalent to Murota's simultaneous axiom (B) used throughout this book, and Mathlib provides no constructor recovering a base family or a Matroid from a bare rank function satisfying (R1)-(R3). Theorem 2.29 is therefore genuine, reusable infrastructure, not a restatement of existing Mathlib API. No reference item was found on the platform for either theorem (GET /theorems?q=matroid, q=valuated matroid return only unrelated tropical-geometry and k-server results). Contributions to a shared DiscreteConvex.Combinatorial definitions layer (the exchange and rank axioms) are welcome from later chunks of this series that build on matroid or base-polyhedron structure.

Selected references

• K. Murota, Discrete Convex Analysis, SIAM, 2003. DOI: 10.1137/1.9780898718508.
• H. Whitney, "On the abstract properties of linear dependence," American Journal of Mathematics, 57(3), 1935, pp. 509–533.
• A. W. M. Dress, W. Wenzel, "Valuated matroids," Advances in Mathematics, 93(2), 1992, pp. 214–250.
• R. A. Brualdi, "Comments on bases in dependence structures," Bulletin of the Australian Mathematical Society, 1(2), 1969, pp. 161–167.

Motivation

Many equivalence problems on finite structures reduce to computing the coarsest partition of a finite set that is compatible with a relation. Deciding whether two states of a finite labelled transition system are bisimilar, testing congruence of finite-state processes in Milner's calculus of communicating systems (CCS), and minimizing a deterministic finite automaton are all instances. Kanellakis and Smolka studied the relational version in connection with CCS equivalence and gave an $O(mn)$-time algorithm, conjecturing that $O(m \log n)$ was possible. Paige and Tarjan's 1987 paper answers that conjecture with an algorithm that has since become the standard method for bisimulation minimization in model checkers and process-algebra tools.

Timeline:

• 1971 — Hopcroft gives an $O(n \log n)$ algorithm for minimizing deterministic finite automata, i.e. for the coarsest partition stable with respect to one or more functions, using the rule "process the smaller half".
• 1983/1990 — Kanellakis and Smolka give an $O(mn)$-time, $O(m + n)$-space algorithm for the relational problem, and $O(c^2 n \log n)$ when every element has at most $c$ successors; they conjecture an $O(m \log n)$ algorithm.
• 1987 — Paige and Tarjan combine Hopcroft's smaller-half strategy with refinement by unions of blocks and obtain $O(m \log n)$ time and $O(m + n)$ space for the relational problem.

Setting

Let $U$ be a finite set with $n = |U|$ elements and let $E \subseteq U \times U$ be a binary relation on $U$; write $xEy$ for $(x, y) \in E$ and $m = |E|$. For $S \subseteq U$ the preimage of $S$ is

$$E^{-1}(S) = \{x \in U \mid \exists y \in S,\ xEy\}.$$

A partition of $U$ is a family of nonempty, pairwise disjoint subsets of $U$, its blocks, whose union is $U$. A partition $R$ is a refinement of a partition $P$ if every block of $R$ lies inside a block of $P$.

A set $B \subseteq U$ is stable with respect to $S \subseteq U$ if $B \subseteq E^{-1}(S)$ or $B \cap E^{-1}(S) = \emptyset$: either every element of $B$ has an $E$-successor in $S$, or none does. A partition is stable with respect to $S$ if all its blocks are, and a partition is stable if it is stable with respect to each of its own blocks.

Given $E$ and an initial partition $P$, the coarsest stable refinement of $P$ is a stable partition $Q$ refining $P$ such that every stable partition refining $P$ is a refinement of $Q$. The relational coarsest partition problem asks for it.

The algorithms refine by the operation $\mathrm{split}(S, Q)$, which replaces each block $B$ of $Q$ that meets both $E^{-1}(S)$ and its complement by the two blocks $B \cap E^{-1}(S)$ and $B - E^{-1}(S)$. The set $S$ is a splitter of $Q$ if $\mathrm{split}(S, Q) \neq Q$.

• The naïve algorithm starts from $Q = P$ and, while possible, picks a splitter $S$ of $Q$ that is a union of blocks of $Q$ and replaces $Q$ by $\mathrm{split}(S, Q)$.
• The improved algorithm also maintains a partition $X$, initially $\{U\}$, of which $Q$ is a refinement. While $Q \neq X$, it picks a block $S \in X$ that is not a block of $Q$ and a block $B \in Q$ with $B \subseteq S$ and $|B| \le |S|/2$, replaces $S$ in $X$ by $B$ and $S - B$, and replaces $Q$ by $\mathrm{split}(S - B, \mathrm{split}(B, Q))$.

The improved algorithm is analysed under the standing assumption $|E(\{x\})| \ge 1$ for all $x \in U$: every element has at least one successor. (The paper reduces the general case to this one by a preprocessing step.)

Formalization targets

Goal: the improved algorithm

For every run $(Q_0, X_0) = (P, \{U\}), \dots, (Q_K, X_K)$ of the improved algorithm with refining blocks $B_0, \dots, B_{K-1}$:

1. at every stage $Q_j$ and $X_j$ are partitions, $Q_j$ refines $X_j$, and $Q_j$ is stable with respect to every block of $X_j$;
2. if $Q_K = X_K$, then $Q_K$ is the coarsest stable refinement of $P$;
3. if $Q_K \neq X_K$, another step applies;
4. $K \le n - 1$;
5. every $x \in U$ satisfies

$$\#\{\, j < K \mid x \in B_j \,\} \le \log_2 n + 1.$$

Items 1–4 are the correctness of the improved algorithm, which the paper deduces from that of the naïve one. Item 5 is the counting fact on which the $O(m \log n)$ bound rests.

Milestones

• §3, p. 978: $S$ is a splitter of $Q$ if and only if $Q$ is unstable with respect to $S$.
• Properties (1)–(3), p. 978: stability is inherited under refinement and under union; $\mathrm{split}$ is monotone in its second argument.
• §3, p. 979: a stable partition is stable with respect to every union of its blocks.
• Lemma 2, p. 979: every stable refinement of $P$ refines each partition produced by the naïve algorithm.
• Theorem 2, p. 979: the naïve algorithm stops after at most $n - 1$ steps at the unique coarsest stable refinement.
• Property (4), p. 978: $\mathrm{split}$ is commutative, and $\mathrm{split}(S, \mathrm{split}(Q, P))$ is the coarsest refinement of $P$ stable with respect to both $S$ and $Q$.
• Lemma 3, p. 980: the three-way split of a block $D$ into $D_{11}$, $D_{12}$ and $D_2$, including $D_{12} = D_1 \cap (E^{-1}(B) - E^{-1}(S - B))$.

Significance

The coarsest stable refinement of the partition of states by their labels is the bisimilarity relation of a finite transition system, so the goal certifies, for any sequence of choices, the correctness of the refinement loop at the core of bisimulation minimization. The halving count is the combinatorial half of the $O(m \log n)$ bound: once the implementation charges $O(|B| + \sum_{y \in B} |E^{-1}(\{y\})|)$ per refining block $B$, the count bounds the total work.

The results are proved in the paper, some by one-line arguments and the elementary properties (1)–(4) not at all ("stated without proof"). No machine-checked proof of the Paige–Tarjan algorithm's correctness or of its halving count is known to be available in Lean or Mathlib. The mission produces a checked account of the invariant, the final correctness and the counting argument for every run, not only for a particular implementation.

Difficulty

The correctness of the improved algorithm is not a special case of the naïve one read off directly. An improved step refines by $B$ and by $S - B$, and $S - B$ is a union of blocks of $Q$ only because $Q$ refines $X$. The invariant that $Q$ is stable with respect to every block of $X$ is what makes $Q = X$ a stopping condition, and it holds initially only under the standing assumption. The naive idea of reusing Hopcroft's argument fails: for relations, stability with respect to $S$ and $B$ does not imply stability with respect to $S - B$, which is why both refinements are performed. For the halving count, the refining blocks that contain a fixed element must be shown to be nested across steps, which requires tracking how blocks of $X$ are replaced.

Formalization scope

• $U$ is a Fintype with decidable equality, $E$ a decidable relation U → U → Prop. Partitions are Finset (Finset U) with an explicit predicate IsPartition (nonempty, pairwise disjoint blocks covering $U$); blocks are required to be nonempty, which the paper leaves implicit.
• "Coarsest" means: every stable partition refining $P$ refines it. The paper's "every other stable partition" is read this way, since a stable partition that does not refine $P$ need not refine the answer.
• Algorithms are step relations; a run is a finite sequence of states indexed by Fin (K + 1), with the choices $S_j, B_j$ recorded. Every statement holds for every run, so no choice rule is fixed.
• Added hypotheses: $U$ nonempty (so $\{U\}$ is a partition and "at most $n - 1$ steps" is meaningful); the standing assumption $\forall x\, \exists y,\ xEy$ for the goal only. Lemma 2 is stated for every stable refinement of $P$, which is what its proof gives and what Theorem 2 uses; it implies the printed form.
• Explicit forms: $|B| \le |S|/2$ is 2 * B.card ≤ S.card, $K \le n - 1$ is K + 1 ≤ n, $\log_2$ is Real.logb 2 of $n$ cast to $\mathbb{R}$. The termination bound for the improved algorithm is not printed in the paper and is derived as in the proof of Theorem 2. Running times ($O(mn)$, $O(m \log n)$) and the data structures of the implementation are out of scope.
• A trivializing reading is ruled out: the goal quantifies over all runs from $(P, \{U\})$ with every side condition of the step (in particular $S \notin Q$ and the half-size condition), and the conclusion is a full correctness statement, not the existence of some stable partition; the discrete partition is stable but is not the answer in general.
• Reusable beyond this mission: preimage, stability, $\mathrm{split}$ and its algebra (properties (1)–(4)), which apply to Hopcroft's algorithm and to bisimulation minimization in general. Contributions proving the elementary properties first, then Lemma 2 and Theorem 2, are the natural attack order.

Selected references

• R. Paige, R. E. Tarjan, Three Partition Refinement Algorithms, SIAM Journal on Computing 16(6):973–989, 1987. https://doi.org/10.1137/0216062
• P. C. Kanellakis, S. A. Smolka, CCS expressions, finite state processes, and three problems of equivalence, Information and Computation 86(1):43–68, 1990. https://doi.org/10.1016/0890-5401(90)90025-D
• J. E. Hopcroft, An n log n algorithm for minimizing states in a finite automaton, in Theory of Machines and Computations, Academic Press, 1971, pp. 189–196. https://doi.org/10.1016/B978-0-12-417750-5.50022-1
• A. V. Aho, J. E. Hopcroft, J. D. Ullman, The Design and Analysis of Computer Algorithms, Addison-Wesley, 1974.

Motivation

The traveling salesman problem with the triangle inequality asks for a shortest closed tour through $n$ points whose distances form a metric. It is NP-hard, so in practice tours are built by fast construction heuristics, and the natural question is how far such a tour can be from optimal in the worst case. Rosenkrantz, Stearns and Lewis (SIAM J. Comput. 6(3), 1977) gave the first systematic worst-case analysis of the standard heuristics. Their results are reproduced in textbooks on approximation algorithms and combinatorial optimization, and they are the reference point against which later guarantees (Christofides' $3/2$ algorithm, the double-tree $2$-approximation) are compared.

The simplest heuristic studied is the nearest neighbor algorithm (Bellmore and Nemhauser, 1968; the "next best method" of Gavett, 1965): from the current node, always move to the closest node not yet visited, and return to the start at the end. The paper shows that this greedy rule is never worse than logarithmic (Theorem 1) and that the logarithm cannot be removed (Theorem 2). This mission is about Theorem 2, the lower bound.

Setting

A traveling salesman graph on $n$ nodes is a complete graph with a distance $d(a,b)\in\mathbb R$ that is symmetric, $d(a,b)=d(b,a)$, nonnegative, $d(a,b)\ge 0$, and satisfies the triangle inequality $d(a,c)\le d(a,b)+d(b,c)$. A tour lists the nodes in a visiting order $\tau(0),\dots,\tau(n-1)$ and returns to $\tau(0)$; its length is the sum of the $n$ distances along it. OPTIMAL is the least length of a tour.

The nearest neighbor algorithm starts at an arbitrary node $\tau(0)$; having reached $\tau(k)$, it moves to a node $\tau(k+1)$ that minimizes $d(\tau(k),\cdot)$ over the nodes not yet visited, breaking ties arbitrarily; after the last node it returns to $\tau(0)$. The length of the resulting tour is written NEARNEIBER. Because the start node and the ties are free, one instance has in general several nearest-neighbor tours. A lower bound needs only one of them; an upper bound must hold for all.

The instances of the proof are built from a recursive family of weighted graphs. With $l_i=\frac16(4\cdot 2^i-(-1)^i+3)$ (so $l_1,l_2,l_3,l_4=2,3,6,11$), the graph $F_1$ is a triangle with unit weights, and $F_{i+1}$ consists of two copies of $F_i$ joined through one new node by two edges of length $1$ and two edges of length $l_i$. Each $F_i$ has $2^{i+1}-1$ nodes and a path $P_i$ from its start node to its middle node through every node, of length $L_i$ with $L_1=2$, $L_{i+1}=2L_i+2l_i$. The graph $G_i$ adds two closing edges to $F_i$, and $\bar G_i$ is the complete graph on the same nodes whose distance is the shortest-path distance of $G_i$.

Formalization targets

Goal: Theorem 2 (p. 566)

For each $m>3$ there is a traveling salesman graph with $n=2^m-1$ nodes and a nearest-neighbor tour on it such that

$$\frac{\mathrm{NEARNEIBER}}{\mathrm{OPTIMAL}}>\frac13\lg(n+1)+\frac49 .$$

The statement is existential in both the instance and the run of the algorithm, exactly as in the paper.

Milestones, in the order the proof uses them

1. (2.12): the difference equation $L_{i+1}=2L_i+2l_i$, $L_1=2$, has the solution $L_i=\frac19(6\,i\,2^i+8\cdot2^i+(-1)^i-9)$.
2. $\bar G_i$ is a traveling salesman graph: the shortest-path distance of $G_i$ is symmetric, nonnegative and satisfies the triangle inequality.
3. (2.13)–(2.17): the shortest-path distances in $F_{i+1}$ between the seven named nodes $A,\dots,G$ of Fig. 1, e.g. $\overline{AG}=l_{i+2}-2$.
4. Property a): every edge of $G_i$ is a shortest path between its endpoints.
5. Property b): the nearest neighbor algorithm started at the start node of $\bar G_i$ can follow $P_i$ and return along the edge of length $l_i-1$.
6. The optimal tour: $\mathrm{OPTIMAL}(\bar G_i)=2^{i+1}-1$.
7. The exact ratio: the tour along $P_i$ has length $L_i+l_i-1$, so its ratio is $(L_i+l_i-1)/n$.
8. The inequality: $(L_i+l_i-1)/n>\frac13\lg(n+1)+\frac49$ for $i\ge3$.

The instance for $m$ is $\bar G_{m-1}$.

Significance

Theorem 1 of the same paper shows $\mathrm{NEARNEIBER}/\mathrm{OPTIMAL}\le\frac12\lceil\lg n\rceil+\frac12$ for every nearest-neighbor tour on every traveling salesman graph. Theorem 2 shows that this bound has the right order: no constant-factor guarantee holds for the nearest neighbor rule, and the gap between the two constants ($\frac13$ against $\frac12$) is all that remains. This separates the nearest neighbor rule from the insertion rules analysed later in the same paper, of which nearest and cheapest insertion are within a factor $2$ of optimal. It is the standard example of a natural greedy heuristic whose approximation ratio grows with $n$.

The upper bound, Theorem 1, is already on Prove2Me with a machine-checked proof (SupplyChainTheory.nearest_neighbor_bound); its statement notes that the lower-bound instances are not formalized there. This mission supplies them: an explicit recursive family of metric instances, the shortest-path computations that certify it, and the arithmetic of its ratio. The result is proved in the paper; to our knowledge it has not been formalized in any proof assistant. The construction (a recursively defined weighted graph with a closed-form shortest-path table) is also a reusable pattern for other worst-case lower bounds of greedy heuristics.

Difficulty

The arithmetic ((2.12) and the final inequality) is routine. The content is in properties a) and b). A shortest-path distance is an infimum over all walks, and property a) asks that no detour through the recursive structure is shorter than the direct edge, at every level of the recursion. The paper handles this by an induction on (2.13)–(2.17) that tracks only seven nodes per level, and argues that distances inside a copy of $F_i$ are not shortened by embedding it into $F_{i+1}$. Property b) then needs that at each step of $P_i$ the chosen node is at least as close as every unvisited node, including nodes in the other copy and nodes reached through the start or right nodes; ties occur, and the claim is only that some resolution of them follows $P_i$. Checking small cases by computer does not give either property for all $i$.

Formalization scope

Nodes of an instance are Fin n, a tour is a permutation of Fin n, the tour length is the sum over consecutive pairs including the closing edge, and OPTIMAL is a minimum over the finite set of permutations. The model is the paper's: symmetric, nonnegative distances with the triangle inequality. The distance structure also carries $d(a,a)=0$, a normalization not in the paper; the diagonal never enters a tour length. A nearest-neighbor tour is a permutation in which each step goes to a node at least as close as every unvisited node, from an arbitrary start with arbitrary ties.

Ratios are multiplied out: the goal is $(\frac13\log_2(n+1)+\frac49)\cdot\mathrm{OPTIMAL}<\mathrm{NEARNEIBER}$ together with $\mathrm{OPTIMAL}>0$, the paper's standing assumption (1.1). $\lg(n+1)$ is Real.logb 2 of $n+1$, as printed. Because of the strict inequality and the conjunct $\mathrm{OPTIMAL}>0$, the all-zero distance does not satisfy the goal, so the statement cannot be met by a degenerate instance.

In the construction the nodes of $F_i$, $G_i$, $\bar G_i$ are numbered $0,\dots,2^{i+1}-2$ from left to right (start node $0$, middle node $2^i-1$, right node $2^{i+1}-2$); in $F_{i+1}$ the left copy comes first, then the new node, then the right copy. Graphs are edge lists with real weights and $l_i$ is defined in $\mathbb R$ exactly as in (2.11). The shortest-path distance is the infimum of walk weights over an inductive walk predicate; it would be $0$ for two nodes with no connecting walk, a case that does not arise because every $G_i$ and $F_i$ is connected. $L_i$ is defined by its difference equation; its identification with the length of the tour along $P_i$ is milestone 7. All construction statements assume $i\ge1$.

A complete development needs a small library for shortest-path distances of finite weighted edge lists (symmetry, triangle inequality, attainment, behaviour under relabelling and under gluing two graphs at a few nodes); this part is reusable beyond the mission. Contributions welcome: proofs of any milestone, and such general shortest-path lemmas as separate theorems. Theorem 1 is not part of this mission.

Selected references

• D. J. Rosenkrantz, R. E. Stearns, P. M. Lewis II, An Analysis of Several Heuristics for the Traveling Salesman Problem, SIAM J. Comput. 6(3):563–581, 1977. https://doi.org/10.1137/0206041
• M. Bellmore, G. L. Nemhauser, The Traveling Salesman Problem: A Survey, Operations Research 16(3):538–558, 1968. https://doi.org/10.1287/opre.16.3.538
• J. W. Gavett, Three Heuristic Rules for Sequencing Jobs to a Single Production Facility, Management Science 11(8):B166–B176, 1965. https://doi.org/10.1287/mnsc.11.8.B166
• N. Christofides, Worst-Case Analysis of a New Heuristic for the Travelling Salesman Problem, Report 388, Graduate School of Industrial Administration, Carnegie Mellon University, 1976.

Motivation

Bin packing asks for the fewest unit-capacity bins that hold a given list of item sizes. It models cutting stock, memory allocation, file placement and the loading of trucks, and it is NP-hard, so in practice lists are packed by simple rules that look at one item at a time. The two most widely used rules are First-Fit and Best-Fit, and the question that Johnson, Demers, Ullman, Garey and Graham answered in 1974 is how far from optimal they can be in the worst case.

Their headline answer is that both rules use at most about $\tfrac{17}{10}$ times the optimal number of bins, and that $\tfrac{17}{10}$ is asymptotically attained. The lists that force this ratio use items larger than $\tfrac12$. When all items are known to be small, which is typical of memory and storage applications, the guarantee is much better, and this mission is about that refinement: the paper's Theorem 2.3 and its corollary, which determine the asymptotic worst-case ratio of First-Fit and Best-Fit exactly as a function of the largest allowed item size $\alpha\le\tfrac12$.

Timeline. Ullman (1971) introduced the worst-case analysis of First-Fit with a $\tfrac{17}{10}L^*+3$ bound. Garey, Graham and Ullman (1972) and Johnson's thesis (MIT, 1973) extended it to Best-Fit and to the decreasing variants. The 1974 SIAM paper collects these results; Theorem 2.3 there is the parametric bound for items of size at most $\alpha$. The additive constants in the unrestricted $\tfrac{17}{10}$ bound were sharpened over the following four decades, culminating in Dósa and Sgall's proof (2013) that $FF(L)\le\lfloor\tfrac{17}{10}L^*\rfloor$.

Setting

A list is a finite sequence $L=(a_1,\dots,a_n)$ of real numbers in $(0,1]$. Its optimum $L^*$ is the least number of bins into which the elements of $L$ can be placed so that no bin contains numbers whose sum exceeds $1$. The level of a bin is the sum of the numbers in it. For a real $\alpha>0$, write $L\subseteq(0,\alpha]$ when every element of $L$ is at most $\alpha$.

First-Fit ($FF$) considers bins $B_1,B_2,\dots$, all initially empty, and places $a_1,a_2,\dots,a_n$ in that order: $a_i$ goes into the bin $B_j$ of least index whose level $\beta$ satisfies $\beta\le 1-a_i$. Best-Fit ($BF$) is the same except that, among the bins with $\beta\le 1-a_i$, it chooses one of largest level $\beta$ (least index among ties). $FF(L)$ and $BF(L)$ denote the numbers of nonempty bins at the end.

The restricted worst-case ratios are

$$R^\alpha_{FF}(k)=\max\Big\{\frac{FF(L)}{L^*}: L\subseteq(0,\alpha],\ L^*=k\Big\},\qquad R^\alpha_{BF}(k)=\max\Big\{\frac{BF(L)}{L^*}: L\subseteq(0,\alpha],\ L^*=k\Big\}.$$

Throughout, $0<\alpha\le\tfrac12$ and $m=\lfloor\alpha^{-1}\rfloor$, an integer with $m\ge 2$ and $\tfrac1{m+1}<\alpha\le\tfrac1m$.

Formalization targets

Goal: the asymptotic ratio (Corollary of Theorem 2.3, p. 308)

$$\lim_{k\to\infty}R^\alpha_{FF}(k)=\lim_{k\to\infty}R^\alpha_{BF}(k)=1+\frac{1}{\lfloor\alpha^{-1}\rfloor}.$$

The goal is stated as a limit, which is the stable form of the result: it is unaffected by any improvement of the additive constants below.

Theorem 2.3(i): the lower bound (p. 307)

For each $k\ge1$ there is a list $L\subseteq(0,\alpha]$ with $L^*=k$ and $FF(L)\ge\frac{m+1}{m}L^*-\frac1m$; likewise for $BF$.

Two steps of the First-Fit upper bound (p. 308)

If no element of $L$ exceeds $\frac1m$, then in the First-Fit packing every bin except possibly the last contains at least $m$ elements, and all but at most two bins have level at least $\frac{m}{m+1}$.

Theorem 2.3(ii): the upper bounds (p. 307)

For every list $L\subseteq(0,\alpha]$,

$$FF(L)\le\frac{m+1}{m}L^*+2,\qquad BF(L)\le\frac{m+1}{m}L^*+2.$$

Significance

The theorem gives an exact, parametric description of how the worst case of the two greedy rules improves as items shrink: the asymptotic ratio is $\tfrac32$ when items are at most $\tfrac12$, $\tfrac43$ when at most $\tfrac13$, and tends to $1$ as the maximum item size tends to $0$. Combined with the $\tfrac{17}{10}$ bound for unrestricted lists, it shows that the bad behaviour of First-Fit is caused entirely by items larger than $\tfrac12$. Such parametric bounds are the standard way bin-packing heuristics are compared in the literature on online and semi-online packing, and the construction in part (i) is a reusable template for lower-bound lists.

The paper proves the First-Fit upper bound and the lower bound (the verification of the lower-bound construction is left to the reader). The Best-Fit upper bound is stated but not proved: the paper says only that "a similar, but slightly more complicated, argument can be used". A formal proof of the goal therefore requires supplying that argument. None of these results is known to have a machine-checked proof; Mathlib contains no bin-packing development.

Difficulty

For First-Fit the upper bound is a counting argument, but it rests on a property of the run, not of the final packing: an item that went into a later bin did not fit into an earlier bin at the moment it was placed. Turning that into a statement about the final levels requires an invariant maintained through the whole sequence of placements.

The Best-Fit upper bound is harder because that property fails: Best-Fit may put a small item into a fuller, later bin while an earlier, lighter bin still has room, so a light early bin and a light later bin can coexist longer than under First-Fit. The paper gives no argument for this case.

The lower bound requires computing the exact behaviour of both algorithms on a specific interleaved list with item sizes perturbed by powers of $m$, and computing $L^*$ exactly for that list, which needs a matching lower bound on the optimum.

Formalization scope

A list is L : List ℝ with the hypothesis IsList L (every element in $(0,1]$); $L\subseteq(0,\alpha]$ is the additional hypothesis ∀ a ∈ L, a ≤ α. $L^*$ is optBins L, a sInf in ℕ over numbers of bins admitting a feasible assignment; the hypothesis IsList makes the set nonempty. The runs ffPack L and bfPack L are folds over the list that keep the nonempty bins in the order they were opened, each with its contents; an item that fits nowhere opens a new bin at the end, which is the paper's "least $j$" over infinitely many empty bins. Comparisons are exact (classical decidability on ℝ), and $FF(L)$, $BF(L)$ are the lengths of the final bin lists. $m$ is Nat.floor α⁻¹, cast before any division.

The ratios $R^\alpha_{FF}(k)$, $R^\alpha_{BF}(k)$ are suprema taken in ℝ≥0∞: an unbounded family would give $+\infty$, never a default value, and at $k=0$ the only admissible list is empty and the value is $0$. The goal is a Tendsto … atTop (𝓝 (1 + (⌊α⁻¹⌋₊)⁻¹)) statement in ℝ≥0∞. A real-valued sSup would have returned $0$ on an unbounded family and made a false bound look provable; that encoding is ruled out. The upper bounds keep the additive constant $2$ and the lower bound the subtractive $\frac1m$ exactly as printed.

The two proof steps are stated under the proof's own hypothesis "no element exceeding $1/m$", which is weaker than $L\subseteq(0,\alpha]$.

A complete development needs invariants of the First-Fit and Best-Fit folds, a lower bound $L^*\ge\sum_i a_i$, and exact evaluation of both runs on the construction of part (i). Lemmas about the fold encoding of First-Fit and Best-Fit and about $L^*$ are reusable in the companion missions on the $\tfrac{17}{10}$, $\tfrac{11}{9}$ and $\tfrac{71}{60}$ bounds of the same paper. Contributions on the Best-Fit upper bound are especially welcome, since the source gives no proof.

Selected references

• D. S. Johnson, A. Demers, J. D. Ullman, M. R. Garey, R. L. Graham, Worst-Case Performance Bounds for Simple One-Dimensional Packing Algorithms, SIAM Journal on Computing 3(4):299–325, 1974. https://doi.org/10.1137/0203025
• J. D. Ullman, The Performance of a Memory Allocation Algorithm, Technical Report 100, Princeton University, 1971.
• M. R. Garey, R. L. Graham, J. D. Ullman, Worst-Case Analysis of Memory Allocation Algorithms, Proc. 4th ACM Symposium on Theory of Computing, 143–150, 1972. https://doi.org/10.1145/800152.804907
• D. S. Johnson, Near-Optimal Bin Packing Algorithms, PhD thesis, Massachusetts Institute of Technology, 1973. http://hdl.handle.net/1721.1/57819
• G. Dósa, J. Sgall, First Fit Bin Packing: A Tight Analysis, Proc. 30th STACS, LIPIcs 20:538–549, 2013. https://doi.org/10.4230/LIPIcs.STACS.2013.538

Motivation

The uncapacitated facility location (UFL) problem is one of the basic models of location theory and operations research: a firm chooses which warehouses, plants or servers to open, paying a fixed cost for each open site and a service cost for every client according to its distance to the nearest open site. It is also a standard test case for approximation algorithms.

Local search is the simplest of these and the one most used in practice: start from any set of open facilities and repeatedly add, drop or exchange one facility while this lowers the cost. The question is how bad a solution can be when no such move helps. Arya, Garg, Khandekar, Meyerson, Munagala and Pandit (SIAM J. Comput. 33(3), 2004) answered it for UFL with an exact constant.

Timeline. Korupolu, Plaxton and Rajaraman (SODA 1998, J. Algorithms 2000) analysed local search with add, drop and swap moves and proved a locality gap of at most 5; their analysis contains the service cost bound restated here as Lemma 4.1. Charikar and Guha (FOCS 1999) proved a locality gap of 3 for a different local search, in which one facility is added and any number are dropped. Arya et al. (STOC 2001; journal version 2004) proved that the add/drop/swap neighbourhood itself has locality gap at most 3, and gave an instance showing that 3 cannot be improved (§4.3).

Setting

A metric instance consists of a finite set $C$ of clients, a finite set $F$ of facilities, and a distance $d$ on $C \cup F$ that is nonnegative, symmetric and satisfies the triangle inequality. The cost of serving client $j$ by facility $i$ is $c_{ji} = d(j,i)$; the distance $c_{ii'}$ between two facilities is also available. Each facility $i \in F$ has an opening cost $f_i \ge 0$.

A solution is a nonempty set $S \subseteq F$ of open facilities. Every client is served by its nearest open facility, so

$$\mathrm{cost}_f(S) = \sum_{i \in S} f_i, \qquad \mathrm{cost}_s(S) = \sum_{j \in C} \min_{i \in S} c_{ji}, \qquad \mathrm{cost}(S) = \mathrm{cost}_f(S) + \mathrm{cost}_s(S).$$

The neighbourhood of $S$ is the set of solutions reachable by adding one facility, dropping one facility, or swapping one open facility for another:

$$\mathcal B(S) = \{S + \{s'\}\} \cup \{S - \{s\} \mid s \in S\} \cup \{S - \{s\} + \{s'\} \mid s \in S\}.$$

$S$ is locally optimum if $\mathrm{cost}(S) \le \mathrm{cost}(S')$ for every $S' \in \mathcal B(S)$. The locality gap is the supremum, over all instances, of the ratio between the cost of a worst local optimum and the cost of a global optimum.

The proofs use the following notation, which appears in the milestones but not in the goal. Fix a second solution $O$ and nearest-facility assignments $\sigma_S : C \to S$, $\sigma_O : C \to O$; write $S_j = c_{j\sigma_S(j)}$, $O_j = c_{j\sigma_O(j)}$, $N_S(s) = \sigma_S^{-1}(s)$, $N_O(o) = \sigma_O^{-1}(o)$ and $N^o_s = N_O(o) \cap N_S(s)$. A facility $s \in S$ captures $o \in O$ if $|N^o_s| > \tfrac12 |N_O(o)|$; $s$ is good if it captures no facility of $O$ and bad otherwise. The proof of the facility cost bound uses a permutation $\pi$ of the clients that maps each $N_O(o)$ onto itself, moves every client of a non-capturing block $N^o_s$ out of that block (Property 3.1), and fixes every client of a capturing block that it would map into the same block.

Formalization targets

Goal: Theorem 4.3

$$\mathrm{cost}(S) \le 3 \cdot \mathrm{cost}(O) \quad \text{for every locally optimum } S \text{ and every solution } O.$$

This is the locality gap bound of Theorem 4.3 (p. 557) in its strongest printed form: $O$ is any solution, not only an optimal one.

Milestones

1. Lemma 4.1 (service cost), p. 554: $\mathrm{cost}_s(S) \le \mathrm{cost}_f(O) + \mathrm{cost}_s(O)$.
2. The refined mapping $\pi$ of the proof of Lemma 4.2, p. 555: such a permutation exists for any two assignments.
3. Inequality (5), p. 555: the drop move for a good facility $s$,

$$-f_s + \sum_{j \in N_S(s),\ \pi(j) \neq j} (O_j + O_{\pi(j)} + S_{\pi(j)} - S_j) + 2 \sum_{j \in N_S(s),\ \pi(j) = j} O_j \ge 0.$$

4. Inequality (6), pp. 555–556: the swap of a bad facility $s$ with the facility $o$ it captures that is nearest to it.
5. Inequality (8), p. 556: for a bad facility $s$ capturing the set $P \subseteq O$, the analogue of (5) with $\sum_{o' \in P} f_{o'} - f_s$ in place of $-f_s$.
6. Lemma 4.2 (facility cost), p. 555: $\mathrm{cost}_f(S) \le \mathrm{cost}_f(O) + 2 \cdot \mathrm{cost}_s(O)$.

A companion item, not a milestone, states the bound in the proof of Theorem 4.4 with $\alpha = \sqrt2$: a local optimum of the instance with facility costs $\sqrt2 f_i$ costs at most $(1+\sqrt2)\,\mathrm{cost}(O)$ in the original instance.

Significance

The result. Theorem 4.3 shows that the simplest local search for metric UFL is within a factor 3 of optimal at every local optimum, with no LP and no rounding, and the tight example of §4.3 shows the analysis cannot be improved for this neighbourhood. Because Lemmas 4.1 and 4.2 hold against every solution $O$, scaling the facility costs before running local search trades the two bounds against each other and gives the $1 + \sqrt2 + \epsilon$ guarantee of Theorem 4.4. The same capture-and-reassign technique is used for k-median (§3) and capacitated facility location (§5).

Formalizing it. The theorem is proved on paper; no machine-checked proof of it or of any locality gap bound for facility location is known to this mission. A formal development would check the reassignment arguments, which are stated case by case in the paper, and would produce reusable Lean infrastructure for metric facility location instances, nearest-facility costs and neighbourhood-based local optimality.

Difficulty

The service cost bound is routine; the facility cost bound is where the work lies. The natural first idea, closing a facility $s \in S$ and sending each of its clients to the facility of $S$ nearest to that client's optimal facility, fails when $s$ serves most of the clients of some $o \in O$: the nearest facility of $S$ to $o$ may be $s$ itself, so the client has nowhere to go. The proof separates good facilities, which can be dropped, from bad ones, which must be swapped with a captured facility, and pays for the clients that cannot be moved through the distance between $s$ and its nearest captured facility. The combinatorial core is the construction of a permutation within each $N_O(o)$ that avoids every non-capturing block and has fixed points only where they are unavoidable.

Formalization scope

Clients and facilities are finite types Cl and Fa. The distance is a real-valued function on Cl ⊕ Fa that is nonnegative, symmetric and satisfies the triangle inequality; $d(x,x) = 0$ is not assumed, since the paper neither states nor uses it. Opening costs are a function f : Fa → ℝ with 0 ≤ f i, and demands are unit, as in the paper.

Solutions are nonempty Finsets. The service cost is $\sum_j \min_{i \in S} c_{ji}$ (Finset.inf') and is defined only for nonempty sets, so no junk value for $\emptyset$ enters. Accordingly the drop move is considered only when a facility remains open; with at least one client, $\emptyset$ cannot serve anyone and is not a solution. Local optimality is required for all moves of $\mathcal B(S)$: every added facility, every dropped facility and every swap, not only the moves used in the proof. The goal is stated as the multiplied-out inequality $\mathrm{cost}(S) \le 3\,\mathrm{cost}(O)$ for every nonempty $O$, never as a ratio, since $\mathrm{cost}(O)$ may be $0$.

In the milestones, the nearest-facility assignments $\sigma_S$, $\sigma_O$ are arbitrary among the nearest ones (ties broken arbitrarily), and the family of bijections $\pi : N_O(o) \to N_O(o)$ is a single permutation of the clients with $\sigma_O \circ \pi = \sigma_O$. Inequality (5) assumes at least one client, which the paper assumes implicitly: with no clients and $S = \{s\}$ it would read $-f_s \ge 0$. The goal and Lemma 4.2 need no such assumption.

A statement that assumes local optimality only for the moves the proof uses, that fixes $O$ to be a global optimum defined by hypotheses, or that allows the empty set a zero service cost would be a different theorem; none of these is used.

Needed infrastructure: sums over nearest-facility assignments and their fibers $N_O(o)$, the permutation $\pi$, and bookkeeping of the three kinds of moves. The instance, cost and local optimality definitions are reusable for other local search analyses of metric location problems. Proofs of any milestone are welcome, as are alternative proofs of the goal.

Selected references

• V. Arya, N. Garg, R. Khandekar, A. Meyerson, K. Munagala, V. Pandit, Local Search Heuristics for k-Median and Facility Location Problems, SIAM J. Comput. 33(3):544–562, 2004. https://doi.org/10.1137/S0097539702416402
• M. R. Korupolu, C. G. Plaxton, R. Rajaraman, Analysis of a Local Search Heuristic for Facility Location Problems, J. Algorithms 37(1):146–188, 2000. https://doi.org/10.1006/jagm.2000.1100
• M. Charikar, S. Guha, Improved Combinatorial Algorithms for the Facility Location and k-Median Problems, FOCS 1999, 378–388. https://doi.org/10.1109/SFFCS.1999.814609

Motivation

A feedforward neural network is a directed acyclic graph of neurons, each computing a fixed scalar activation of a weighted sum of its inputs; fixing the graph and the activation and letting the weights vary gives a hypothesis class. Chapter 20 of Shalev-Shwartz and Ben-David, Understanding Machine Learning: From Theory to Algorithms (doi:10.1017/CBO9781107298019), studies these classes through the book's three lenses. Approximation: every Boolean function is implemented by a network of depth 2 (Claim 20.1), but only at exponential size (Theorem 20.2), while a sign neuron implements conjunctions and disjunctions (Lemma 20.4), the bridge to Boolean circuits and hence to everything computable in bounded time. Estimation: the VC dimension of the class of sign networks over a graph with $|E|$ edges is $O(|E|\log|E|)$ (Theorem 20.6), so the sample complexity is governed by the number of weights. Optimization: training is NP-hard even for tiny networks, and the practical answer is SGD with the gradient computed by backpropagation, whose correctness the chapter derives from the chain rule.

Setting

A layered graph has layers $V_0, \dots, V_T$, every edge joining $V_{t-1}$ to $V_t$; $V_0$ holds the $n$ inputs and a constant neuron outputting $1$. With weights $w : E \to \mathbb{R}$ and an activation $\sigma$, the outputs are computed layer by layer, $a_{t+1,i} = \sum_{j : (v_{t,j}, v_{t+1,i}) \in E} w_{t,i,j}\,o_{t,j}$ and $o_{t+1,i} = \sigma(a_{t+1,i})$. The class $H_{V,E,\sigma} = \{h_{V,E,\sigma,w} : w : E \to \mathbb{R}\}$ (20.1); for binary classification the output layer is a single neuron and $\sigma$ is the sign function, so $H_{V,E,\operatorname{sign}}$ is a set of $\{\pm1\}$-valued predictors on $\mathbb{R}^n$. The size of the network is $|V|$, its depth $T$. The growth function $\tau_H(m) = \max_{|C| \le m}|H_C|$ extends to classes with any finite codomain (p. 275), and the proof of Theorem 20.6 uses two of its properties, stated as Exercises 3 and 4: the growth function of a product class is at most the product of the growth functions, and likewise for a composition class. For backpropagation the activation is any differentiable $\sigma$ and the loss is $\frac12\|o_T - y\|^2$; the backward pass sets $\delta_T = o_T - y$ and $\delta_t = \delta_{t+1}\operatorname{diag}(\sigma'(a_{t+1}))W_t$.

Formalization targets

Goal: Theorem 20.6

The VC dimension of $H_{V,E,\operatorname{sign}}$ is $O(|E|\log|E|)$. Explicitly, for a layered graph of depth at least $1$ with a single output neuron,

$$\operatorname{VCdim}(H_{V,E,\operatorname{sign}}) \le 2|E|\log_2(16|E|),$$

stated as: every $m \le \operatorname{VCdim}$ satisfies this bound (so the VC dimension is finite).

Milestones

Claim 20.1 (the depth-2 graph with $|V_1| = 2^n + 1$ whose sign class contains every function $\{\pm1\}^n \to \{\pm1\}$); Theorem 20.2 (every sign network implementing all functions $\{0,1\}^n \to \{0,1\}$ has $2^{n/3} \le 2|V|$); Lemma 20.4 (conjunction and disjunction as sign neurons); Exercise 4 (growth function of a composition); the correctness of backpropagation (§20.6: the partial derivative for the edge $(v_{t,j}, v_{t+1,i})$ is $\delta_{t+1,i}\sigma'(a_{t+1,i})o_{t,j}$). Further items: Exercise 3 (growth function of a product) and the intermediate bound $\tau_H(m) \le (em)^{|E|}$ of the proof of Theorem 20.6.

Significance

Theorem 20.6 is the reason networks are learnable at all in the book's sense: by the fundamental theorem, a class with finite VC dimension is agnostic PAC learnable with sample complexity linear in that dimension, and here the dimension is essentially the number of tunable parameters. The proof technique, due to Kakade and Tewari's lecture notes, is a composition-and-product argument on growth functions that applies to any layered class of threshold units and is reusable well beyond this chapter. Theorem 20.2 is the matching negative fact on expressive power, and it is a corollary of the same bound: a class that shatters $2^n$ points needs $\Omega(2^n)$ edges. Backpropagation's correctness is the one theorem about training the chapter can offer, given the hardness results, and it is the algorithm every practitioner runs.

Difficulty

Claim 20.1 and Lemma 20.4 are explicit constructions: the neuron $g_i(x) = \operatorname{sign}(\langle x, u_i\rangle - n + 1)$ detects $x = u_i$ because $\langle x, u_i\rangle \le n - 2$ otherwise, and the output neuron takes the disjunction; formally one must build the weight function and evaluate the forward pass on the $2^n$ inputs. Exercises 3 and 4 are counting: a restricted product is determined by its two restricted factors, and a restricted composition $f_2 \circ f_1$ on $C$ is determined by $f_1|_C$ and $f_2|_{f_1(C)}$, with $|f_1(C)| \le |C|$. Theorem 20.6 then needs: the class of one neuron is the class of homogenous halfspaces on its $d_{t,i}$ incoming coordinates, of VC dimension at most $d_{t,i}$ (Mission VI), Sauer's lemma in the form $\tau(m) \le (em)^{d}$ for every $m \ge 1$ (Mission IV; for $m \le d$ use $2^m \le (em)^m$), the layer class as a product and the network as a composition of layer classes, and finally the arithmetic $2^m \le (em)^{|E|} \Rightarrow m \le 2|E|\log_2(16|E|)$, which replaces the book's appeal to Lemma A.2 (for $m \ge 8|E|$ one has $\ln m \le \frac{m\ln 2}{2|E|}$). Theorem 20.2 follows from the goal with $|E| \le |V|^2$. Backpropagation is a chain-rule computation in a single real variable: the loss as a function of one weight is a composition of finitely many differentiable maps, and the derivative unwinds to the backward recursion; the formal effort is in the induction along layers with the natural-number indexing of the model.

Formalization scope

Layers and neurons are indexed by natural numbers: a LayeredGraph records the depth, the layer widths and, for each $t < T$, the finite set of edges $(v_{t,j}, v_{t+1,i})$ as pairs $(i, j)$ within the layer widths. Weights are functions on all index triples, and only those on edges are used, so the class is the image of all weight functions, as in (20.1). The forward computation netOutput is a recursion on the layer index; netInput is $a_{t+1,i}$. The sign activation returns $\pm1$ with $\operatorname{sign}(0) = -1$, the book's convention elsewhere, and a neuron with no incoming edges outputs $\sigma(0)$ (p. 270). The binary class signNetClass n G is Bool-valued, true iff the output neuron's input is positive, and is stated for graphs of depth at least $1$ (for depth $0$ the edges out of the input layer would be used but not counted in $|E|$). Growth functions with finite codomain are growthY, an sSup over restriction sizes, well defined because the codomains are finite; the Bool case is Mission IV's growth, and VC dimension and shattering are Mission IV's. Theorem 20.6 and Theorem 20.2 are given with explicit constants derived from the proof, since $O(\cdot)$ statements have no formal content; the drafter verified $\max\{m : 2^m \le (em)^{|E|}\} \le 2|E|\log_2(16|E|)$ numerically for $|E|$ up to $3000$ and at $10^4, \dots, 10^7$, and $2^n \le 2|V|^2\log_2(16|V|^2) \le 8|V|^3$. Backpropagation is stated for an arbitrary layered graph (phantom edges have weight $0$, p. 279), any differentiable activation, and one edge at a time as a HasDerivAt of the loss in that weight; $\delta_t$ is defined by recursion on $T - t$. The book's layer indices in (20.3) are shifted by one in the statement.

Not stated: Theorem 20.3 (Turing machines), Theorem 20.5 and Exercise 1 (sigmoid approximation, which needs a convention for outputs in $[-1,1]$ that the chapter leaves open), Theorem 20.7 and Exercise 6 (NP-hardness), Exercise 5 (the $\Omega(|E|^2)$ sigmoid lower bound, which assumes an exact threshold), the sigmoid half of Theorem 20.2, and the SGD pseudocode of §20.6, which is a heuristic without a stated guarantee.

Selected references

• S. Shalev-Shwartz, S. Ben-David, Understanding Machine Learning: From Theory to Algorithms, Cambridge University Press, 2014, Chapter 20. doi:10.1017/CBO9781107298019
• M. Anthony, P. L. Bartlett, Neural Network Learning: Theoretical Foundations, Cambridge University Press, 1999. doi:10.1017/CBO9780511624216
• D. E. Rumelhart, G. E. Hinton, R. J. Williams, Learning representations by back-propagating errors, Nature 323, 1986. doi:10.1038/323533a0
• I. Parberry, Circuit Complexity and Neural Networks, MIT Press, 1994.
• E. B. Baum, D. Haussler, What size net gives valid generalization?, Neural Computation 1(1), 1989. doi:10.1162/neco.1989.1.1.151

Motivation

Chapter 3 of Kearns and Vazirani, An Introduction to Computational Learning Theory (MIT Press, 1994, doi:10.7551/mitpress/3897.001.0001), asks how many random examples suffice to learn a concept from an infinite class. The cardinality bound of Occam's Razor is useless there, yet the rectangle game of Chapter 1 shows that some infinite classes are learnable from a finite sample. The answer is the Vapnik–Chervonenkis dimension: the size of the largest set on which the class realizes every labeling. Sauer's lemma says that a class of VC dimension $d$ realizes only $\Phi_d(m) = \sum_{i \le d}\binom{m}{i} \le (em/d)^d$ labelings on any $m$ points, polynomially many rather than $2^m$, and the ε-net theorem of Blumer, Ehrenfeucht, Haussler and Warmuth turns this into a sample bound: a consistent hypothesis from a class of VC dimension $d$ is probably approximately correct once $m$ is of order $(1/\epsilon)(\log(1/\delta) + d\log(1/\epsilon))$. A matching lower bound shows that $\Omega(d/\epsilon)$ examples are necessary. The chapter thus gives a single combinatorial parameter that characterizes, up to a logarithmic factor, the sample complexity of learning any class in the distribution-free model.

Setting

For a class $C$ of concepts $X \to \{0,1\}$ and a finite $S \subseteq X$, $\Pi_C(S)$ is the set of dichotomies of $S$ realized by $C$; $S$ is shattered if all $2^{|S|}$ are realized; $\mathrm{VCD}(C)$ is the supremum of the sizes of shattered sets, possibly $\infty$; $\Pi_C(m)$ is the largest $|\Pi_C(S)|$ over $|S| = m$; and $\Phi_d(m)$ is defined by $\Phi_d(m) = \Phi_d(m-1) + \Phi_{d-1}(m-1)$, $\Phi_d(0) = \Phi_0(m) = 1$. For a target $c$ the error regions are $c \,\Delta\, h$ for $h$ in the hypothesis class, and a set of points is an ε-net if it meets every error region of weight at least $\epsilon$ under the target distribution $D$. Samples, their product law, consistency and the error of a hypothesis are those of Mission I.

Formalization targets

Goal: Theorems 3.3 and 3.4

Let $H$ be a class of VC dimension at most $d$, well-behaved for the target $c$ (the double-sample event of the proof is null-measurable), and $m \ge 8/\epsilon$. The points of a random sample of $m$ examples of a target $c$ fail to be an ε-net for the error regions $\{c \,\Delta\, h : h \in H\}$ with probability at most

$$2\,\Phi_d(2m)\,2^{-\epsilon m/2},$$

so any algorithm that outputs a hypothesis in $H$ consistent with its sample has error greater than $\epsilon$ with at most that probability; with $m \ge (4/\epsilon)\log_2(2/\delta)$ and $m \ge (8d/\epsilon)\log_2(13/\epsilon)$ the probability is at most $\delta$; and, if $H$ is nonempty, every class contained in $H$ for whose targets $H$ is well-behaved is PAC learnable using $H$.

Milestones

Lemma 3.1 (Sauer's lemma, $\Pi_C(m) \le \Phi_d(m)$); Lemma 3.2 ($\Phi_d(m) = \sum_{i \le d}\binom{m}{i}$); the polynomial bound $\Phi_d(m) \le (em/d)^d$ of p. 57; Theorem 3.5 (the $\Omega(d/\epsilon)$ lower bound, in the two explicit forms of its proof).

Significance

Theorem 3.3 is the fundamental theorem of PAC learning: it replaces $\log|H|$ in Occam's Razor by the VC dimension and thereby covers rectangles, halfspaces, polygons, neural networks with a fixed architecture, and every class whose dichotomies grow polynomially. Its proof, the double sample and random partition argument, is the origin of symmetrization in empirical process theory. Sauer's lemma is a cornerstone of extremal combinatorics with independent proofs by Sauer, Shelah and Vapnik–Chervonenkis, and the lower bound of Theorem 3.5 shows that the upper bound is tight to within $\log(1/\epsilon)$, so the VC dimension genuinely characterizes sample complexity. None of these is machine-checked. Formalizing them puts on the platform the VC dimension, the growth function and the ε-net theorem with explicit constants, stated on the same sample law as the rest of this series, and the first information-theoretic lower bound for learning.

Difficulty

Sauer's lemma is a double induction on $d$ and $m$ through the auxiliary class $C'$ of dichotomies whose two extensions to a distinguished point are both realized, which needs care with the identification of dichotomies of $S$ and of $S \setminus \{x\}$. The ε-net theorem needs: the reduction $\Pr[A] \le 2\Pr[B]$ from a failed ε-net on the first half to a region hit at least $\epsilon m/2$ times by the second half, which is a Chebyshev bound on a binomial variable and is where $m \ge 8/\epsilon$ enters; the exchangeability of the $2m$ draws with a random partition into two halves; the counting bound $\binom{m}{\ell}/\binom{2m}{\ell} \le 2^{-\ell}$; and Sauer's lemma applied to the error regions, whose growth function equals that of $H$. The explicit constants require the numerical inequality $2(2em/d)^d 2^{-\epsilon m/2} \le \delta$ under the two stated conditions. The lower bound is a probabilistic argument with a random target: conditional on the sample, the labels of unseen points are fair coins, so the number of errors on them is binomial and exceeds half its range with probability at least $1/2$; the refined bound scales this construction to a region of weight $16\epsilon$ and uses Markov's inequality to bound the number of draws landing in it. Measurability of the failure sets is avoided by stating outer-measure bounds, except for the double-sample event, which the proof integrates: it is assumed null-measurable (the well-behavedness of Blumer et al., without which the theorem is false for a class of VC dimension $1$ on $\omega_1$). For the lower bound it is avoided by working over a finitely supported distribution on a space with measurable singletons.

Formalization scope

The VC dimension is a supremum in $\mathbb{N} \cup \{\infty\}$, the growth function a supremum in $\mathbb{N}$ (bounded by $2^m$), and $\Phi_d$ the book's recurrence, with its closed form and polynomial bound stated as separate theorems. The goal is stated for a hypothesis class $H$ (Theorem 3.4), Theorem 3.3 being the case $C = H$; it carries the exact bound of the proof, the explicit constants of Blumer et al. in place of the book's $c_0$, the requirement $m \ge 8/\epsilon$ of the proof's Chebyshev step, measurability of the hypotheses and the target, well-behavedness of $H$ for the target, and $0 < \epsilon, \delta < 1$. PAC learnability of the subclasses of $H$ needs $H$ nonempty, since no algorithm outputs hypotheses in the empty class. The lower bound is stated for every deterministic learning function, on an instance space with measurable singletons, for a class shattering some set of $d \ge 1$ points, with the explicit constants derived in the proof sketch ($m \le d/2$: error $\ge 1/8$ with probability $\ge 1/2$; $\epsilon \le 1/16$ and $m \le (d-1)/(64\epsilon)$: error $> \epsilon$ with probability $\ge 1/4$). Running time is not modelled. The composition bound for layered networks (Theorems 3.6 and 3.7) is not stated.

Trivializing readings are excluded: the ε-net event ranges over every hypothesis of $H$, the failure bounds are uniform over all consistent learners, and the lower bound holds for every learning function. Welcome contributions: Sauer's lemma, the closed form and the $(em/d)^d$ bound, the random-partition counting lemma, and the binomial median inequality used in the lower bound.

Selected references

• M. J. Kearns, U. V. Vazirani, An Introduction to Computational Learning Theory, MIT Press, 1994, Chapter 3. doi:10.7551/mitpress/3897.001.0001
• A. Blumer, A. Ehrenfeucht, D. Haussler, M. K. Warmuth, Learnability and the Vapnik–Chervonenkis dimension, Journal of the ACM 36(4), 1989. doi:10.1145/76359.76371
• V. N. Vapnik, A. Ya. Chervonenkis, On the uniform convergence of relative frequencies of events to their probabilities, Theory of Probability and its Applications 16(2), 1971. doi:10.1137/1116025
• N. Sauer, On the density of families of sets, Journal of Combinatorial Theory, Series A 13(1), 1972. doi:10.1016/0097-3165(72)90019-2
• A. Ehrenfeucht, D. Haussler, M. Kearns, L. Valiant, A general lower bound on the number of examples needed for learning, Information and Computation 82(3), 1989. doi:10.1016/0890-5401(89)90002-3