The approximation method in Hamming terms

A local approximation scheme (Cslib.Circuits.Approximation.Scheme) evaluates a circuit in an approximate interpretation and decodes each approximate value a as a function decode a on the samples. When correctness of a decoded value implies equality, the exceptions charged to the gates measure how far the decoded output of a circuit is from the function the circuit computes:

• a circuit computing f on the samples has a decoded output f̃ with d_H(f, f̃) ≤ ∑_gates errorCost(gate), the sum of the local errors of its gates (Cslib.Circuits.Approximation.Scheme.hammingDist_le_sum_errorCost);
• hence the lower-bound principle: if every gate errs on at most δ samples and f is at Hamming distance at least ε from every decoded approximate value, then ε ≤ δ C(f), so C(f) ≥ ε / δ for δ > 0 (Cslib.Circuits.Approximation.Scheme.le_mul_complexity_of_le_hammingDist), and the same with the failures of a one-sided correctness relation in place of the Hamming distance (Cslib.Circuits.Approximation.Scheme.le_mul_complexity).

Weighting the samples by μ ≥ 0, for instance a probability distribution, the union bound over the gates bounds the weight of the samples on which the approximate output fails by the sum of per-gate bounds on the weights of the gates' exceptions (Cslib.Circuits.Approximation.Scheme.sum_failures_le), with the weighted lower-bound principle as a consequence (Cslib.Circuits.Approximation.Scheme.le_mul_complexity_of_le_sum_failures).

This is a reformulation of the classical method of approximations Jukna, Chapter 9 in the language of the Hamming distance, not a new lower-bound technique, and the known limitations of the method of approximations apply to it unchanged.

Main results

• Cslib.Circuits.Approximation.Scheme.hammingDist_le_cost, Cslib.Circuits.Approximation.Scheme.hammingDist_le_sum_errorCost: the decoded output is within the total local error of the target.
• Cslib.Circuits.Approximation.Scheme.le_mul_size: every circuit computing the target has ε ≤ δ s for its number s of gates.
• Cslib.Circuits.Approximation.Scheme.le_mul_complexity, Cslib.Circuits.Approximation.Scheme.le_mul_complexity_of_le_hammingDist: the lower-bound principle ε ≤ δ C(f).
• Cslib.Circuits.Approximation.Scheme.sum_programExceptions_le, Cslib.Circuits.Approximation.Scheme.sum_failures_le: the weighted union bound.
• Cslib.Circuits.Approximation.Scheme.le_mul_complexity_of_le_sum_failures: the weighted lower-bound principle.

References

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

Lower bounds from failures

theorem Cslib.Circuits.Approximation.Scheme.le_mul_size {σ : 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) {δ ε : ℕ} (hδ : ∀ (op : σ.Op), S.errorCost op ≤ δ) (hε : ∀ (a : A), ε ≤ (S.failures samples a target).card) : ε ≤ δ * C.size

If every operation errs on at most δ samples and every approximate value fails on at least ε of the samples, then every circuit computing target on the samples has ε ≤ δ s for its number s of gates, that is, at least ε / δ gates when δ > 0.

theorem Cslib.Circuits.Approximation.Scheme.le_mul_complexity {σ : 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] [exact.IsComplete] (samples : Finset Sample) (f : (Fin n → U) → U) {δ ε : ℕ} (hδ : ∀ (op : σ.Op), S.errorCost op ≤ δ) (hε : ∀ (a : A), ε ≤ (S.failures samples a fun (s : Sample) => f (exactInput s)).card) : ε ≤ δ * complexity exact (single f)

The lower-bound principle of the approximation method: if every operation errs on at most δ samples and every approximate value fails on at least ε of the samples for f, then ε ≤ δ C(f), that is, C(f) ≥ ε / δ when δ > 0.

The Hamming distance

theorem Cslib.Circuits.Approximation.Scheme.hammingDist_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) [Fintype Sample] [DecidableEq U] (hrel : ∀ {u v : U}, S.relation u v → u = v) (C : Circuit σ n 1) {target : Sample → U} (hC : ∀ (s : Sample), C.eval exact (exactInput s) 0 = target s) : hammingDist target (decode (C.eval approx approxInput 0)) ≤ C.program.cost S.errorCost

When correctness implies equality, the decoded approximate output of a circuit computing target differs from target on at most as many samples as the total cost of its gates.

theorem Cslib.Circuits.Approximation.Scheme.hammingDist_le_sum_errorCost {σ : 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) [Fintype Sample] [DecidableEq U] (hrel : ∀ {u v : U}, S.relation u v → u = v) (C : Circuit σ n 1) {target : Sample → U} (hC : ∀ (s : Sample), C.eval exact (exactInput s) 0 = target s) : hammingDist target (decode (C.eval approx approxInput 0)) ≤ ∑ k : Fin C.size, S.errorCost (C.program.lines k).op

The decoded output is within the total local error of the target: when correctness implies equality, a circuit computing f has a decoded approximate output f̃ with d_H(f, f̃) ≤ ∑_gates errorCost(gate).

theorem Cslib.Circuits.Approximation.Scheme.le_mul_complexity_of_le_hammingDist {σ : 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) [Fintype Sample] [DecidableEq U] [exact.IsComplete] (hrel : ∀ {u v : U}, S.relation u v → u = v) (f : (Fin n → U) → U) {δ ε : ℕ} (hδ : ∀ (op : σ.Op), S.errorCost op ≤ δ) (hε : ∀ (a : A), ε ≤ hammingDist (fun (s : Sample) => f (exactInput s)) (decode a)) : ε ≤ δ * complexity exact (single f)

The lower-bound principle in Hamming terms: when correctness implies equality, if every operation errs on at most δ samples and f is at Hamming distance at least ε from every decoded approximate value, then ε ≤ δ C(f), that is, C(f) ≥ ε / δ when δ > 0.

Weighted samples

theorem Cslib.Circuits.Approximation.Scheme.sum_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} (S : Scheme exact approx decode exactInput approxInput) {μ : Sample → ℝ} {w : σ.Op → ℝ} [DecidableEq Sample] (hμ : ∀ (s : Sample), 0 ≤ μ s) (hw : ∀ (op : σ.Op) (a : Fin (σ.Arity op) → A), ∑ s ∈ S.exceptions op a, μ s ≤ w op) {g : ℕ} (p : Program σ n g) : ∑ s ∈ S.programExceptions p, μ s ≤ ∑ k : Fin g, w (p.lines k).op

The weighted union bound over the gates: if the exceptions of every operation weigh at most w op, then the exceptions of all gates of a program weigh at most the sum of w over its gates.

theorem Cslib.Circuits.Approximation.Scheme.sum_failures_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} (S : Scheme exact approx decode exactInput approxInput) {μ : Sample → ℝ} {w : σ.Op → ℝ} [DecidableRel S.relation] (hμ : ∀ (s : Sample), 0 ≤ μ s) (hw : ∀ (op : σ.Op) (a : Fin (σ.Arity op) → A), ∑ s ∈ S.exceptions op a, μ s ≤ w op) (samples : Finset Sample) (C : Circuit σ n 1) {target : Sample → U} (hC : ∀ s ∈ samples, C.eval exact (exactInput s) 0 = target s) : ∑ s ∈ S.failures samples (C.eval approx approxInput 0) target, μ s ≤ ∑ k : Fin C.size, w (C.program.lines k).op

The weighted approximation method. If the exceptions of every operation weigh at most w op, then the samples on which the approximate output of a circuit computing target fails weigh at most the sum of w over its gates. For a probability distribution μ, this bounds the probability of failure.

theorem Cslib.Circuits.Approximation.Scheme.le_mul_complexity_of_le_sum_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) {μ : Sample → ℝ} [DecidableRel S.relation] [exact.IsComplete] (hμ : ∀ (s : Sample), 0 ≤ μ s) (samples : Finset Sample) (f : (Fin n → U) → U) {δ ε : ℝ} (hδ : ∀ (op : σ.Op) (a : Fin (σ.Arity op) → A), ∑ s ∈ S.exceptions op a, μ s ≤ δ) (hε : ∀ (a : A), ε ≤ ∑ s ∈ S.failures samples a fun (s : Sample) => f (exactInput s), μ s) : ε ≤ δ * ↑(complexity exact (single f))

The weighted lower-bound principle: if the exceptions of every operation weigh at most δ and every approximate value fails for f on samples of total weight at least ε, then ε ≤ δ C(f), that is, C(f) ≥ ε / δ when δ > 0.