Håstad's theorem with the sharp exponent

Håstad's theorem [Has86], Jukna, Chapter 12, Arora and Barak, Section 14.1 with the exponent 1 / (d - 1): a circuit of negations and unbounded fan-in conjunctions and disjunctions whose AND/OR depth is at most d (the largest number of conjunctions and disjunctions on a path, negations free: Circuit.depthWith Unbounded.andOrCost), computing the parity of n bits, has at least 2 ^ s conjunctions and disjunctions for every s ≥ 2 with 17 s (16 s + 1) ^ (d - 2) ≤ n (Unbounded.two_pow_le_card_andOr_of_computes_parity). In particular it has at least 2 ^ s gates whenever (17 s) ^ (d - 1) ≤ n and d ≥ 2 (Unbounded.two_pow_le_size_of_computes_parity_of_pow_le), and at least 2 ^ (n ^ (1 / (d - 1)) / 17) / 2 gates once n ≥ 34 ^ (d - 1) (Unbounded.two_rpow_le_two_mul_size_of_computes_parity), a size 2 ^ Ω(n ^ (1 / (d - 1))) with explicit constants. The exponent is optimal: parity has circuits of AND/OR depth d with 2 ^ O(n ^ (1 / (d - 1))) gates [Has86], and indeed every symmetric function has circuits of AND/OR depth d with at most 2 ^ (C n ^ (1 / (d - 1))) + n gates [LR26] (Unbounded.exists_circuit_of_isSymmetric). Korten's top-down argument gives the same exponent with an unspecified constant (Unbounded.two_rpow_lt_add_size_of_computes_parity). Since negations are free, the bounds hold for Circuit.depth, which counts them (Circuit.depthWith_le_depth, Unbounded.two_pow_le_size_of_computes_parity_of_depth_le), improving the exponent 1 / (d + 1) of Unbounded.two_pow_le_size_of_computes_parity, and for formulas (Unbounded.two_pow_le_size_of_formula_computes_parity_of_depthWith_le).

The proof refines the one of Unbounded.two_pow_le_size_of_computes_parity in three ways.

• Negations are free: the stages are indexed by AND/OR depth, and only conjunctions and disjunctions are switched; a negation is shallow when its argument is (Unbounded.shallow_trace_of_forall_ne_not).
• The first stage switches conjunctions and disjunctions of literals, formulas in disjunctive normal form with terms of one literal, so it leaves a constant fraction 1 / 17 of the bits free rather than 1 / (16 s + 1) (Unbounded.two_pow_mul_card_filter_not_shallow_le_of_ne_not with k = 1).
• There is no last stage: after d - 1 stages every gate of AND/OR depth at most d - 1 is shallow, so a gate of AND/OR depth d is, up to negation, a formula in disjunctive normal form with terms of fewer than s literals (Unbounded.exists_dnf_of_shallow), and such a formula cannot compute restricted parity on s or more free bits (Cslib.Logic.PL.DNF.not_forall_eval_eq_parity_fill_bne).

Main results

• Cslib.Circuits.Boolean.Unbounded.shallow_trace_of_forall_ne_not: negations keep wires shallow.
• Cslib.Circuits.Boolean.Unbounded.two_pow_mul_card_filter_exists_not_shallow_le_depthWith: random restrictions make the gates of small AND/OR depth shallow, stage by stage.
• Cslib.Circuits.Boolean.Unbounded.two_pow_le_card_andOr_of_computes_parity: Håstad's theorem with the sharp exponent, counting conjunctions and disjunctions.
• Cslib.Circuits.Boolean.Unbounded.two_pow_le_size_of_computes_parity_of_depthWith_le, Cslib.Circuits.Boolean.Unbounded.two_pow_le_size_of_computes_parity_of_pow_le, Cslib.Circuits.Boolean.Unbounded.two_rpow_le_two_mul_size_of_computes_parity: the same for the number of gates.
• Cslib.Circuits.Boolean.Unbounded.two_pow_le_size_of_computes_parity_of_depth_le, Cslib.Circuits.Boolean.Unbounded.two_pow_le_size_of_computes_parity_of_depth_le_of_pow_le, Cslib.Circuits.Boolean.Unbounded.two_rpow_le_two_mul_size_of_computes_parity_of_depth_le: the same when depth counts negations.
• Cslib.Circuits.Boolean.Unbounded.two_pow_le_size_of_formula_computes_parity_of_depthWith_le, Cslib.Circuits.Boolean.Unbounded.two_pow_le_size_of_formula_computes_parity_of_pow_le, Cslib.Circuits.Boolean.Unbounded.two_rpow_le_two_mul_size_of_formula_computes_parity: the same for formulas.

References

• J. Håstad, Almost optimal lower bounds for small depth circuits
• S. Jukna, Boolean Function Complexity: Advances and Frontiers
• S. Arora, B. Barak, Computational Complexity: A Modern Approach
• Lecomte and Ramakrishnan

Programs, with free negations

theorem Cslib.Circuits.Boolean.Unbounded.shallow_trace_of_forall_ne_not {n s g : ℕ} {ρ : BitString.PartialAssignment (Fin n)} {p : Program signature n g} (hs : 2 ≤ s) {j : ℕ} (h : ∀ (k : Fin g), (p.lines k).op ≠ Op.not → Program.depthsWith andOrCost p k ≤ j → Shallow s ρ fun (x : BitString n) => p.eval interpretation x k) (w : Wire n g) (hw : Program.wireDepthsWith andOrCost p w ≤ j) : Shallow s ρ fun (x : BitString n) => p.trace interpretation x w

If every conjunction and disjunction of AND/OR depth at most j is shallow under ρ, so is every wire of AND/OR depth at most j: inputs are shallow, and negations keep functions shallow.

theorem Cslib.Circuits.Boolean.Unbounded.shallow_two_trace_of_wireDepthsWith_eq_zero {n g : ℕ} {p : Program signature n g} (ρ : BitString.PartialAssignment (Fin n)) (w : Wire n g) (hw : Program.wireDepthsWith andOrCost p w = 0) : Shallow 2 ρ fun (x : BitString n) => p.trace interpretation x w

Every wire of AND/OR depth zero, a literal, has decision tree depth at most one under every restriction.

theorem Cslib.Circuits.Boolean.Unbounded.two_pow_mul_card_filter_exists_not_shallow_le_depthWith {n s g : ℕ} {p : Program signature n g} (hs : 2 ≤ s) {e : ℕ} (hn : s * (16 * s + 1) ^ e ≤ n / 17) (i : ℕ) (hi : i ≤ e) : 2 ^ s * {ρ ∈ BitString.PartialAssignment.withFree (Fin n) (n / 17 / (16 * s + 1) ^ i) | ∃ (k : Fin g), Program.depthsWith andOrCost p k ≤ i + 1 ∧ ¬Shallow s ρ fun (x : BitString n) => p.eval interpretation x k}.card ≤ {k : Fin g | (p.lines k).op ≠ Op.not ∧ Program.depthsWith andOrCost p k ≤ i + 1}.card * (BitString.PartialAssignment.withFree (Fin n) (n / 17 / (16 * s + 1) ^ i)).card

Random restrictions make the gates of small AND/OR depth shallow. For s ≥ 2 and s (16 s + 1) ^ e ≤ ⌊n / 17⌋, after a first stage leaving ⌊n / 17⌋ bits free and i ≤ e more stages each leaving a 1 / (16 s + 1) fraction of the free bits, at most a G / 2 ^ s fraction of the restrictions make some gate of AND/OR depth at most i + 1 s-deep, where G is the number of conjunctions and disjunctions of AND/OR depth at most i + 1.

Håstad's theorem

theorem Cslib.Circuits.Boolean.Unbounded.two_pow_le_card_andOr_of_trace_eq_parity {n s g : ℕ} {p : Program signature n g} {w : Wire n g} (hw : ∀ (x : Fin n → Bool), p.trace interpretation x w = parity n x) (hs : 2 ≤ s) {d : ℕ} (hd : Program.wireDepthsWith andOrCost p w ≤ d) (hn : 17 * s * (16 * s + 1) ^ (d - 2) ≤ n) : 2 ^ s ≤ {k : Fin g | (p.lines k).op ≠ Op.not}.card

Håstad's theorem with the sharp exponent, for programs: if a wire of AND/OR depth at most d computes the parity of n bits, the program has at least 2 ^ s conjunctions and disjunctions, for every s ≥ 2 with 17 s (16 s + 1) ^ (d - 2) ≤ n.

theorem Cslib.Circuits.Boolean.Unbounded.two_pow_le_card_andOr_of_computes_parity {n s : ℕ} {C : Circuit signature n 1} (hC : C.Computes interpretation (single (parity n))) (hs : 2 ≤ s) {d : ℕ} (hd : Circuit.depthWith andOrCost C ≤ d) (hn : 17 * s * (16 * s + 1) ^ (d - 2) ≤ n) : 2 ^ s ≤ {k : Fin C.size | (C.program.lines k).op ≠ Op.not}.card

Håstad's theorem with the sharp exponent, counting conjunctions and disjunctions. A circuit of negations and unbounded fan-in conjunctions and disjunctions of AND/OR depth at most d computing the parity of n bits has at least 2 ^ s conjunctions and disjunctions, for every s ≥ 2 with 17 s (16 s + 1) ^ (d - 2) ≤ n. Their number is the AND/OR cost C.program.cost andOrCost (cost_andOrCost_eq_card).

theorem Cslib.Circuits.Boolean.Unbounded.two_pow_le_size_of_computes_parity_of_depthWith_le {n s : ℕ} {C : Circuit signature n 1} (hC : C.Computes interpretation (single (parity n))) (hs : 2 ≤ s) {d : ℕ} (hd : Circuit.depthWith andOrCost C ≤ d) (hn : 17 * s * (16 * s + 1) ^ (d - 2) ≤ n) : 2 ^ s ≤ C.size

Håstad's theorem with the sharp exponent. A circuit of negations and unbounded fan-in conjunctions and disjunctions of AND/OR depth at most d computing the parity of n bits has at least 2 ^ s gates, for every s ≥ 2 with 17 s (16 s + 1) ^ (d - 2) ≤ n.

Round numbers

theorem Cslib.Circuits.Boolean.Unbounded.two_pow_le_size_of_computes_parity_of_pow_le {n s : ℕ} {C : Circuit signature n 1} (hC : C.Computes interpretation (single (parity n))) (hs : 2 ≤ s) {d : ℕ} (hd₂ : 2 ≤ d) (hd : Circuit.depthWith andOrCost C ≤ d) (hn : (17 * s) ^ (d - 1) ≤ n) : 2 ^ s ≤ C.size

Håstad's theorem with the sharp exponent, in round numbers. A circuit of negations and unbounded fan-in conjunctions and disjunctions of AND/OR depth at most d ≥ 2 computing the parity of n bits has at least 2 ^ s gates, for every s ≥ 2 with (17 s) ^ (d - 1) ≤ n.

theorem Cslib.Circuits.Boolean.Unbounded.two_rpow_le_two_mul_size_of_computes_parity {n : ℕ} {C : Circuit signature n 1} (hC : C.Computes interpretation (single (parity n))) {d : ℕ} (hd₂ : 2 ≤ d) (hd : Circuit.depthWith andOrCost C ≤ d) (hn : 34 ^ (d - 1) ≤ n) : 2 ^ (↑n ^ (↑(d - 1))⁻¹ / 17) ≤ 2 * ↑C.size

Håstad's theorem with the sharp exponent, as a real bound. A circuit of negations and unbounded fan-in conjunctions and disjunctions of AND/OR depth at most d ≥ 2 computing the parity of n ≥ 34 ^ (d - 1) bits has at least 2 ^ (n ^ (1 / (d - 1)) / 17) / 2 gates.

Depth counting negations

theorem Cslib.Circuits.Boolean.Unbounded.two_pow_le_size_of_computes_parity_of_depth_le {n s : ℕ} {C : Circuit signature n 1} (hC : C.Computes interpretation (single (parity n))) (hs : 2 ≤ s) {d : ℕ} (hd : C.depth ≤ d) (hn : 17 * s * (16 * s + 1) ^ (d - 2) ≤ n) : 2 ^ s ≤ C.size

Håstad's theorem with the sharp exponent, when depth counts negations. A circuit of negations and unbounded fan-in conjunctions and disjunctions of depth at most d computing the parity of n bits has at least 2 ^ s gates, for every s ≥ 2 with 17 s (16 s + 1) ^ (d - 2) ≤ n.

theorem Cslib.Circuits.Boolean.Unbounded.two_pow_le_size_of_computes_parity_of_depth_le_of_pow_le {n s : ℕ} {C : Circuit signature n 1} (hC : C.Computes interpretation (single (parity n))) (hs : 2 ≤ s) {d : ℕ} (hd₂ : 2 ≤ d) (hd : C.depth ≤ d) (hn : (17 * s) ^ (d - 1) ≤ n) : 2 ^ s ≤ C.size

Håstad's theorem with the sharp exponent, when depth counts negations, in round numbers: at least 2 ^ s gates for every s ≥ 2 with (17 s) ^ (d - 1) ≤ n, when d ≥ 2.

theorem Cslib.Circuits.Boolean.Unbounded.two_rpow_le_two_mul_size_of_computes_parity_of_depth_le {n : ℕ} {C : Circuit signature n 1} (hC : C.Computes interpretation (single (parity n))) {d : ℕ} (hd₂ : 2 ≤ d) (hd : C.depth ≤ d) (hn : 34 ^ (d - 1) ≤ n) : 2 ^ (↑n ^ (↑(d - 1))⁻¹ / 17) ≤ 2 * ↑C.size

Håstad's theorem with the sharp exponent, when depth counts negations, as a real bound: at least 2 ^ (n ^ (1 / (d - 1)) / 17) / 2 gates when d ≥ 2 and n ≥ 34 ^ (d - 1).

Formulas

theorem Cslib.Circuits.Boolean.Unbounded.two_pow_le_size_of_formula_computes_parity_of_depthWith_le {n s : ℕ} {F : Formula signature n} (hF : F.Computes interpretation (parity n)) (hs : 2 ≤ s) {d : ℕ} (hd : Formula.depthWith andOrCost F ≤ d) (hn : 17 * s * (16 * s + 1) ^ (d - 2) ≤ n) : 2 ^ s ≤ F.size

Håstad's theorem with the sharp exponent, for formulas. A formula of negations and unbounded fan-in conjunctions and disjunctions of AND/OR depth at most d computing the parity of n bits has at least 2 ^ s operation nodes, for every s ≥ 2 with 17 s (16 s + 1) ^ (d - 2) ≤ n.

theorem Cslib.Circuits.Boolean.Unbounded.two_pow_le_size_of_formula_computes_parity_of_pow_le {n s : ℕ} {F : Formula signature n} (hF : F.Computes interpretation (parity n)) (hs : 2 ≤ s) {d : ℕ} (hd₂ : 2 ≤ d) (hd : Formula.depthWith andOrCost F ≤ d) (hn : (17 * s) ^ (d - 1) ≤ n) : 2 ^ s ≤ F.size

Håstad's theorem with the sharp exponent, for formulas, in round numbers: at least 2 ^ s operation nodes for every s ≥ 2 with (17 s) ^ (d - 1) ≤ n, when d ≥ 2.

theorem Cslib.Circuits.Boolean.Unbounded.two_rpow_le_two_mul_size_of_formula_computes_parity {n : ℕ} {F : Formula signature n} (hF : F.Computes interpretation (parity n)) {d : ℕ} (hd₂ : 2 ≤ d) (hd : Formula.depthWith andOrCost F ≤ d) (hn : 34 ^ (d - 1) ≤ n) : 2 ^ (↑n ^ (↑(d - 1))⁻¹ / 17) ≤ 2 * ↑F.size

Håstad's theorem with the sharp exponent, for formulas, as a real bound: at least 2 ^ (n ^ (1 / (d - 1)) / 17) / 2 operation nodes when d ≥ 2 and n ≥ 34 ^ (d - 1).