Håstad's theorem: parity needs large circuits of constant depth

Håstad's theorem for circuits with unbounded fan-in: a circuit of depth d with fewer than 2 ^ s gates that computes the parity of n bits has n < s (16 s + 1) ^ d, for every s ≥ 2. So such circuits, and formulas (Formula.toCircuit), have size 2 ^ Ω(n ^ (1 / (d + 1))) [FSS84], [Ajt83], [Has86], Jukna, Chapter 12. The exponent 1 / (d + 1) is weaker than Håstad's 1 / (d - 1): each stage below leaves a 1 / (16 s + 1) fraction of the free bits rather than 1 / (10 s) with a final DNF stage. Depth counts every gate on a path, negations included, and size counts every gate.

The proof restricts the circuit d times by random restrictions (partial assignments, BitString.PartialAssignment). After stage j, every gate of depth at most j computes, under the restriction so far, a function of decision tree complexity below s (Shallow). A gate of depth j + 1 then computes, up to negation, a formula in disjunctive normal form whose terms have fewer than s literals (exists_dnf_of_shallow), and the switching lemma shows that at most a 2 ^ (-s) fraction of the extensions of the restriction fail to make it shallow (two_pow_mul_card_filter_not_shallow_le). Drawing a restriction with fewer free bits by first drawing one with more free bits and then an extension of it (PartialAssignment.mul_card_filter_withFree_le), at most a G / 2 ^ s fraction of the restrictions leaving n / (16 s + 1) ^ j bits free make some gate of depth at most j deep, where G is the number of those gates (two_pow_mul_card_filter_exists_not_shallow_le). With fewer than 2 ^ s gates, some restriction makes the output shallow, while the restricted parity needs to query every free bit. The counted form also bounds the Fourier tails of small circuits of constant depth Linial, Mansour and Nisan.

Main definitions

• Cslib.Circuits.Boolean.Shallow: a function has, under a restriction, small decision tree complexity.

Main results

• Cslib.Circuits.Boolean.Unbounded.exists_dnf_of_shallow: an operation applied to shallow functions computes a narrow formula in disjunctive normal form, up to negation.
• Cslib.Circuits.Boolean.Unbounded.two_pow_mul_card_filter_not_shallow_le: the switching lemma for one operation applied to shallow functions.
• Cslib.Circuits.Boolean.Unbounded.two_pow_mul_card_filter_not_shallow_le_of_ne_not: the switching lemma for a conjunction or disjunction of functions of decision tree depth at most k, leaving a 1 / (16 k + 1) fraction of the free bits.
• Cslib.Circuits.Boolean.Unbounded.two_pow_mul_card_filter_exists_not_shallow_le: random restrictions make small circuits of constant depth shallow.
• Cslib.Circuits.Boolean.Unbounded.two_pow_le_size_of_computes_parity: Håstad's theorem for circuits.
• Cslib.Circuits.Boolean.Unbounded.two_pow_le_size_of_formula_computes_parity: Håstad's theorem for formulas.

References

• M. Furst, J. B. Saxe, M. Sipser, Parity, circuits, and the polynomial-time hierarchy
• M. Ajtai, Σ¹₁-formulae on finite structures
• J. Håstad, Almost optimal lower bounds for small depth circuits
• S. Jukna, Boolean Function Complexity: Advances and Frontiers
• N. Linial, Y. Mansour, N. Nisan, Constant depth circuits, Fourier transform, and learnability

Shallow functions

def Cslib.Circuits.Boolean.Shallow {n : ℕ} (s : ℕ) (ρ : BitString.PartialAssignment (Fin n)) (f : BitString n → Bool) : Prop

f is s-shallow under ρ: the function it computes under ρ has decision tree complexity below s.

@[instance_reducible]

noncomputable instance Cslib.Circuits.Boolean.instDecidableShallow {n : ℕ} (s : ℕ) (ρ : BitString.PartialAssignment (Fin n)) (f : BitString n → Bool) : Decidable (Shallow s ρ f)

theorem Cslib.Circuits.Boolean.Shallow.mono {n s : ℕ} {ρ ρ' : BitString.PartialAssignment (Fin n)} {f : BitString n → Bool} (hf : Shallow s ρ f) (h : ρ'.Extends ρ) : Shallow s ρ' f

Restricting further keeps a function shallow.

theorem Cslib.Circuits.Boolean.Shallow.of_le {n s : ℕ} {ρ : BitString.PartialAssignment (Fin n)} {f : BitString n → Bool} {s' : ℕ} (h : Shallow s ρ f) (hs : s ≤ s') : Shallow s' ρ f

A function shallow for one bound is shallow for every larger bound.

theorem Cslib.Circuits.Boolean.shallow_proj {n s : ℕ} (hs : 2 ≤ s) (ρ : BitString.PartialAssignment (Fin n)) (i : Fin n) : Shallow s ρ fun (x : BitString n) => x i

The input bits are shallow.

theorem Cslib.Circuits.Boolean.Shallow.not {n s : ℕ} {ρ : BitString.PartialAssignment (Fin n)} {f : BitString n → Bool} (h : Shallow s ρ f) : Shallow s ρ fun (x : BitString n) => !f x

The negation of a shallow function is shallow.

theorem Cslib.Circuits.Boolean.Shallow.exists_tree {n s : ℕ} {ρ : BitString.PartialAssignment (Fin n)} {f : BitString n → Bool} (h : Shallow s ρ f) : ∃ (t : DecisionTree (Fin n) Bool), (∀ (y : Fin n → Bool), t.eval y = f (ρ.fill y)) ∧ t.depth < s

Shallow functions have decision trees of depth below s.

theorem Cslib.Circuits.Boolean.not_shallow_parity {n s : ℕ} {ρ : BitString.PartialAssignment (Fin n)} (h : s ≤ ρ.free.card) : ¬Shallow s ρ (parity n)

Restricted parity is not shallow when at least s bits are free.

One stage of restrictions

theorem Cslib.Circuits.Boolean.Unbounded.exists_dnf_of_shallow {n s : ℕ} {ρ : BitString.PartialAssignment (Fin n)} {op : Op} (hop : op ≠ Op.not) {args : Fin op.arity → BitString n → Bool} (h : ∀ (j : Fin op.arity), Shallow s ρ (args j)) : ∃ (D : Logic.PL.DNF (Fin n)) (b : Bool), (∀ t ∈ D, List.length t < s ∧ (List.map Prod.fst t).Nodup) ∧ ∀ (y : Fin n → Bool), Logic.PL.DNF.eval y D = ((interpretation op fun (j : Fin (signature.Arity op)) => args j (ρ.fill y)) != b)

Operations applied to shallow functions are narrow formulas in disjunctive normal form, up to negation: a disjunction is the disjunction of the paths to true of decision trees for its arguments, and the negation of a conjunction is the disjunction of their paths to false.

theorem Cslib.Circuits.Boolean.Unbounded.card_filter_not_shallow_le_of_ne_not {n : ℕ} {ρ : BitString.PartialAssignment (Fin n)} {op : Op} (hop : op ≠ Op.not) {k : ℕ} {args : Fin op.arity → BitString n → Bool} (h : ∀ (j : Fin op.arity), Shallow (k + 1) ρ (args j)) (ℓ s : ℕ) : {ρ' ∈ ρ.extensions ℓ | ¬Shallow s ρ' fun (x : BitString n) => interpretation op fun (j : Fin (signature.Arity op)) => args j x}.card ≤ (ρ.extensions (ℓ - s)).card * (4 * k) ^ s

The switching step for a conjunction or disjunction. If the arguments of a conjunction or disjunction have decision tree depth at most k under ρ, at most #E(ℓ - s) (4k)^s of the extensions of ρ with ℓ free bits leave it s-deep, where E(m) are the extensions of ρ with m free bits.

theorem Cslib.Circuits.Boolean.Unbounded.card_filter_not_shallow_le {n s : ℕ} {ρ : BitString.PartialAssignment (Fin n)} {op : Op} {args : Fin op.arity → BitString n → Bool} (h : ∀ (j : Fin op.arity), Shallow s ρ (args j)) (ℓ : ℕ) : {ρ' ∈ ρ.extensions ℓ | ¬Shallow s ρ' fun (x : BitString n) => interpretation op fun (j : Fin (signature.Arity op)) => args j x}.card ≤ (ρ.extensions (ℓ - s)).card * (4 * s) ^ s

The switching step for one operation. If the arguments of an operation are shallow under ρ, few extensions of ρ leave it deep.

theorem Cslib.Circuits.Boolean.Unbounded.two_pow_mul_card_filter_not_shallow_le_of_ne_not {n s : ℕ} {ρ : BitString.PartialAssignment (Fin n)} {op : Op} (hop : op ≠ Op.not) {k : ℕ} {args : Fin op.arity → BitString n → Bool} (h : ∀ (j : Fin op.arity), Shallow (k + 1) ρ (args j)) {ℓ : ℕ} (hsℓ : s ≤ ℓ) (hℓ : (16 * k + 1) * ℓ ≤ ρ.free.card) : 2 ^ s * {ρ' ∈ ρ.extensions ℓ | ¬Shallow s ρ' fun (x : BitString n) => interpretation op fun (j : Fin (signature.Arity op)) => args j x}.card ≤ (ρ.extensions ℓ).card

The switching fraction for a conjunction or disjunction: if its arguments have decision tree depth at most k under ρ, at most a 2 ^ (-s) fraction of the extensions of ρ with ℓ free bits leave it s-deep, when s ≤ ℓ and ℓ is at most a 1 / (16 k + 1) fraction of the free bits of ρ. For arguments that are literals, k = 1 and the fraction is 1 / 17.

theorem Cslib.Circuits.Boolean.Unbounded.two_pow_mul_card_filter_not_shallow_le {n s : ℕ} {ρ : BitString.PartialAssignment (Fin n)} {op : Op} {args : Fin op.arity → BitString n → Bool} (h : ∀ (j : Fin op.arity), Shallow s ρ (args j)) {ℓ : ℕ} (hsℓ : s ≤ ℓ) (hℓ : (16 * s + 1) * ℓ ≤ ρ.free.card) : 2 ^ s * {ρ' ∈ ρ.extensions ℓ | ¬Shallow s ρ' fun (x : BitString n) => interpretation op fun (j : Fin (signature.Arity op)) => args j x}.card ≤ (ρ.extensions ℓ).card

The switching fraction for one operation: if the arguments of an operation are shallow under ρ, at most a 2 ^ (-s) fraction of the extensions of ρ with ℓ free bits leave it deep, when s ≤ ℓ and ℓ is at most a 1 / (16 s + 1) fraction of the free bits of ρ.

Programs

theorem Cslib.Circuits.Boolean.Unbounded.shallow_trace_wires {n s : ℕ} {ρ : BitString.PartialAssignment (Fin n)} {g : ℕ} {p : Program signature n g} (hs : 2 ≤ s) {j : ℕ} (hρ : ∀ (k : Fin g), p.depths k ≤ j → Shallow s ρ fun (x : BitString n) => p.eval interpretation x k) {k : Fin g} (hk : p.depths k ≤ j + 1) (a : Fin (Op.arity (p.lines k).op)) : Shallow s ρ fun (x : BitString n) => p.trace interpretation x ((p.lines k).wires a)

If every gate of depth at most j is shallow under ρ, so is every argument of a gate of depth at most j + 1.

theorem Cslib.Circuits.Boolean.Unbounded.two_pow_mul_card_filter_exists_not_shallow_le {n s g : ℕ} {p : Program signature n g} (hs : 2 ≤ s) {d : ℕ} (hn : s * (16 * s + 1) ^ d ≤ n) (j : ℕ) (hj : j ≤ d) : 2 ^ s * {ρ ∈ BitString.PartialAssignment.withFree (Fin n) (n / (16 * s + 1) ^ j) | ∃ (k : Fin g), p.depths k ≤ j ∧ ¬Shallow s ρ fun (x : BitString n) => p.eval interpretation x k}.card ≤ {k : Fin g | p.depths k ≤ j}.card * (BitString.PartialAssignment.withFree (Fin n) (n / (16 * s + 1) ^ j)).card

Random restrictions make small circuits of constant depth shallow. For a program with gates of depth at most d, s ≥ 2 and s (16 s + 1) ^ d ≤ n, after j ≤ d stages at most a G / 2 ^ s fraction of the restrictions leaving n / (16 s + 1) ^ j bits free make some gate of depth at most j deep, where G is the number of gates of depth at most j.

Circuits

theorem Cslib.Circuits.Boolean.Unbounded.shallow_output {n s : ℕ} {ρ : BitString.PartialAssignment (Fin n)} {C : Circuit signature n 1} (hs : 2 ≤ s) (hρ : ∀ (k : Fin C.size), C.program.depths k ≤ C.depth → Shallow s ρ fun (x : BitString n) => C.program.eval interpretation x k) : Shallow s ρ fun (x : BitString n) => C.program.trace interpretation x (C.outputs 0)

If every gate of depth at most the depth of a circuit is shallow under ρ, so is its output.

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

Håstad's theorem for circuits with unbounded fan-in. A circuit of depth d computing the parity of n bits has at least 2 ^ s gates, for every s ≥ 2 with s (16 s + 1) ^ d ≤ n.

theorem Cslib.Circuits.Boolean.Unbounded.two_pow_le_size_of_formula_computes_parity {n s : ℕ} {F : Formula signature n} (hF : F.Computes interpretation (parity n)) (hs : 2 ≤ s) (hn : s * (16 * s + 1) ^ F.depth ≤ n) : 2 ^ s ≤ F.size

Håstad's theorem for formulas with unbounded fan-in. A formula of depth d computing the parity of n bits has at least 2 ^ s operation nodes, for every s ≥ 2 with s (16 s + 1) ^ d ≤ n.