Flattening the sums of an unbounded fan-in formula

A formula of unbounded fan-in may nest sum gates arbitrarily deep, so its size is not bounded by its product-depth and the fan-in of its gates. Merging consecutive sum gates repairs this (original): every maximal block of sum gates of F computes a linear combination, with coefficients the products of the edge constants along the paths, of the non-sum formulas below it (SPFormula.linComb F, a finitely supported function from formulas to coefficients). Equal formulas merge into one term. SPFormula.flatten F is one sum gate over that combination, in which every product gate has its arguments flattened in turn.

flatten F computes the polynomial of F (SPFormula.polynomial_flatten), its product-depth is at most that of F (SPFormula.productDepth_flatten_le), and its size is bounded by the number of distinct subformulas of F: if F lies in a set S of formulas closed under taking arguments, with #S ≤ B and every product gate in S of fan-in at most B, then flatten F has at most (B + 1) ^ (2 * F.productDepth + 1) nodes (SPFormula.nodeCount_flatten_le). Along a path of flatten F the sum and product gates alternate, a sum gate has at most #S arguments, one for each distinct non-sum subformula, and a product gate at most B.

This is the step, left implicit in the proof of [LimayeSrinivasanTavenas2021, Lemma 15, §5, p. 12] ("by expanding it, we can transform it to a set-multilinear formula of size at most s ^ (2Δ)"), that turns a circuit of product-depth Δ into a formula of polynomial size; the circuits are unfolded in Complexity.Computability.Circuit.Arithmetic.SPCircuit.

Main definitions

• Cslib.Circuits.Arithmetic.SPFormula.ofFinsupp: the sum gate over a finitely supported linear combination of formulas.
• Cslib.Circuits.Arithmetic.SPFormula.linComb: the linear combination of non-sum formulas that a formula computes, with flattened arguments.
• Cslib.Circuits.Arithmetic.SPFormula.flatten: the flattened formula.

Main results

• Cslib.Circuits.Arithmetic.SPFormula.polynomial_flatten: the flattened formula computes the same polynomial.
• Cslib.Circuits.Arithmetic.SPFormula.productDepth_flatten_le: it is no deeper in products.
• Cslib.Circuits.Arithmetic.SPFormula.nodeCount_flatten_le (original): its size is at most (B + 1) ^ (2 * F.productDepth + 1).

References

• N. Limaye, S. Srinivasan, S. Tavenas, Superpolynomial lower bounds against low-depth algebraic circuits, ECCC TR21-081 revision 1, proof of Lemma 15 (§5, p. 12)

noncomputable def Cslib.Circuits.Arithmetic.SPFormula.ofFinsupp {K : Type u_1} {n : ℕ} [Semiring K] (f : SPFormula K n →₀ K) : SPFormula K n

The sum gate over the finitely supported linear combination f of formulas: each formula H of the support is an argument, with edge constant f H.

noncomputable def Cslib.Circuits.Arithmetic.SPFormula.linComb {K : Type u_1} {n : ℕ} [Semiring K] : SPFormula K n → SPFormula K n →₀ K

The linear combination of non-sum formulas computed by a formula: an input or a constant is itself, a sum gate is the combination of those of its arguments with its edge constants, and a product gate is itself with flattened arguments.

noncomputable def Cslib.Circuits.Arithmetic.SPFormula.flatten {K : Type u_1} {n : ℕ} [Semiring K] (F : SPFormula K n) : SPFormula K n

The flattened formula: one sum gate over the linear combination of non-sum formulas that F computes, the arguments of every product gate flattened in turn.

@[simp]

theorem Cslib.Circuits.Arithmetic.SPFormula.linComb_input {K : Type u_1} {n : ℕ} [Semiring K] (i : Fin n) : linComb (Formula.input i) = Finsupp.single (Formula.input i) 1

An input is a combination of itself.

@[simp]

theorem Cslib.Circuits.Arithmetic.SPFormula.linComb_add {K : Type u_1} {n : ℕ} [Semiring K] {m : ℕ} (c : Fin m → K) (F : Fin m → SPFormula K n) : (add c F).linComb = ∑ j : Fin m, c j • (F j).linComb

A sum gate is the combination of its arguments with its edge constants.

@[simp]

theorem Cslib.Circuits.Arithmetic.SPFormula.linComb_mul {K : Type u_1} {n : ℕ} [Semiring K] {m : ℕ} (F : Fin m → SPFormula K n) : (mul F).linComb = Finsupp.single (mul fun (j : Fin m) => (F j).flatten) 1

A product gate is a combination of itself, with flattened arguments.

@[simp]

theorem Cslib.Circuits.Arithmetic.SPFormula.linComb_const {K : Type u_1} {n : ℕ} [Semiring K] (a : K) : (const a).linComb = Finsupp.single (const a) 1

A constant is a combination of itself.

theorem Cslib.Circuits.Arithmetic.SPFormula.nodeCount_ofFinsupp {K : Type u_1} {n : ℕ} [Semiring K] (f : SPFormula K n →₀ K) : Formula.nodeCount (ofFinsupp f) = ∑ H ∈ f.support, Formula.nodeCount H + 1

The sum gate over a combination has one more node than the formulas of its support.

theorem Cslib.Circuits.Arithmetic.SPFormula.productDepth_ofFinsupp_le {K : Type u_1} {n : ℕ} [Semiring K] {f : SPFormula K n →₀ K} {t : ℕ} (h : ∀ H ∈ f.support, H.productDepth ≤ t) : (ofFinsupp f).productDepth ≤ t

The sum gate over a combination is no deeper in products than the formulas of its support.

theorem Cslib.Circuits.Arithmetic.SPFormula.productDepth_le_of_mem_support_linComb {K : Type u_1} {n : ℕ} [Semiring K] (F H : SPFormula K n) : H ∈ F.linComb.support → H.productDepth ≤ F.productDepth

The formulas of the combination of F are no deeper in products than F.

theorem Cslib.Circuits.Arithmetic.SPFormula.productDepth_flatten_le {K : Type u_1} {n : ℕ} [Semiring K] (F : SPFormula K n) : F.flatten.productDepth ≤ F.productDepth

Flattening does not increase the product-depth.

Size

theorem Cslib.Circuits.Arithmetic.SPFormula.card_support_linComb_le {K : Type u_1} {n : ℕ} [Semiring K] {S : Finset (SPFormula K n)} (hS : ∀ (op : (sigmaPiSignature K).Op) (args : Fin ((sigmaPiSignature K).Arity op) → Formula (sigmaPiSignature K) n), Formula.gate op args ∈ S → ∀ (j : Fin ((sigmaPiSignature K).Arity op)), args j ∈ S) {F : SPFormula K n} (hF : F ∈ S) : F.linComb.support.card ≤ S.card

If F lies in a set S of formulas closed under taking arguments, its combination has at most #S formulas.

theorem Cslib.Circuits.Arithmetic.SPFormula.nodeCount_ofFinsupp_le {K : Type u_1} {n : ℕ} [Semiring K] {f : SPFormula K n →₀ K} {B e : ℕ} (hf : f.support.card ≤ B) (h : ∀ H ∈ f.support, Formula.nodeCount H ≤ (B + 1) ^ e) : Formula.nodeCount (ofFinsupp f) ≤ (B + 1) ^ (e + 1)

A sum gate over at most B formulas of at most (B + 1) ^ e nodes each has at most (B + 1) ^ (e + 1) nodes.

theorem Cslib.Circuits.Arithmetic.SPFormula.nodeCount_le_of_mem_support_linComb {K : Type u_1} {n : ℕ} [Semiring K] {S : Finset (SPFormula K n)} {B : ℕ} (hS : ∀ (op : (sigmaPiSignature K).Op) (args : Fin ((sigmaPiSignature K).Arity op) → Formula (sigmaPiSignature K) n), Formula.gate op args ∈ S → ∀ (j : Fin ((sigmaPiSignature K).Arity op)), args j ∈ S) (hB : S.card ≤ B) (hmul : ∀ (m : ℕ) (args : Fin ((sigmaPiSignature K).Arity (SigmaPiOp.mul m)) → Formula (sigmaPiSignature K) n), Formula.gate (SigmaPiOp.mul m) args ∈ S → m ≤ B) {F : SPFormula K n} (hF : F ∈ S) (H : SPFormula K n) : H ∈ F.linComb.support → Formula.nodeCount H ≤ (B + 1) ^ (2 * F.productDepth)

Size of the terms of a combination (original): let F lie in a set S of formulas closed under taking arguments, with #S ≤ B and every product gate of S of fan-in at most B. Every formula of the combination of F has at most (B + 1) ^ (2 * F.productDepth) nodes.

theorem Cslib.Circuits.Arithmetic.SPFormula.nodeCount_flatten_le {K : Type u_1} {n : ℕ} [Semiring K] {S : Finset (SPFormula K n)} {B : ℕ} (hS : ∀ (op : (sigmaPiSignature K).Op) (args : Fin ((sigmaPiSignature K).Arity op) → Formula (sigmaPiSignature K) n), Formula.gate op args ∈ S → ∀ (j : Fin ((sigmaPiSignature K).Arity op)), args j ∈ S) (hB : S.card ≤ B) (hmul : ∀ (m : ℕ) (args : Fin ((sigmaPiSignature K).Arity (SigmaPiOp.mul m)) → Formula (sigmaPiSignature K) n), Formula.gate (SigmaPiOp.mul m) args ∈ S → m ≤ B) {F : SPFormula K n} (hF : F ∈ S) : Formula.nodeCount F.flatten ≤ (B + 1) ^ (2 * F.productDepth + 1)

Size of the flattened formula (original): if F lies in a set S of formulas closed under taking arguments, with #S ≤ B and every product gate of S of fan-in at most B, then flatten F has at most (B + 1) ^ (2 * F.productDepth + 1) nodes.

The computed polynomial

theorem Cslib.Circuits.Arithmetic.SPFormula.polynomial_ofFinsupp {K : Type u_1} {n : ℕ} [CommSemiring K] (f : SPFormula K n →₀ K) : (ofFinsupp f).polynomial = (Finsupp.linearCombination K polynomial) f

The sum gate over a combination computes the combination of the polynomials of its support.

theorem Cslib.Circuits.Arithmetic.SPFormula.linearCombination_linComb {K : Type u_1} {n : ℕ} [CommSemiring K] (F : SPFormula K n) : (Finsupp.linearCombination K polynomial) F.linComb = F.polynomial

The combination of the polynomials of the combination of F is the polynomial of F.

@[simp]

theorem Cslib.Circuits.Arithmetic.SPFormula.polynomial_flatten {K : Type u_1} {n : ℕ} [CommSemiring K] (F : SPFormula K n) : F.flatten.polynomial = F.polynomial

The flattened formula computes the same polynomial.