Documentation

Complexity.Computability.Circuit.Boolean.Smolensky.Approximation

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 #

Main results #

References #

source
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.

Instances For
    source
    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.

    Instances For
      source
      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.

      Instances For
        source
        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.

        source
        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.

        Instances For
          source
          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.