Spira's theorem: balancing formulas

Spira's theorem [Spi71], Jukna, Chapter 6: every De Morgan formula with L leaves has an equivalent formula with at most 4 ⌈log₂ L⌉ AND and OR gates on every path (Boolean.exists_formula_depthWith_le_four_mul_clog). Conversely a formula with at most d AND and OR gates on every path has at most 2 ^ d leaves (Boolean.leafSize_le_two_pow_depthWith_binaryCost). So the formula depth of a function is at most four times the logarithm of the leaf size of any formula for it (Boolean.formulaDepth_le_four_mul_clog), and some formula for it has at most 2 to the formula depth leaves (Boolean.exists_computes_leafSize_le_two_pow_formulaDepth).

The proof splits a formula F with L leaves at a subformula G with between L / 3 and 2 L / 3 leaves, found by walking from the root towards the argument with the most leaves (Formula.exists_split, for any basis of fan-in at most two). Then F ≡ (G ∧ F[G := 1]) ∨ (¬G ∧ F[G := 0]), where each of the three formulas has at most 2 L / 3 leaves and is balanced recursively, at the cost of two AND and OR gates per level.

Main results

• Cslib.Circuits.Formula.exists_split: a subformula with between a third and two thirds of the leaves, and its context.
• Cslib.Circuits.Boolean.exists_formula_depthWith_le_four_mul_clog: Spira's theorem.
• Cslib.Circuits.Boolean.leafSize_le_two_pow_depthWith_binaryCost: the converse bound.
• Cslib.Circuits.Boolean.formulaDepth_le_four_mul_clog, Cslib.Circuits.Boolean.exists_computes_leafSize_le_two_pow_formulaDepth: formula depth and the logarithm of formula leaf size agree up to a factor of four.

References

• P. M. Spira, On time-hardware complexity tradeoffs for Boolean functions
• S. Jukna, Boolean Function Complexity: Advances and Frontiers

theorem Cslib.Circuits.Formula.exists_split {n : ℕ} {σ : Signature} (hσ : ∀ (op : σ.Op), σ.Arity op ≤ 2) {L : ℕ} (hL : 2 ≤ L) (H : Formula σ n) (hH : 2 * L < 3 * H.leafSize) : ∃ (G : Formula σ n) (C : Formula σ (n + 1)), C.substLast G = H ∧ L < 3 * G.leafSize ∧ 3 * G.leafSize ≤ 2 * L ∧ ∀ (K : Formula σ n), (C.substLast K).leafSize + G.leafSize = H.leafSize + K.leafSize

A balanced split. In a formula over a basis of fan-in at most two with more than 2 L / 3 leaves, for L ≥ 2, walking towards the argument with the most leaves reaches a subformula G with more than L / 3 and at most 2 L / 3 leaves. The rest of the formula is a context C with one hole, its last input: plugging G into C gives back the formula, and plugging a formula K into C replaces the leaves of G by those of K.

theorem Cslib.Circuits.Boolean.exists_formula_depthWith_le_four_mul_clog {n : ℕ} (F : Formula signature n) : ∃ (G : Formula signature n), (∀ (x : Fin n → Bool), G.eval interpretation x = F.eval interpretation x) ∧ Formula.depthWith binaryCost G ≤ 4 * Nat.clog 2 F.leafSize

Spira's theorem. Every De Morgan formula with L leaves has an equivalent formula with at most 4 ⌈log₂ L⌉ AND and OR gates on every path.

theorem Cslib.Circuits.Boolean.leafSize_le_two_pow_depthWith_binaryCost {n : ℕ} (F : Formula signature n) : F.leafSize ≤ 2 ^ Formula.depthWith binaryCost F

A De Morgan formula with at most d AND and OR gates on every path has at most 2 ^ d leaves.

theorem Cslib.Circuits.Boolean.formulaDepth_le_four_mul_clog {n : ℕ} {f : BooleanFunction n} {F : Formula signature n} (hF : F.Computes interpretation f) : formulaDepth f ≤ 4 * Nat.clog 2 F.leafSize

The formula depth of a function is at most 4 ⌈log₂ L⌉ for every formula with L leaves computing it.

theorem Cslib.Circuits.Boolean.exists_computes_leafSize_le_two_pow_formulaDepth {n : ℕ} (f : BooleanFunction n) : ∃ (F : Formula signature n), F.Computes interpretation f ∧ F.leafSize ≤ 2 ^ formulaDepth f

Conversely, some formula for a function has at most 2 ^ d leaves, where d is its formula depth.