Smolensky's approximation of circuits

A circuit of the AC⁰[p] basis of depth d agrees with a function of degree at most ((p - 1) ℓ) ^ d over any commutative ring R of characteristic p, such as ZMod p or a finite field of order p ^ k, on all but size · 2 ^ n / 2 ^ ℓ inputs (exists_lowDegree_approx) [Raz87], [Smo87].

The circuit is evaluated on pairs: the true function computed by a wire, and its approximant (pairInterpretation). An operation applied to pairs computes the true function of its arguments and applies the gate approximator of exists_gate_approx chosen for these true arguments to their approximants. So the approximants multiply degrees by (p - 1) ℓ per level of depth, and they are exact at every input where no gate approximator errs on its true arguments, which leaves at most 2 ^ n / 2 ^ ℓ inputs per gate.

Main definitions

• Cslib.Circuits.Boolean.Smolensky.inputPair: the inputs as pairs of a bit and its value in R.
• Cslib.Circuits.Boolean.Smolensky.gateApprox: the gate approximator chosen for an operation.
• Cslib.Circuits.Boolean.Smolensky.pairInterpretation: the interpretation on pairs of a true function and its approximant.
• Cslib.Circuits.Boolean.Smolensky.errorSet: the inputs on which the approximator of a gate errs.

Main results

• Cslib.Circuits.Boolean.Smolensky.exists_lowDegree_approx: Smolensky's approximation theorem.

References

• A. A. Razborov, Lower bounds on the size of bounded depth circuits over a complete basis with logical addition
• R. Smolensky, Algebraic methods in the theory of lower bounds for Boolean circuit complexity

def Cslib.Circuits.Boolean.Smolensky.inputPair {R : Type u_1} [CommRing R] {n : ℕ} (i : Fin n) : (BitString n → Bool) × (BitString n → R)

The inputs as pairs: the input bit and its value in R.

noncomputable def Cslib.Circuits.Boolean.Smolensky.gateApprox (R : Type u_1) [CommRing R] (p : ℕ) {n ℓ : ℕ} [DecidableEq R] [Fact (Nat.Prime p)] [CharP R p] (hℓ : 1 ≤ ℓ) (op : Unbounded.extSignature.Op) (u : BitString n → Fin (Unbounded.extSignature.Arity op) → Bool) : (Fin (Unbounded.extSignature.Arity op) → R) → R

The gate approximator chosen by exists_gate_approx for an operation whose arguments depend on the input as u.

theorem Cslib.Circuits.Boolean.Smolensky.gateApprox_spec (R : Type u_1) [CommRing R] (p : ℕ) {n ℓ : ℕ} [DecidableEq R] [Fact (Nat.Prime p)] [CharP R p] (hℓ : 1 ≤ ℓ) (op : Unbounded.extSignature.Op) (u : BitString n → Fin (Unbounded.extSignature.Arity op) → Bool) : (∀ (D : ℕ) (v : Fin (Unbounded.extSignature.Arity op) → BitString n → R), (∀ (k : Fin (Unbounded.extSignature.Arity op)), v k ∈ BitString.lowDegree R (Fin n) D) → (fun (x : BitString n) => gateApprox R p hℓ op u fun (k : Fin (Unbounded.extSignature.Arity op)) => v k x) ∈ BitString.lowDegree R (Fin n) ((p - 1) * ℓ * D)) ∧ {x : BitString n | (gateApprox R p hℓ op u fun (k : Fin (Unbounded.extSignature.Arity op)) => BitString.bitVal R (u x k)) ≠ BitString.bitVal R (Unbounded.extInterpretation (modGate p) op (u x))}.card * 2 ^ ℓ ≤ 2 ^ n

noncomputable def Cslib.Circuits.Boolean.Smolensky.pairInterpretation (R : Type u_1) [CommRing R] (p : ℕ) {n ℓ : ℕ} [DecidableEq R] [Fact (Nat.Prime p)] [CharP R p] (hℓ : 1 ≤ ℓ) : Interpretation Unbounded.extSignature ((BitString n → Bool) × (BitString n → R))

The interpretation on pairs of a true function and its approximant.

theorem Cslib.Circuits.Boolean.Smolensky.fst_trace_pair {R : Type u_1} [CommRing R] {p n ℓ : ℕ} [DecidableEq R] [Fact (Nat.Prime p)] [CharP R p] {g : ℕ} (hℓ : 1 ≤ ℓ) (P : Program Unbounded.extSignature n g) (w : Wire n g) (x : BitString n) : (P.trace (pairInterpretation R p hℓ) inputPair w).1 x = P.trace (Unbounded.extInterpretation (modGate p)) x w

The true functions of the pair evaluation are the gate functions of the program.

theorem Cslib.Circuits.Boolean.Smolensky.trace_pair_gate {R : Type u_1} [CommRing R] {p n ℓ : ℕ} [DecidableEq R] [Fact (Nat.Prime p)] [CharP R p] {g : ℕ} (hℓ : 1 ≤ ℓ) (P : Program Unbounded.extSignature n g) (k : Fin g) : P.trace (pairInterpretation R p hℓ) inputPair (Wire.gate k) = pairInterpretation R p hℓ (P.lines k).op fun (a : Fin (Unbounded.extSignature.Arity (P.lines k).op)) => P.trace (pairInterpretation R p hℓ) inputPair ((P.lines k).wires a)

The pair at a gate is its operation applied to the pairs at its wires.

theorem Cslib.Circuits.Boolean.Smolensky.snd_trace_pair_mem {R : Type u_1} [CommRing R] {p n ℓ : ℕ} [DecidableEq R] [Fact (Nat.Prime p)] [CharP R p] {g : ℕ} (hℓ : 1 ≤ ℓ) (P : Program Unbounded.extSignature n g) (w : Wire n g) : (P.trace (pairInterpretation R p hℓ) inputPair w).2 ∈ BitString.lowDegree R (Fin n) (((p - 1) * ℓ) ^ P.wireDepths w)

Degrees of the approximants: at most ((p - 1) ℓ) ^ depth.

noncomputable def Cslib.Circuits.Boolean.Smolensky.errorSet (R : Type u_1) [CommRing R] (p : ℕ) {n ℓ : ℕ} [DecidableEq R] [Fact (Nat.Prime p)] [CharP R p] {g : ℕ} (hℓ : 1 ≤ ℓ) (P : Program Unbounded.extSignature n g) (k : Fin g) : Finset (BitString n)

The inputs on which the approximator chosen for gate k errs on its true arguments.

theorem Cslib.Circuits.Boolean.Smolensky.card_errorSet_mul_le {R : Type u_1} [CommRing R] {p n ℓ : ℕ} [DecidableEq R] [Fact (Nat.Prime p)] [CharP R p] {g : ℕ} (hℓ : 1 ≤ ℓ) (P : Program Unbounded.extSignature n g) (k : Fin g) : (errorSet R p hℓ P k).card * 2 ^ ℓ ≤ 2 ^ n

theorem Cslib.Circuits.Boolean.Smolensky.snd_trace_pair_eq {R : Type u_1} [CommRing R] {p n ℓ : ℕ} [DecidableEq R] [Fact (Nat.Prime p)] [CharP R p] {g : ℕ} (hℓ : 1 ≤ ℓ) (P : Program Unbounded.extSignature n g) {x : BitString n} (hx : ∀ (k : Fin g), x ∉ errorSet R p hℓ P k) (w : Wire n g) : (P.trace (pairInterpretation R p hℓ) inputPair w).2 x = BitString.bitVal R ((P.trace (pairInterpretation R p hℓ) inputPair w).1 x)

Exactness of the approximants where no gate approximator errs.

theorem Cslib.Circuits.Boolean.Smolensky.exists_lowDegree_approx {R : Type u_1} [CommRing R] {p n ℓ : ℕ} [DecidableEq R] [Fact (Nat.Prime p)] [CharP R p] (hℓ : 1 ≤ ℓ) (C : Circuit Unbounded.extSignature n 1) : ∃ Q ∈ BitString.lowDegree R (Fin n) (((p - 1) * ℓ) ^ C.depth), {x : Fin n → Bool | Q x ≠ BitString.bitVal R (C.eval (Unbounded.extInterpretation (modGate p)) x 0)}.card * 2 ^ ℓ ≤ C.size * 2 ^ n

Smolensky's approximation theorem. A circuit of the AC⁰[p] basis of depth d agrees with a function of degree at most ((p - 1) ℓ) ^ d over a commutative ring R of characteristic p on all but size · 2 ^ n / 2 ^ ℓ inputs, for every ℓ ≥ 1.