Documentation

Complexity.Computability.Circuit.Boolean.Yablonskii

Yablonskii's formulas for parity #

Write n = 2 ^ k + r with r ≤ 2 ^ k. Splitting the bits into blocks of 2 ^ (k - 1) + ⌊r / 2⌋ and 2 ^ (k - 1) + ⌈r / 2⌉ bits and combining formulas for their parities by x ⊕ y = (x ∧ ¬y) ∨ (¬x ∧ y) gives a De Morgan formula (see Complexity/Computability/Circuit/Boolean/Formula.lean) for the parity of n bits of leaf size at most 2 ^ k (2 ^ k + 3 r) [Yab54], [Juk12] (exists_formula_parity_two_pow_add). The bound is exactly additive along the recursion: 2 m (2 m + 3 r) = 2 · m (m + 3 s) + 2 · m (m + 3 t) for m = 2 ^ (k - 1), s = ⌊r / 2⌋ and t = ⌈r / 2⌉, and an exclusive or doubles the leaves of both arguments.

As 9 (2 ^ k + r) ^ 2 - 8 · 2 ^ k (2 ^ k + 3 r) = (2 ^ k - 3 r) ^ 2, the parity of any number n of bits has a formula of leaf size at most 9 n ^ 2 / 8 (exists_formula_parity_eight_mul_leafSize_le), within a factor 9 / 8 of Khrapchenko's lower bound n ^ 2 (sq_le_leafSize_of_computes_parity). For r = 0 the construction is the balanced formula parityFormula, whose leaf size n ^ 2 is optimal.

The formulas are balanced: they have at most 2 ⌈log₂ n⌉ AND and OR gates on every path (depthWith_binaryCost_yablonskiiFormula), so the formula depth of parity, with negations free, is at most 2 ⌈log₂ n⌉ (formulaDepth_parity_le_two_mul_clog).

Main definitions #

Main results #

References #

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

Yablonskii's formula for the parity of the 2 ^ k + r bits from o on, where r ≤ 2 ^ k: the exclusive or of such formulas for the first 2 ^ (k - 1) + ⌊r / 2⌋ and the remaining 2 ^ (k - 1) + ⌈r / 2⌉ bits. For r = 0 it is parityFormula k o (yablonskiiFormula_zero).

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

    Yablonskii's formula computes the parity of the 2 ^ k + r bits from o on.

    source
    theorem Cslib.Circuits.Boolean.leafSize_yablonskiiFormula_le {n : ℕ} (k r o : ℕ) (hr : r ≤ 2 ^ k) (h : o + (2 ^ k + r) ≤ n) :
    (yablonskiiFormula k r o hr h).leafSize ≤ 2 ^ k * (2 ^ k + 3 * r)

    Yablonskii's formula has leaf size at most 2 ^ k (2 ^ k + 3 r).

    source
    theorem Cslib.Circuits.Boolean.depthWith_binaryCost_yablonskiiFormula {n : ℕ} (k r o : ℕ) (hr : r ≤ 2 ^ k) (h : o + (2 ^ k + r) ≤ n) :
    Formula.depthWith binaryCost (yablonskiiFormula k r o hr h) = 2 * k + if r = 0 then 0 else 2

    Counting only AND and OR gates, Yablonskii's formula has depth 2 k for r = 0 and 2 (k + 1) for r > 0.

    source
    theorem Cslib.Circuits.Boolean.yablonskiiFormula_zero {n : ℕ} (k o : ℕ) (h : o + (2 ^ k + 0) ≤ n) :
    yablonskiiFormula k 0 o ⋯ h = parityFormula k o h

    For r = 0, Yablonskii's formula is the balanced formula parityFormula.

    source
    theorem Cslib.Circuits.Boolean.depthWith_binaryCost_parityFormula {n : ℕ} (k o : ℕ) (h : o + 2 ^ k ≤ n) :
    Formula.depthWith binaryCost (parityFormula k o h) = 2 * k

    Counting only AND and OR gates, the balanced formula parityFormula k o has depth 2 k.

    source
    theorem Cslib.Circuits.Boolean.computes_yablonskiiFormula (k r : ℕ) (hr : r ≤ 2 ^ k) :
    (yablonskiiFormula k r 0 hr ⋯).Computes interpretation (parity (2 ^ k + r))

    Yablonskii's formula on all 2 ^ k + r bits computes their parity.

    source
    theorem Cslib.Circuits.Boolean.computes_const_false_parity_zero :
    (Formula.const false).Computes interpretation (parity 0)

    The constant formula false computes the parity of no bits.

    source
    theorem Cslib.Circuits.Boolean.exists_formula_parity_two_pow_add {k r : ℕ} (hr : r ≤ 2 ^ k) :
    ∃ (F : Formula signature (2 ^ k + r)), F.Computes interpretation (parity (2 ^ k + r)) ∧ F.leafSize ≤ 2 ^ k * (2 ^ k + 3 * r)

    Yablonskii's bound. The parity of 2 ^ k + r bits, r ≤ 2 ^ k, has a De Morgan formula of leaf size at most 2 ^ k (2 ^ k + 3 r).

    source
    theorem Cslib.Circuits.Boolean.exists_formula_parity_eight_mul_leafSize_le (n : ℕ) :
    ∃ (F : Formula signature n), F.Computes interpretation (parity n) ∧ 8 * F.leafSize ≤ 9 * n ^ 2

    Yablonskii's bound, uniformly. The parity of n bits has a De Morgan formula of leaf size at most 9 n ^ 2 / 8.

    source
    theorem Cslib.Circuits.Boolean.formulaDepth_parity_le_two_mul_clog (n : ℕ) :
    formulaDepth (parity n) ≤ 2 * Nat.clog 2 n

    The formula depth of the parity of n bits, with negations free, is at most 2 ⌈log₂ n⌉.