The approximation method

A local approximation scheme compares a circuit evaluated exactly with the same circuit evaluated in an approximate interpretation, on a finite space of samples. It gives, for every gate, a finite set of samples on which replacing the exact operation by the approximate one may go wrong, of bounded size. Evaluating the circuit approximately, the approximate value of every wire is then correct on every sample outside the union of the exception sets of the gates (program_correct), and so a circuit computing a target fails on at most as many samples as the total cost of its gates (card_failures_le_cost). Each gate is charged once, however often its value is reused.

Correctness is a relation between exact values, so that it can be one-sided, as in Razborov's method of approximations for monotone circuits Jukna, Chapter 9.

Main definitions

• Cslib.Circuits.Approximation.Scheme: a local approximation scheme.
• Cslib.Circuits.Approximation.Scheme.programExceptions: the exceptions of all gates.
• Cslib.Circuits.Approximation.Scheme.failures: the samples on which an approximate value is wrong.

Main results

• Cslib.Circuits.Approximation.Scheme.program_correct: the approximate values are correct away from the exceptions.
• Cslib.Circuits.Approximation.Scheme.card_failures_le_cost: the number of failures is at most the total cost.

References

• S. Jukna, Boolean Function Complexity: Advances and Frontiers

structure Cslib.Circuits.Approximation.Scheme {σ : Signature} {U : Type u_1} {A : Type u_2} {Sample : Type u_3} {n : ℕ} (exact : Interpretation σ U) (approx : Interpretation σ A) (decode : A → Sample → U) (exactInput : Sample → Fin n → U) (approxInput : Fin n → A) : Type (max (max (max u_1 u_2) u_3) u_4)

A local approximation scheme for the exact interpretation exact by the approximate interpretation approx, on samples Sample: decode a s reads an approximate value a on the sample s, the exact circuit inputs on a sample are exactInput s, and the approximate ones are approxInput.

• relation : U → U → Prop

  Correctness of a decoded approximate value with respect to an exact value.

• relation_trans {u v w : U} : self.relation u v → self.relation v w → self.relation u w
• map_relation (op : σ.Op) (u v : Fin (σ.Arity op) → U) : (∀ (i : Fin (σ.Arity op)), self.relation (u i) (v i)) → self.relation (exact op u) (exact op v)

  The exact operations preserve correctness.

• errorCost : σ.Op → ℕ

  The number of exceptions charged to each operation.

• exceptions (op : σ.Op) : (Fin (σ.Arity op) → A) → Finset Sample

  The samples on which applying an approximate operation to given arguments may go wrong.

• input_correct (s : Sample) (i : Fin n) : self.relation (exactInput s i) (decode (approxInput i) s)

  The approximate inputs are correct on every sample.

• gate_correct (op : σ.Op) (a : Fin (σ.Arity op) → A) (s : Sample) : s ∉ self.exceptions op a → self.relation (exact op fun (i : Fin (σ.Arity op)) => decode (a i) s) (decode (approx op a) s)

  An approximate operation is correct away from its exceptions.

• exceptions_card_le (op : σ.Op) (a : Fin (σ.Arity op) → A) : (self.exceptions op a).card ≤ self.errorCost op

def Cslib.Circuits.Approximation.Scheme.programExceptions {σ : Signature} {U : Type u_1} {A : Type u_2} {Sample : Type u_3} {n : ℕ} {exact : Interpretation σ U} {approx : Interpretation σ A} {decode : A → Sample → U} {exactInput : Sample → Fin n → U} {approxInput : Fin n → A} [DecidableEq Sample] (S : Scheme exact approx decode exactInput approxInput) {g : ℕ} : Program σ n g → Finset Sample

The exceptions of all gates of a program, applied to their approximate arguments.

@[simp]

theorem Cslib.Circuits.Approximation.Scheme.programExceptions_empty {σ : Signature} {U : Type u_1} {A : Type u_2} {Sample : Type u_3} {n : ℕ} {exact : Interpretation σ U} {approx : Interpretation σ A} {decode : A → Sample → U} {exactInput : Sample → Fin n → U} {approxInput : Fin n → A} [DecidableEq Sample] (S : Scheme exact approx decode exactInput approxInput) : S.programExceptions Program.empty = ∅

@[simp]

theorem Cslib.Circuits.Approximation.Scheme.programExceptions_gate {σ : Signature} {U : Type u_1} {A : Type u_2} {Sample : Type u_3} {n : ℕ} {exact : Interpretation σ U} {approx : Interpretation σ A} {decode : A → Sample → U} {exactInput : Sample → Fin n → U} {approxInput : Fin n → A} [DecidableEq Sample] (S : Scheme exact approx decode exactInput approxInput) {g : ℕ} (p : Program σ n g) (line : Line σ n g) : S.programExceptions (p.gate line) = S.programExceptions p ∪ S.exceptions line.op (p.trace approx approxInput ∘ line.wires)

theorem Cslib.Circuits.Approximation.Scheme.card_programExceptions_le {σ : Signature} {U : Type u_1} {A : Type u_2} {Sample : Type u_3} {n : ℕ} {exact : Interpretation σ U} {approx : Interpretation σ A} {decode : A → Sample → U} {exactInput : Sample → Fin n → U} {approxInput : Fin n → A} [DecidableEq Sample] (S : Scheme exact approx decode exactInput approxInput) {g : ℕ} (p : Program σ n g) : (S.programExceptions p).card ≤ p.cost S.errorCost

There are at most as many exceptions as the total cost of the gates.

theorem Cslib.Circuits.Approximation.Scheme.program_correct {σ : Signature} {U : Type u_1} {A : Type u_2} {Sample : Type u_3} {n : ℕ} {exact : Interpretation σ U} {approx : Interpretation σ A} {decode : A → Sample → U} {exactInput : Sample → Fin n → U} {approxInput : Fin n → A} [DecidableEq Sample] (S : Scheme exact approx decode exactInput approxInput) {g : ℕ} (p : Program σ n g) {s : Sample} (hs : s ∉ S.programExceptions p) (w : Wire n g) : S.relation (p.trace exact (exactInput s) w) (decode (p.trace approx approxInput w) s)

Away from the exceptions, the approximate value of every wire is correct.

theorem Cslib.Circuits.Approximation.Scheme.circuit_correct {σ : Signature} {U : Type u_1} {A : Type u_2} {Sample : Type u_3} {n : ℕ} {exact : Interpretation σ U} {approx : Interpretation σ A} {decode : A → Sample → U} {exactInput : Sample → Fin n → U} {approxInput : Fin n → A} [DecidableEq Sample] (S : Scheme exact approx decode exactInput approxInput) {m : ℕ} (C : Circuit σ n m) (o : Fin m) {s : Sample} (hs : s ∉ S.programExceptions C.program) : S.relation (C.eval exact (exactInput s) o) (decode (C.eval approx approxInput o) s)

Away from the exceptions, every output of a circuit is correct.

def Cslib.Circuits.Approximation.Scheme.failures {σ : Signature} {U : Type u_1} {A : Type u_2} {Sample : Type u_3} {n : ℕ} {exact : Interpretation σ U} {approx : Interpretation σ A} {decode : A → Sample → U} {exactInput : Sample → Fin n → U} {approxInput : Fin n → A} (S : Scheme exact approx decode exactInput approxInput) [DecidableRel S.relation] (samples : Finset Sample) (a : A) (target : Sample → U) : Finset Sample

The samples of samples on which the approximate value a is not correct for target.

@[simp]

theorem Cslib.Circuits.Approximation.Scheme.mem_failures {σ : Signature} {U : Type u_1} {A : Type u_2} {Sample : Type u_3} {n : ℕ} {exact : Interpretation σ U} {approx : Interpretation σ A} {decode : A → Sample → U} {exactInput : Sample → Fin n → U} {approxInput : Fin n → A} (S : Scheme exact approx decode exactInput approxInput) [DecidableRel S.relation] {samples : Finset Sample} {a : A} {target : Sample → U} {s : Sample} : s ∈ S.failures samples a target ↔ s ∈ samples ∧ ¬S.relation (target s) (decode a s)

theorem Cslib.Circuits.Approximation.Scheme.failures_subset_programExceptions {σ : Signature} {U : Type u_1} {A : Type u_2} {Sample : Type u_3} {n : ℕ} {exact : Interpretation σ U} {approx : Interpretation σ A} {decode : A → Sample → U} {exactInput : Sample → Fin n → U} {approxInput : Fin n → A} (S : Scheme exact approx decode exactInput approxInput) [DecidableRel S.relation] [DecidableEq Sample] (samples : Finset Sample) (C : Circuit σ n 1) {target : Sample → U} (hC : ∀ s ∈ samples, C.eval exact (exactInput s) 0 = target s) : S.failures samples (C.eval approx approxInput 0) target ⊆ S.programExceptions C.program

A circuit computing target exactly on the samples fails, approximately, only on exceptions.

theorem Cslib.Circuits.Approximation.Scheme.card_failures_le_cost {σ : Signature} {U : Type u_1} {A : Type u_2} {Sample : Type u_3} {n : ℕ} {exact : Interpretation σ U} {approx : Interpretation σ A} {decode : A → Sample → U} {exactInput : Sample → Fin n → U} {approxInput : Fin n → A} (S : Scheme exact approx decode exactInput approxInput) [DecidableRel S.relation] (samples : Finset Sample) (C : Circuit σ n 1) {target : Sample → U} (hC : ∀ s ∈ samples, C.eval exact (exactInput s) 0 = target s) : (S.failures samples (C.eval approx approxInput 0) target).card ≤ C.program.cost S.errorCost

The approximation method. A circuit computing target exactly on the samples fails, approximately, on at most as many of them as the total cost of its gates.