Documentation

Complexity.Computability.Circuit.Boolean.Khrapchenko

Khrapchenko's bound #

Khrapchenko's theorem says that a De Morgan formula (see Complexity/Computability/Circuit/Boolean/Formula.lean) that is true on a set A of inputs and false on a set B has leaf size at least |E(A, B)| ^ 2 / (|A| |B|), where E(A, B) are the pairs of A × B at Hamming distance one (Formula.sq_card_hammingEdges_le, stated without division) [Khr71b], Jukna, Section 6.8. An input leaf can only separate along its own coordinate, so its edges form a matching; a binary gate splits one side, and the Cauchy–Schwarz inequality makes the measure subadditive; a negation exchanges the sides.

If every input of A has at least s₁ neighbors in B and every input of B has at least s₀ neighbors in A, a formula separating them has leaf size at least s₀ s₁ (Formula.mul_le_leafSize). So "at least k of n bits" needs leaf size k (n + 1 - k) (mul_le_leafSize_of_computes_threshold) and majority needs leaf size ⌊(n + 1) ^ 2 / 4⌋ (sq_div_four_le_leafSize_of_computes_majority) [Khr71b], and the parity of n bits, which changes with every bit, needs leaf size n ^ 2 (sq_le_leafSize_of_computes_parity) [Khr71a]. Splitting the bits in halves, x ⊕ y = (x ∧ ¬y) ∨ (¬x ∧ y) gives formulas of leaf size exactly n ^ 2 when n is a power of two (isLeast_leafSize_parity_two_pow).

Since a formula of depth d has at most 2 ^ d leaves, formulas for parity have depth at least 2 log₂ n (two_mul_log_le_depth_of_computes_parity). Here the depth counts negations; for the textbook bound, where negations are free, see Complexity/Computability/Circuit/Boolean/KhrapchenkoDepth.lean: the formula depth of the parity of 2 ^ k bits is exactly 2 k (formulaDepth_parity_two_pow).

Main definitions #

Main results #

References #

Khrapchenko's theorem #

source
theorem Cslib.Circuits.Formula.sq_card_hammingEdges_le {n : ℕ} {A B : Finset (BitString n)} (F : Formula Boolean.signature n) (hA : ∀ a ∈ A, F.eval Boolean.interpretation a = true) (hB : ∀ b ∈ B, F.eval Boolean.interpretation b = false) :
(hammingEdges A B).card ^ 2 ≤ F.leafSize * A.card * B.card

Khrapchenko's bound. A De Morgan formula that is true on A and false on B has leaf size at least |E(A, B)| ^ 2 / (|A| |B|), where E(A, B) are the pairs at Hamming distance one.

source
theorem Cslib.Circuits.Formula.mul_le_leafSize {n : ℕ} {A B : Finset (BitString n)} (F : Formula Boolean.signature n) {s₀ s₁ : ℕ} (hA : ∀ a ∈ A, F.eval Boolean.interpretation a = true) (hB : ∀ b ∈ B, F.eval Boolean.interpretation b = false) (hAne : A.Nonempty) (h₁ : ∀ a ∈ A, s₁ ≤ {b ∈ B | hammingDist a b = 1}.card) (h₀ : ∀ b ∈ B, s₀ ≤ {a ∈ A | hammingDist b a = 1}.card) :
s₀ * s₁ ≤ F.leafSize

If every input of a nonempty A has at least s₁ neighbors in B and every input of B has at least s₀ neighbors in A, a De Morgan formula that is true on A and false on B has leaf size at least s₀ s₁.

Threshold functions #

source
theorem Cslib.Circuits.Boolean.mul_le_leafSize_of_computes_threshold {n k : ℕ} {F : Formula signature n} (hF : F.Computes interpretation (threshold n k)) :
k * (n + 1 - k) ≤ F.leafSize

Khrapchenko's bound for threshold functions. A De Morgan formula computing "at least k of the n bits are true" has leaf size at least k (n + 1 - k).

source
theorem Cslib.Circuits.Boolean.sq_div_four_le_leafSize_of_computes_majority {n : ℕ} {F : Formula signature n} (hF : F.Computes interpretation (majority n)) :
(n + 1) ^ 2 / 4 ≤ F.leafSize

Khrapchenko's bound for majority. A De Morgan formula computing the majority of n bits has leaf size at least ⌊(n + 1) ^ 2 / 4⌋ = ⌊(n + 1) / 2⌋ ⌈(n + 1) / 2⌉.

Parity #

source
theorem Cslib.Circuits.Boolean.sq_le_leafSize_of_computes_parity {n : ℕ} {F : Formula signature n} (hF : F.Computes interpretation (parity n)) :
n ^ 2 ≤ F.leafSize

Khrapchenko's bound for parity. A De Morgan formula computing the parity of n bits has leaf size at least n ^ 2.

source
theorem Cslib.Circuits.Boolean.two_mul_log_le_depth_of_computes_parity {n : ℕ} {F : Formula signature n} (hF : F.Computes interpretation (parity n)) :
2 * Nat.log 2 n ≤ F.depth

A De Morgan formula computing the parity of n bits has depth at least 2 log₂ n, counting negations.

Formulas for parity #

source
theorem Cslib.Circuits.Boolean.parityOn_consecutive_add {n : ℕ} (o a b : ℕ) (x : BitString n) :
parityOn {i : Fin n | o ≤ ↑i ∧ ↑i < o + (a + b)} x = (parityOn {i : Fin n | o ≤ ↑i ∧ ↑i < o + a} x ^^ parityOn {i : Fin n | o + a ≤ ↑i ∧ ↑i < o + a + b} x)

The parity of the a + b consecutive bits from o on is the exclusive or of the parities of the first a and the last b of them.

source
theorem Cslib.Circuits.Boolean.parityOn_consecutive_one {n : ℕ} (o : ℕ) (h : o < n) (x : BitString n) :
parityOn {i : Fin n | o ≤ ↑i ∧ ↑i < o + 1} x = x ⟨o, h⟩

The parity of the single bit o is that bit.

source
def Cslib.Circuits.Boolean.parityFormula {n : ℕ} (k o : ℕ) :
o + 2 ^ k ≤ n → Formula signature n

A De Morgan formula for the parity of the 2 ^ k bits from o on, of leaf size 4 ^ k.

Instances For
    source
    theorem Cslib.Circuits.Boolean.eval_parityFormula {n : ℕ} (k o : ℕ) (h : o + 2 ^ k ≤ n) (x : BitString n) :
    (parityFormula k o h).eval interpretation x = parityOn {i : Fin n | o ≤ ↑i ∧ ↑i < o + 2 ^ k} x

    The formula parityFormula k o computes the parity of the 2 ^ k bits from o on.

    source
    theorem Cslib.Circuits.Boolean.leafSize_parityFormula {n : ℕ} (k o : ℕ) (h : o + 2 ^ k ≤ n) :
    (parityFormula k o h).leafSize = 4 ^ k

    The formula parityFormula k o has leaf size 4 ^ k.

    source
    theorem Cslib.Circuits.Boolean.exists_formula_parity_two_pow (k : ℕ) :
    ∃ (F : Formula signature (2 ^ k)), F.Computes interpretation (parity (2 ^ k)) ∧ F.leafSize = (2 ^ k) ^ 2

    Khrapchenko's bound is tight for parity: the parity of 2 ^ k bits has a De Morgan formula of leaf size (2 ^ k) ^ 2.

    source
    theorem Cslib.Circuits.Boolean.isLeast_leafSize_parity_two_pow (k : ℕ) :
    IsLeast {L : ℕ | ∃ (F : Formula signature (2 ^ k)), F.Computes interpretation (parity (2 ^ k)) ∧ F.leafSize = L} ((2 ^ k) ^ 2)

    The least leaf size of a De Morgan formula for the parity of 2 ^ k bits is (2 ^ k) ^ 2.