Complexitylib: a blueprint for computational complexity in Lean

7 Circuits, advice, and uniformity

This chapter covers Boolean circuits over explicit bases, nonuniform circuit families and the class \(\mathsf{P/poly}\), its characterization by polynomial advice, the translation to and from CSLib’s circuit model, logspace-uniform circuit families, the containment \(\mathsf{BPP} \subseteq \mathsf{P/poly}\), the small-depth classes \(\mathsf{NC}\), \(\mathsf{AC}\) and \(\mathsf{TC}\), Boolean formulas, and Barrington’s theorem. The library proves that polynomial advice and polynomial-size circuits give the same class, that logspace-uniform polynomial-size circuit families decide exactly \(\mathsf{P}\) (Arora–Barak, Section 6.2), that \(\mathsf{BPP} \subseteq \mathsf{P/poly}\), the nonuniform Barrington theorem for variable-bounded logarithmic-depth formulas, and the containment of \(\mathsf{NC}^1\) in the formula and branching-program classes of that theorem. Still planned are the interleaving \(\mathsf{NC}^i \subseteq \mathsf{AC}^i \subseteq \mathsf{NC}^{i+1}\), the containment of logarithmic-depth formulas in \(\mathsf{NC}^1\) (and with it \(\mathsf{NC}^1 = \mathsf{FormulaNC1}\)), and a uniform Barrington theorem, which is the main open mathematical item. The main open infrastructure items are a circuit encoding designed for log-space generation and a consolidation of the library’s parallel circuit and formula representations (Section 7.10).

Two conventions hold throughout. The size of a circuit counts internal and output gates but not input wires, and negations on gate inputs are free; this differs from Arora–Barak, who count input vertices and NOT gates, but the difference does not affect polynomial size bounds. A circuit family stores an explicit answer for the empty input, because the circuit model requires at least one input wire. Every class in this chapter is nonuniform unless its name says otherwise.

7.1 The circuit model

A basis is a type of operations, each with an arity constraint (any fan-in, fan-in exactly \(k\), or fan-in at most \(k\)) and an evaluation map on bit strings of admissible length. A circuit over a basis \(B\) with \(N \ge 1\) inputs, \(M \ge 1\) outputs and \(G\) internal gates consists of \(G\) internal gates and \(M\) output gates. A gate applies an operation of \(B\) to a list of wires whose length the operation admits, and each gate input carries its own negation flag. The wires are the \(N\) inputs followed by the \(G\) internal gates. Internal gate \(i\) may read only wires \(0, \dots , N + i - 1\), so the circuit is acyclic by construction, and an output gate may read any wire. Evaluation \(C : \{ 0,1\} ^N \to \{ 0,1\} ^M\) gives each input wire its input bit and each gate the value of its operation on its input wires, each negated when its flag is set. The size of \(C\) is \(G + M\). The depth of an input wire is \(0\), the depth of a gate is one more than the largest depth of a wire it reads (\(1\) for a gate with no inputs), and the depth of \(C\) is the largest depth of an output gate.

Definition 240 AND/OR bases
✓

The bases whose operations are AND and OR with fan-in exactly \(2\), with fan-in at most \(k\), and with any fan-in. In the last two a gate may have no inputs, and then computes the empty conjunction \(1\) or the empty disjunction \(0\). Negation is available only through the free per-input flags. Unless stated otherwise, a circuit is a circuit over the fan-in-two basis.

A basis is complete if, for all \(N, M \ge 1\), every function \(\{ 0,1\} ^N \to \{ 0,1\} ^M\) is computed by some circuit over it; the fan-in-two AND/OR basis is complete. For \(N \ge 1\), \(f : \{ 0,1\} ^N \to \{ 0,1\} \) and a basis \(B\), \(\mathrm{size}_B(f)\) is the least size of a single-output circuit over \(B\) computing \(f\). The general version takes values in \(\mathbb {N} \cup \{ \infty \} \) and equals \(\infty \) exactly when no circuit over \(B\) computes \(f\). For a complete basis a natural-number-valued version is provided, and it agrees with the general one.

The wiring digraph of a circuit has its \(N + G + M\) input, internal and output vertices, numbered in that order, and an edge from each wire to every gate that reads it. Every edge goes from a smaller index to a larger one, so the digraph is acyclic, and its number of edges is at most the total fan-in of the circuit (the number of gate-input occurrences, output gates included). The bound can be strict, since a gate that reads one wire twice contributes one edge.

Proof ▶

Internal gate \(i\) reads only wires below \(N + i\), and the output vertices come last. Each edge comes from at least one gate-input occurrence.

Let \(C\) be a fan-in-two circuit on \(k + m\) inputs with \(m \ge 1\), \(M \ge 1\) outputs and \(G\) internal gates, and let \(s \in \{ 0,1\} ^k\). There is a fan-in-two circuit \(C_s\) on \(m\) inputs, again with \(M\) outputs and \(G\) internal gates and hence of the same size as \(C\), such that \(C_s(y) = C(s\, y)\) for every \(y \in \{ 0,1\} ^m\), where \(s\, y\) is the concatenation.

Proof ▶

Fix the inputs one at a time; each step removes one input wire, rewires the gates that read it so that they compute the same values, and keeps the gates.

Write \(\mathrm{size}\) for the fan-in-two AND/OR size complexity. Let \(m \ge 1\), let \(f : \{ 0,1\} ^{k + m} \to \{ 0,1\} \), and let \(g : \{ 0,1\} ^m \to \{ 0,1\} \) output \(1\) on \(y\) exactly when \(f(x\, y) = 1\) for some \(x \in \{ 0,1\} ^k\). Then \(\mathrm{size}(g) \le 2^k (\mathrm{size}(f) + 1)\).

Proof ▶

Induction on \(k\). Fixing the first input of a function to a constant does not increase its size, since the input can be hardwired without adding gates, and the disjunction of two functions has size at most the sum of their sizes plus one.

7.2 Circuit families and \(\mathsf{P/poly}\)

A circuit family over \(B\) consists of a single-output circuit \(C_n\) over \(B\) on \(n\) inputs, with any number of internal gates, for every \(n \ge 1\), together with an output bit for the empty input. It computes the Boolean function family given by \(C_n\) at length \(n \ge 1\) and by the stored bit at length \(0\), and it decides the language of strings on which it outputs \(1\). Its size at \(n \ge 1\) is the size of \(C_n\), and its size at \(0\) is \(0\). It has polynomial size if a single polynomial \(p \in \mathbb {N}[X]\) satisfies \(\mathrm{size}(n) \le p(n)\) for every \(n\).

Definition 246 \(\mathsf{SIZE}\)
✓

For \(s : \mathbb {N} \to \mathbb {N}\), \(\mathsf{SIZE}(s)\) is the class of languages decided by a fan-in-two AND/OR circuit family whose size at every length \(n\) is at most \(s(n)\). The same definition is available over any basis.

Definition 247 \(\mathsf{P/poly}\)
✓
#

\(\mathsf{P/poly} = \bigcup _{p \in \mathbb {N}[X]} \mathsf{SIZE}(n \mapsto p(n))\).

Proposition 248 Big-O form of \(\mathsf{P/poly}\)
✓
#

\(L \in \mathsf{P/poly}\) if and only if some fan-in-two circuit family decides \(L\) and has size \(O(n^k)\) for some \(k\), that is, size at most \(C n^k\) at every sufficiently large length \(n\), for some constant \(C\).

Proof ▶

Convert between polynomial bounds and big-O power bounds.

Every basis \(B\) is a CSLib signature whose operation symbols are the gate kinds of \(B\): an operation, a fan-in it allows, and a negation flag for each input, interpreted exactly as a gate of that kind evaluates. A circuit over \(B\) with \(N \ge 1\) inputs, \(G\) internal gates and \(M \ge 1\) outputs becomes a CSLib circuit over this signature that computes the same function and has exactly \(G + M\) gates, its size. Every output of the translation is an internal gate, and its total fan-in is that of the original circuit. The translation goes one way for general bases: the converse, from CSLib circuits over \(B\)’s signature whose outputs are internal gates, is planned.

Proof ▶

The program lists the internal gates and then the output gates, with each wire renumbered in CSLib’s layout, and the outputs are the last \(M\) gates. Induction on the position shows that every gate of the program carries the value of the corresponding typed gate.

Let \(N, M \ge 1\). A De Morgan circuit in CSLib’s model (constants, negation, and binary conjunction and disjunction, every gate counted, and outputs designated wires at no cost) with \(N\) inputs, \(g\) gates, and \(M\) outputs becomes a fan-in-two AND/OR circuit of size exactly \(g + M\) computing the same outputs. Conversely, a fan-in-two AND/OR circuit with \(N\) inputs, \(G\) internal gates, and \(M\) outputs has a CSLib circuit with at most \(N + 2G + M\) gates computing the same outputs. For a single function \(f\) on \(N\) bits, a CSLib circuit with \(g\) gates computing \(f\) gives \(\mathrm{size}(f) \le g + 1\) for the fan-in-two AND/OR size complexity, and \(f\) has a CSLib circuit with at most \(N + 2\, \mathrm{size}(f)\) gates. Consequently \(L \in \mathsf{P/poly}\) if and only if, for some polynomial \(p\), every length-\(n\) slice of \(L\), including \(n = 0\), is decided by a CSLib circuit with at most \(p(n)\) gates, and \(\mathsf{P/poly}\) equals CSLib’s \(\mathsf{P/poly}\). The size classes interleave: \(\mathsf{SIZE}(s)\) lies in CSLib’s \(\mathsf{SIZE}(n + 2s + 1)\), and CSLib’s \(\mathsf{SIZE}(s)\) lies in \(\mathsf{SIZE}(s + 1)\).

CSLib’s Boolean \(\mathsf{SIZE}\) and \(\mathsf{P/poly}\) (at most \(s(n)\) De Morgan gates at every length \(n\), and \(\bigcup _k \mathsf{SIZE}(n^k + k)\)) are pending CSLib work by this library’s author, not yet in upstream CSLib; the library builds them from the pinned integration branch. The equality of the two \(\mathsf{P/poly}\) classes is therefore a consistency check between two definitions by the same author, not corroboration by an independently reviewed upstream definition.

Proof ▶

The two models share their wire layout, so the first translation maps each CSLib gate to one of ours: \(\neg w\) becomes \(\neg w \wedge \neg w\) and a constant becomes \(x_0 \wedge \neg x_0\) or \(x_0 \vee \neg x_0\). For the second, keep every wire and its negation available, at a cost of \(N\) gates for the negated inputs, two gates per internal gate, and one gate per output. The length-zero slice, which our families answer separately, is a single constant gate in CSLib’s model.

Corollary 251 A language outside \(\mathsf{P/poly}\)
✓

Some language is not in \(\mathsf{P/poly}\).

Proof ▶

By the equality with CSLib’s \(\mathsf{P/poly}\), this is CSLib’s theorem that some language lies outside its \(\mathsf{P/poly}\): by Shannon’s counting argument some language has, at every large length \(n\), no De Morgan circuit with at most \(2^n / n\) gates, and every bound \(n^k + k\) falls below \(2^n / n\) for large \(n\). That theorem, like CSLib’s \(\mathsf{P/poly}\), comes from the pending CSLib work described in Theorem 250.

Let \(N, M \ge 1\), as in Theorem 250. In CSLib’s model inputs have depth \(0\), every gate (negations and constants included) adds one level, and the depth of a circuit is the largest depth of an output wire. The translation of a CSLib De Morgan circuit has depth exactly one more, for its output gates. Conversely, a fan-in-two AND/OR circuit with \(N\) inputs, \(G\) internal gates, and \(M\) outputs has a CSLib circuit computing the same outputs with exactly \(N + 2G + M\) gates and depth at most one more. For the depth classes \(\mathsf{DEPTH}(d)\) of Definition 273: if \(f \in \mathsf{DEPTH}(d)\), then for every \(n \ge 1\) some CSLib circuit of depth at most \(d(n) + 1\) computes \(f_n\); and if for every \(n \ge 1\) some CSLib circuit of depth at most \(d(n)\) computes \(f_n\), then \(f \in \mathsf{DEPTH}(n \mapsto d(n) + 1)\).

Proof ▶

The first translation replaces each CSLib gate by one gate of ours. For the second, keep both rails of every wire: negate the inputs once, compute each gate’s positive rail directly and its negative rail by De Morgan from the complementary rails, so each gate costs two gates and no extra depth.

Theorem 253
✓

\(\mathsf{P} \subseteq \mathsf{P/poly}\).

Proof ▶

Unroll a polynomial-time decider into its circuit family.

7.3 Advice

An advice function \(a : \mathbb {N} \to \{ 0,1\} ^*\) has polynomial length if \(|a(n)| \le p(n)\) for every \(n\) and a polynomial \(p \in \mathbb {N}[X]\). A deterministic machine \(M\) decides \(L\) with advice \(a\) in time \(T\) if on input \(\langle a(|x|), x \rangle \) (the library’s self-delimiting pairing) it halts within \(T(|x|)\) steps with \(1\) in the first output cell when \(x \in L\) and \(0\) otherwise. The time bound is measured in \(|x|\), not in the length of the paired input. \(\mathsf{PAdvice}\) is the class of languages decided, by a machine with any number of work tapes, with polynomial-length advice in time \(O(n^d)\) for some \(d\).

\(\mathsf{PAdvice} \subseteq \mathsf{P/poly}\). More precisely, if a deterministic machine decides \(L\) with advice \(a\) in time \(T = O(n^d)\), then hardwiring the advice into its acceptance circuits gives a fan-in-two family of size \(O(n^{3d})\) deciding \(L\), whatever the length of the advice.

Proof ▶

At each length, unroll the advised machine and hardwire the fixed advice prefix of its input.

\(\mathsf{P/poly} \subseteq \mathsf{PAdvice}\). More precisely, if a fan-in-two family \(F\) of size \(O(n^d)\) decides \(L\), then its family codes (Definition 258) form polynomial-length advice, with which the serialized circuit evaluator of Theorem 260 decides \(L\) in time \(O(n^{4(d+1)})\), measured in \(|x|\).

Proof ▶

The advice at length \(n\) is the family code at length \(n\), which has polynomial length by Lemma 259, and the machine is the serialized circuit evaluator, whose quadratic running time in the length of the paired input is polynomial in \(|x|\).

Corollary 257
✓

\(\mathsf{PAdvice} = \mathsf{P/poly}\).

Proof ▶

Combine the two containments.

7.4 Serialized circuits and their evaluation

A fan-in-two single-output circuit is serialized as its gate count in terminated unary followed by its gates in index order, the output gate last. A gate is written as an operation bit, two negation flags, and two absolute wire references in terminated unary. The partial evaluator \(\mathrm{evalCode}(N, c, x)\) decodes \(c\), rejects inputs of the wrong length and codes that are malformed, have trailing bits, are empty, or reference a wire that is not yet computed, and evaluates the gates in order with a memo array. The code of a family at length \(0\) is the bit \(0\) followed by the stored answer; at length \(n \ge 1\) it is the bit \(1\) followed by the code of \(C_n\). The family evaluator runs a code \(c\) on a string \(x\) as follows: if \(x\) is empty, \(c\) must be \(0\, b\) for a bit \(b\), and the answer is \(b\); if \(x\) is nonempty, \(c\) must be \(1\, c'\), and the answer is \(\mathrm{evalCode}(|x|, c', x)\); every other case is rejected. The evaluation language is the set of strings \(\langle c, x \rangle \) (the library’s self-delimiting pairing) on which the family evaluator returns \(1\).

For a fan-in-two single-output circuit \(C\) with \(N \ge 1\) inputs and size \(s\), \(\mathrm{evalCode}(N, \mathrm{code}(C), x) = C(x)\) for every \(x \in \{ 0,1\} ^N\), and \(|\mathrm{code}(C)| \le 1 + s\, (2(N + s) + 6)\).

Proof ▶

The iterative evaluator agrees gate by gate with typed evaluation.

A fixed deterministic machine with three work tapes decides the evaluation language within \(4n + 20(n + 1)^2 + 17 = O(n^2)\) steps on every input of length \(n\); malformed pairs and malformed codes are rejected. In particular the evaluation language is in \(\mathsf{P}\).

Proof ▶

Validate the outer pair and copy the code and the input onto work tapes in linear time. Then stream the gates once, appending each gate value to a memo tape and reading the two referenced values by unary lookup; each gate costs \(O(|\mathrm{memo}|)\) steps, for a total of \(20(|c| + |x| + 1)^2\) steps in the core.

7.5 Functional unrolling

The circuits below compute the output bit of a bounded run. They are not the Cook–Levin CNF, which expresses the existence of an accepting tableau rather than computing the output of a deterministic run.

Let \(M\) be a nondeterministic machine and \(T, n, m \in \mathbb {N}\) with \(m \ge 1\). For every assignment of the \(n\) data positions and the \(T\) choice positions to input wires among \(m\) inputs, there is a fan-in-two circuit on \(m\) inputs that, on every input whose data wires carry \(x \in \{ 0,1\} ^n\) and whose choice wires carry \(c \in \{ 0,1\} ^T\), outputs \(1\) exactly when the \(T\)-step trace of \(M\) on \(x\) under \(c\) is in the halting state with \(1\) in the first output cell. Its size is at most \(\kappa _M (T + 2)^3\) for a constant \(\kappa _M\) depending only on \(M\), not on \(n\) or \(m\). With the choices placed first (\(m = T + n \ge 1\)), the number of \(c \in \{ 0,1\} ^T\) on which the circuit accepts \(c\, x\) equals the number of accepting choice sequences of length \(T\) of \(M\) on \(x\).

Proof ▶

Encode bounded configurations one-hot, compile the initial configuration and one transition layer as Boolean formula fragments, tile \(T\) layers, and append a final halt-and-output gate.

For a deterministic machine \(M\) and \(f : \mathbb {N} \to \mathbb {N}\), the unrolling family has at length \(n \ge 1\) the acceptance circuit of \(M\) at horizon \(f(n)\) with every choice input hardwired to \(0\), and at length \(0\) the output bit of the \(f(0)\)-step run on the empty input. If \(M\) decides \(L\) in time \(f\), the family decides \(L\). If \(f = O(n^d)\), the family has size \(O(n^{3d})\).

Proof ▶

A deterministic machine ignores its choices, so any fixed choice string gives the output bit.

7.6 Logspace uniformity

Definition 263 Logspace-uniform \(\mathsf{P/poly}\)
✓

A fan-in-two circuit family is logspace-uniform if some function in \(\mathsf{FL}\) maps \(1^n\) to the family code at length \(n\), for every \(n\), as in Arora–Barak, Section 6.2. The generator reads \(n\) in unary, and its output at \(n = 0\) carries the stored empty-input answer. The class \(\mathsf{UniformPPoly}\) consists of the languages decided by a logspace-uniform circuit family of polynomial size. P-uniformity is not used.

Proposition 264
✓
#

\(\mathsf{UniformPPoly} \subseteq \mathsf{P/poly}\).

Proof ▶

Forget the generator.

\(\mathsf{UniformPPoly} \subseteq \mathsf{P}\).

Proof ▶

Since \(\mathsf{FL} \subseteq \mathsf{FP}\), the map \(x \mapsto \langle \mathrm{gen}(1^{|x|}), x \rangle \) is in \(\mathsf{FP}\). The language is the preimage of the evaluation language under this map, and \(\mathsf{P}\) is closed under preimages by \(\mathsf{FP}\) functions. The size bound of the family is not used.

Let \(M\) be a deterministic machine and \(h : \mathbb {N} \to \mathbb {N}\). The direct unrolling of \(M\) at horizon \(h\) has at length \(n \ge 1\) the acceptance circuit of Theorem 261 at horizon \(h(n)\) on \(n\) inputs, the data on the inputs in order and every choice position on input \(0\). The padded direct unrolling \(P_{M,h}\) appends to this gate list constant-\(0\) gates up to \(\kappa _M (h(n) + 2)^3\) gates and then a gate copying the original output, so its gate count is a closed-form cubic in \(h(n)\); at length \(0\) it stores the output bit of the \(h(0)\)-step run on the empty input. Let \(D_{M,h}(n)\) be the family code of \(P_{M,h}\) at length \(n\). If \(M\) decides \(L\) in time \(h\), then \(P_{M,h}\) decides \(L\), and if \(h = O(n^d)\), then \(P_{M,h}\) has size \(O(n^{3d})\). For every polynomial \(q \in \mathbb {N}[X]\) and \(h(n) = q(n) + n + 1\), the map \(x \mapsto D_{M,h}(|x|)\) is in \(\mathsf{FL}\).

Proof ▶

The padding gates are never read and the final gate copies the acceptance bit, so correctness and the size bound come from Theorem 261, the choices being irrelevant to a deterministic machine. For the code map, the direct unrolling is an initialization fragment, a stream of fixed-size transition fragments whose wire offsets have closed forms, and a final gate. A streaming transducer computes the offsets with binary counters, addition, multiply-add and fixed-polynomial evaluation, and writes each reference in terminated unary. One polynomial bounds every counter value, so the auxiliary space is logarithmic.

\(\mathsf{P} \subseteq \mathsf{UniformPPoly}\). More precisely, every language decided by a deterministic machine within \(q(n)\) steps, for a polynomial \(q \in \mathbb {N}[X]\), is in \(\mathsf{UniformPPoly}\).

Proof ▶

A machine that decides \(L\) in time \(q\) also decides it in time \(h(n) = q(n) + n + 1\). At horizon \(h\) its padded direct unrolling decides \(L\), has polynomial size, and has a code map in \(\mathsf{FL}\).

Theorem 268 Logspace-uniform circuits capture \(\mathsf{P}\)
✓

\(\mathsf{UniformPPoly} = \mathsf{P}\).

Proof ▶

Combine the two containments.

7.7 \(\mathsf{BPP}\) is contained in \(\mathsf{P/poly}\)

Lemma 269 One seed for all inputs of a length
✓

Let \(M\) be a probabilistic machine and \(f : \mathbb {N} \to \mathbb {N}\) such that, for every \(x\), the fraction of choice strings \(c \in \{ 0,1\} ^{f(|x|)}\) on which the \(f(|x|)\)-step trace of \(M\) on \(x\) under \(c\) is halted with output \(1\) is at least \(2/3\) if \(x \in L\) and at most \(1/3\) if \(x \notin L\); no halting assumption is made. For every \(n\) there is a single string of \(r(n) f(n)\) random bits, where \(r(n) = 12(n + 1) + 1\), on which the strict majority vote of these \(f(n)\)-step runs of \(M\), one on each of the \(r(n)\) consecutive blocks of \(f(n)\) bits, is correct for every \(x \in \{ 0,1\} ^n\).

Proof ▶

Amplification makes the error on each input less than \(2^{-(n+1)}\), and a union bound over the \(2^n\) inputs leaves a good seed.

Under the hypotheses of Lemma 269, the family whose circuit at length \(n \ge 1\) hardwires a seed selected by that lemma into \(r(n)\) parallel copies of the acceptance circuit at horizon \(f(n)\), followed by a strict-majority fragment, and whose answer at length \(0\) is whether the empty string is in \(L\), is a fan-in-two circuit family deciding \(L\). If \(f = O(n^d)\), its size is \(O(n^{3d+4})\).

Proof ▶

Compose copies of the original acceptance circuit rather than unrolling the repeated machine, whose control state would store the whole vote vector.

Theorem 271 Adleman
✓

\(\mathsf{BPP} \subseteq \mathsf{P/poly}\).

Proof ▶

Apply the hardwired amplification family to a \(\mathsf{BPP}\) machine.

Corollary 272
✓

\(\mathsf{BPP} \subseteq \mathsf{PAdvice}\).

Proof ▶

Compose the two containments.

7.8 Small-depth classes

Definition 273 \(\mathsf{DEPTH}\), \(\mathsf{NC}^i\) and \(\mathsf{AC}^i\)
✓

These are classes of Boolean function families, one function \(\{ 0,1\} ^n \to \{ 0,1\} \) for each \(n\) (including \(n = 0\)), not of languages. The depth of a circuit family at length \(n \ge 1\) is the depth of \(C_n\), and at length \(0\) it is \(0\). For \(d : \mathbb {N} \to \mathbb {N}\), \(\mathsf{DEPTH}(d)\) consists of the families computed by a fan-in-two AND/OR circuit family of depth at most \(d(n)\) at every length \(n\), with no size bound; the same definition is available over any basis. A family is in \(\mathsf{NC}^i\) if a fan-in-two AND/OR circuit family of polynomial size and depth at most \(c\, (\lfloor \log _2 n \rfloor + 1)^i\) at every length \(n\), for some constant \(c \in \mathbb {N}\) (with \(\lfloor \log _2 0 \rfloor = 0\)), computes it. \(\mathsf{AC}^i\) is defined the same way with unbounded fan-in. \(\mathsf{NC}^0\), \(\mathsf{NC}^1\) and \(\mathsf{AC}^0\) are the special cases. These classes are nonuniform.

Definition 274 \(\mathsf{TC}^i\)
✓

A threshold gate with cutoff \(t\) outputs \(1\) when at least \(t\) of its inputs are \(1\); the threshold basis has unweighted threshold gates of any fan-in, with the free negation flags on their inputs. \(\mathsf{TC}^i\) is defined like \(\mathsf{AC}^i\) over this basis.

For \(i \le j\), \(\mathsf{NC}^i \subseteq \mathsf{NC}^j\), \(\mathsf{AC}^i \subseteq \mathsf{AC}^j\) and \(\mathsf{TC}^i \subseteq \mathsf{TC}^j\); in particular \(\mathsf{NC}^0 \subseteq \mathsf{NC}^1\). For every \(i\), \(\mathsf{AC}^i \subseteq \mathsf{TC}^i\); in particular \(\mathsf{AC}^0 \subseteq \mathsf{TC}^0\).

Proof ▶

Monotonicity is monotonicity of the depth envelope. For \(\mathsf{AC}^i \subseteq \mathsf{TC}^i\), transport circuits along the embedding of AND and OR gates as threshold gates, which preserves semantics, size and depth exactly.

Proposition 276 Interleaving

For every \(i\), \(\mathsf{NC}^i \subseteq \mathsf{AC}^i \subseteq \mathsf{NC}^{i+1}\).

Proof ▶

A fan-in-two gate is an unbounded gate. Conversely, size does not count wires, so first merge repeated inputs of each unbounded gate: a gate of a circuit with \(n\) inputs and \(G\) internal gates then reads at most \(2(n + G)\) distinct literals, a polynomial number. Replace each such gate by a balanced fan-in-two tree of depth \(O(\log n)\), and a gate with no inputs by a constant built from an input and its negation.

7.9 Formulas and Barrington’s theorem

A Boolean formula is a tree built from variables \(x_i\) (\(i \in \mathbb {N}\)), the two constants, negation, and binary conjunction and disjunction. It is evaluated under a total assignment \(\mathbb {N} \to \{ 0,1\} \). Its size is its number of nodes, its depth is the length of a longest root-to-leaf path, with each negation counted as one level, and its variables are the indices \(i\) of the variables \(x_i\) occurring in it.

Unfolding one output of a fan-in-two circuit \(C\) with \(N \ge 1\) inputs gives a formula whose variables are all below \(N\), which under every assignment \(\alpha \) computes that output of \(C\) on \((\alpha (0), \dots , \alpha (N - 1))\), and whose depth is at most twice the depth of that output gate. No size bound is claimed, since shared subcircuits are duplicated.

Proof ▶

Structural recursion on wire indices; an edge negation followed by its gate costs two formula levels.

Definition 279 Permutation branching program
✓

A width-\(w\) permutation branching program is a list of instructions \((i, \pi _0, \pi _1)\) with \(i \in \mathbb {N}\) and \(\pi _0, \pi _1 \in S_w\); the instruction reads variable \(i\). Under an assignment \(\alpha \), an instruction selects \(\pi _{\alpha (i)}\), and the program evaluates to the product \(\pi ^{(1)} \pi ^{(2)} \cdots \pi ^{(k)}\) of the selected permutations in \(S_w\), where \((\pi \tau )(y) = \pi (\tau (y))\). A program computes \(f\) through \(\sigma \) if, under every assignment \(\alpha \), it evaluates to \(\sigma \) when \(f(\alpha ) = 1\) and to the identity otherwise.

Lemma 280 Five-cycles are commutators
✓

Some two \(5\)-cycles in \(S_5\) have a \(5\)-cycle as their commutator, and every \(5\)-cycle in \(S_5\) is the commutator \([a, b] = a b a^{-1} b^{-1}\) of two \(5\)-cycles \(a\) and \(b\).

Proof ▶

One explicit pair is checked by kernel computation, and the \(5\)-cycles form a single conjugacy class.

For every \(5\)-cycle \(\sigma \in S_5\), every Boolean formula of depth \(d\) is computed through \(\sigma \) by a width-\(5\) permutation branching program of length at most \(4^d\); in particular it is computed through some \(\sigma \neq 1\) by such a program. A formula of depth at most \(\lfloor \log _2 n \rfloor \), with \(n \ge 1\), is therefore computed through some \(\sigma \neq 1\) by a width-\(5\) program of length at most \(n^2\).

Proof ▶

Induction on the formula, for all target \(5\)-cycles at once. The variable \(x_i\) is the instruction \((i, 1, \sigma )\), the constant true is a single constant instruction, and false is the empty program. For a negation, compute the subformula through \(\sigma ^{-1}\) and fold a final multiplication by \(\sigma \) into the last instruction, so the length does not grow. For a conjunction, write \(\sigma = [a, b]\) with \(5\)-cycles \(a\) and \(b\) and concatenate programs for the two conjuncts through \(a\) and \(b\) and their inverses, four blocks of length at most \(4^{d-1}\). A disjunction is a negated conjunction of negations, with the negations folded in the same way.

An explicit computable compiler maps every formula \(\varphi \) and target \(\sigma \in S_5\) to a width-\(5\) program of length at most \(4^{\mathrm{depth}(\varphi )}\) which, whenever \(\sigma \) is a \(5\)-cycle, computes \(\varphi \) through \(\sigma \). If every variable of \(\varphi \) is at most \(b\), then so is the variable read by every instruction. For the fixed \(5\)-cycle \(\sigma _0 = [a_0, b_0]\), the commutator of two explicit \(5\)-cycles, the program evaluates to \(\sigma _0 \neq 1\) when \(\varphi \) is true and to the identity otherwise.

Proof ▶

Follow the recursion of Theorem 281, writing each target \(5\)-cycle \(\sigma \) as the commutator of the conjugates of \(a_0\) and \(b_0\) by the first permutation, in an explicit enumeration of \(S_5\), that conjugates \(\sigma _0\) to \(\sigma \).

For a width-\(w\) program \(P\) of length \(\ell \) and a point \(x\), there is a formula that, under every assignment, is true exactly when the value of \(P\) moves \(x\), and that has depth at most \((w + 1) \lceil \log _2 \ell \rceil + 2\), where \(\lceil \log _2 \ell \rceil \) is read as \(0\) for \(\ell \le 1\). If every instruction of \(P\) reads a variable below \(n\), then every variable of the formula is below \(n\).

Proof ▶

Split the program in half and compose the two halves through the \(w\) possible intermediate points.

Definition 284 Formula and program families
✓

\(\mathsf{FormulaNC1}\) is the class of Boolean function families computed by a family of formulas \((\varphi _n)\) in which \(\varphi _n\) reads only variables below \(n\), is evaluated on \(x \in \{ 0,1\} ^n\) under the assignment sending \(i {\lt} n\) to \(x_i\) (and every other index to \(0\)), and has depth at most \(c \lfloor \log _2 n \rfloor + c\) for a constant \(c\). \(\mathsf{Width5BP}\) is the class of Boolean function families decided by a family of width-\(5\) programs \(P_n\) for \(n \ge 1\), each reading only variables below \(n\) and with a designated point \(x_n\), together with an explicit answer at \(n = 0\); on \(x \in \{ 0,1\} ^n\) the output is \(1\) exactly when the value of \(P_n\) under the same assignment moves \(x_n\), and the length of \(P_n\) is at most \(C (n + 1)^k\) for constants \(C, k\).

\(\mathsf{FormulaNC1} = \mathsf{Width5BP}\): every formula family witnessing membership in \(\mathsf{FormulaNC1}\) has a program family witnessing membership in \(\mathsf{Width5BP}\) that computes the same Boolean function family, and conversely. The same equality holds for the total-assignment variants, whose members assign to each \(n\) a function \((\mathbb {N} \to \{ 0,1\} ) \to \{ 0,1\} \): there the formula at \(n\) may read any variable and has depth at most \(c \lfloor \log _2 n \rfloor + c\), and the program at \(n\) may read any variable, decides by whether it moves a designated point, and has length at most \(C (n + 1)^k\) at every \(n\), including \(n = 0\).

Proof ▶

Compile \(\varphi _n\) at the fixed \(5\)-cycle \(\sigma _0\). The program evaluates to \(\sigma _0\) or to the identity, and a \(5\)-cycle moves every point, so any designated point is moved exactly when \(\varphi _n\) is true. Its length is at most \(4^{c \lfloor \log _2 n \rfloor + c} \le 4^c n^{2c}\), and it reads only variables below \(n\) (constant instructions read variable \(0\)). Conversely, a program of length at most \(C (n + 1)^k\) has a balanced decision formula of depth at most \(6 \lceil \log _2 (C (n + 1)^k) \rceil + 2\), which is logarithmic in \(n\), with its variables below \(n\).

\(\mathsf{NC}^1 \subseteq \mathsf{FormulaNC1}\), and hence \(\mathsf{NC}^1 \subseteq \mathsf{Width5BP}\).

Proof ▶

Unfold the output of each circuit; the depth at most doubles, from \(c \lfloor \log _2 n \rfloor + c\) to \(2c \lfloor \log _2 n \rfloor + 2c\), and the variables stay below the arity. The polynomial size bound is not used.

\(\mathsf{FormulaNC1} \subseteq \mathsf{NC}^1\). Consequently \(\mathsf{NC}^1 = \mathsf{FormulaNC1} = \mathsf{Width5BP}\).

Proof ▶

A formula of depth \(d\) has fewer than \(2^{d+1}\) nodes, so logarithmic depth gives polynomial size. At each length \(n \ge 1\), compile each node to a gate, pushing negations down by De Morgan’s laws into input flags and building constants from an input and its negation; the stored answer at length \(0\) is the value of \(\varphi _0\).

There are injective codes for formulas (a unary token count followed by the postfix token stream) and for width-\(5\) programs (a unary instruction count followed by the instructions, each a unary variable index and two seven-bit permutation ranks), and a total function \(g\) on bit strings, sending every string that does not decode to a formula to the empty string, such that for every formula \(\varphi \) of depth \(d\), \(g(\mathrm{code}(\varphi ))\) is the code of, and decodes to, the program compiled from \(\varphi \) at \(\sigma _0\) in Theorem 282, and \(|g(\mathrm{code}(\varphi ))| \le 4^d + 1 + 4^d (|\mathrm{code}(\varphi )| + 15)\).

Proof ▶

Run the compiler on the decoded formula and bound each serialized instruction by the code length of the formula.

Lemma 289 The Barrington generator in small space

A deterministic transducer computes \(g(\mathrm{code}(\varphi ))\) from \(\mathrm{code}(\varphi )\) using \(O(\mathrm{depth}(\varphi ) + \log |\mathrm{code}(\varphi )|)\) work-tape cells.

Proof ▶

Emit the compiled program instruction by instruction: an instruction index is a path of length \(\mathrm{depth}(\varphi )\) in the recursion tree, with a constant amount of permutation data per level, and the formula node at the current position is located by counting in the input code.

Theorem 290 Uniform Barrington

Call a formula family logspace-uniform if some function in \(\mathsf{FL}\) maps \(1^n\) to \(\mathrm{code}(\varphi _n)\), and a program family logspace-uniform if some function in \(\mathsf{FL}\) maps \(1^n\) to the code of \((P_n, x_n)\). A Boolean function family has a logspace-uniform \(\mathsf{FormulaNC1}\) witness if and only if it has a logspace-uniform \(\mathsf{Width5BP}\) witness.

Proof ▶

Forward: compose the formula generator with the small-space Barrington generator; the depth is \(O(\log n)\), so the space is \(O(\log n)\). Backward: generate the balanced decision formula of each program in logarithmic space.

7.10 Open directions

The following items are infrastructure rather than theorems.

  • A circuit encoding designed for generation. The current code format has a gate-count header, absolute wire references into subformulas of varying size, and no sharing. The log-space generator behind Lemma 266 must therefore compute closed-form wire offsets for every fragment, and the uniform unrolling development is about 59,000 lines. A layered grid encoding, in which every wire reference is an affine function of the loop counters, would make future uniformity proofs (uniform \(\mathsf{NC}\) and \(\mathsf{AC}\), Theorem 290, finer notions such as DLOGTIME uniformity) much shorter. It should come with an \(\mathsf{FL}\) translation into the existing codec, so that \(\mathsf{UniformPPoly}\) does not change.

  • One representation of circuits and formulas. The library has about fourteen parallel representations: typed circuits, raw gate lists, general, monotone and negation-normal unbounded formulas, two CNF/DNF types, two decision-tree types, branching programs, and several family wrappers. A single formula type with a substitution operation (a monadic bind), and circuits built so that acyclicity holds by typing, would let restriction, unfolding and normalization lemmas be proved once.