Sparse corrections of Boolean circuits

Let f and g be Boolean functions with m outputs on n inputs that differ only on the inputs in a set s, and only in the outputs selected by select : Fin k → Fin m. A circuit for g is corrected into one for f as follows. Compute the indicator of s once, and compute the selected outputs of f ⊕ g by a single circuit that is only required to be correct on s. Mask each of these labels with the indicator and add it, by an exclusive or, to the corresponding output of g; the other outputs of g are kept. The mask and the exclusive or cost five De Morgan gates per selected output, so with 1_s the indicator of s and C^s complexity on s, C(f | g) ≤ C(1_s) + C^s((f ⊕ g) ∘ select) + 5 k (complexityGiven_le_of_cover). Correcting in both directions bounds |C(f) - C(g)| by the same quantity (dist_complexity_le_of_cover). For a single output, the indicator of the inputs where f and g differ is f ⊕ g itself, so |C(f) - C(g)| ≤ C(f ⊕ g) + 4 (dist_complexity_single_le_complexity_xor).

The point of keeping the indicator and the labels as two circuits shared by all outputs is that both can be much cheaper than the truth tables they encode: when s is small, 1_s is a sparse function and the labels form a partial function defined on few inputs. Bounds for the complexity of such functions turn these corrections into continuity estimates for circuit complexity; see Complexity.Computability.Circuit.Boolean.SparseSynthesis. The case of a single changed input is Cslib.Circuits.Boolean.complexity_update_le.

Main results

• Cslib.Circuits.Boolean.complexityGiven_le_of_cover: the cost of a sparse correction, given the function being corrected.
• Cslib.Circuits.Boolean.dist_complexity_le_of_cover, Cslib.Circuits.Boolean.dist_complexity_le_sum_of_cover: sparse corrections change the complexity by at most their cost.
• Cslib.Circuits.Boolean.dist_complexity_single_le_complexity_xor: |C(f) - C(g)| ≤ C(f ⊕ g) + 4.

References

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

theorem Cslib.Circuits.Boolean.dist_complexity_single_le_complexity_xor {n : ℕ} (f g : BooleanFunction n) : (complexity interpretation (single f)).dist (complexity interpretation (single g)) ≤ complexity interpretation (single fun (x : Fin n → Bool) => f x ^^ g x) + 4

Correcting a single output: the complexities of f and g differ by at most the complexity of f ⊕ g, the indicator of the inputs on which they differ, plus four gates.

theorem Cslib.Circuits.Boolean.complexityGiven_le_of_cover {n m k : ℕ} (f g : BitString n → BitString m) (s : Finset (BitString n)) (select : Fin k → Fin m) (hs : ∀ x ∉ s, f x = g x) (hselect : ∀ j ∉ Set.range select, ∀ (x : BitString n), f x j = g x j) : complexityGiven interpretation f g ≤ (complexity interpretation (single fun (x : Fin n → Bool) => decide (x ∈ s)) + complexityOn interpretation ↑s fun (x : Fin n → Bool) (i : Fin k) => f x (select i) ^^ g x (select i)) + 5 * k

Sparse correction. Suppose that f and g agree outside s, and agree on every output outside the range of select. Given the values of g, computing f costs at most the complexity of the indicator of s, plus the complexity on s of the outputs of f ⊕ g selected by select, plus five gates for each of the k indices of select.

theorem Cslib.Circuits.Boolean.dist_complexity_le_of_cover {n m k : ℕ} (f g : BitString n → BitString m) (s : Finset (BitString n)) (select : Fin k → Fin m) (hs : ∀ x ∉ s, f x = g x) (hselect : ∀ j ∉ Set.range select, ∀ (x : BitString n), f x j = g x j) : (complexity interpretation f).dist (complexity interpretation g) ≤ (complexity interpretation (single fun (x : Fin n → Bool) => decide (x ∈ s)) + complexityOn interpretation ↑s fun (x : Fin n → Bool) (i : Fin k) => f x (select i) ^^ g x (select i)) + 5 * k

Sparse correction changes complexity little. If f and g agree outside s, and agree on every output outside the range of select, then their complexities differ by at most the complexity of the indicator of s, plus the complexity on s of the outputs of f ⊕ g selected by select, plus five gates for each of the k indices of select.

theorem Cslib.Circuits.Boolean.dist_complexity_le_sum_of_cover {n m k : ℕ} (f g : BitString n → BitString m) (s : Finset (BitString n)) (select : Fin k → Fin m) (hs : ∀ x ∉ s, f x = g x) (hselect : ∀ j ∉ Set.range select, ∀ (x : BitString n), f x j = g x j) : (complexity interpretation f).dist (complexity interpretation g) ≤ complexity interpretation (single fun (x : Fin n → Bool) => decide (x ∈ s)) + ∑ i : Fin k, complexityOn interpretation (↑s) (single fun (x : Fin n → Bool) => f x (select i) ^^ g x (select i)) + 5 * k

Sparse correction with separate labels. If f and g agree outside s, and agree on every output outside the range of select, then their complexities differ by at most the complexity of the indicator of s, plus the sum over the indices i of select of the complexity on s of output select i of f ⊕ g, plus five gates for each of the k indices of select.