Arithmetic formulas of unbounded fan-in and their product-depth

The model of constant-depth algebraic circuits of Limaye, Srinivasan and Tavenas [LimayeSrinivasanTavenas2021, §1, p. 1, and footnote 1] (paraphrased): gates have unbounded fan-in, leaves are variables or constants from the field, a sum gate computes a linear combination of its children with constants labelling the edges (footnote 1), and a product gate computes the product of its children. A formula is such a circuit whose underlying graph is a tree (footnote 2). The size is the number of nodes, and the product-depth is the largest number of product gates on a path from the root to a leaf.

The signature sigmaPiSignature K has, for every m, a sum gate add m c of arity m with edge constants c : Fin m → K, a product gate mul m of arity m, and a constant const a of arity zero. Formulas over it are the library's generic Cslib.Circuits.Formulas, so their API applies unchanged. The product-depth is the generic weighted depth Formula.depthWith in which product gates cost one and the other operations nothing (SigmaPiOp.mulCost); since a gate of unbounded fan-in absorbs any number of consecutive gates of the same kind, this is the measure of the source, not of the fan-in-two arithmetic basis Cslib.Circuits.arithSignature. The size of the source is the generic Cslib.Circuits.Formula.nodeCount, the operation nodes (constants included) and the input leaves.

A sum gate add m c is the affine operation ⟨m, c, 0⟩ of Cslib.Circuits.affineSignature, with constant term b = 0: it computes ∑ j, c j * x j. The constant term is dropped here because the source's sum gates are linear, and constants are separate leaves; product gates have no affine counterpart.

A formula computes a polynomial formally: it is evaluated in MvPolynomial (Fin n) K at the variables, a constant a denoting C a (SPFormula.polynomial), as circuits do in Cslib.Circuits.Circuit.polynomial.

Set-multilinearity is relative to a partition of the variables into blocks, given by a block map blk : Fin n → Fin d. A formula is set-multilinear on a set S of blocks (SPFormula.IsSetMultilinear) when every input leaf is set-multilinear on its own block, every constant on no block, the children of a sum gate are all set-multilinear on S, and the children of a product gate are set-multilinear on pairwise disjoint sets whose union is S. Such a formula computes a polynomial homogeneous of degree #S (SPFormula.IsSetMultilinear.isHomogeneous).

This predicate is a syntactic strengthening, original to this formalization, of the definition in [LimayeSrinivasanTavenas2021, §1, p. 2], which is semantic: a circuit is set-multilinear when each of its gates computes a set-multilinear polynomial in a subset of the blocks. A semantically set-multilinear formula may contain, for example, a sum gate with children on different sets of blocks whose contributions cancel or carry the edge constant 0, such as 1 · x₁ + 0 · x₂ for variables x₁ and x₂ of different blocks. The lower bound of [LimayeSrinivasanTavenas2021, Theorem 2, p. 3] is stated for semantically set-multilinear circuits; to derive its case of formulas from results about this predicate, a normalization lemma is needed, turning a semantically set-multilinear formula into a syntactically set-multilinear one computing the same polynomial without increasing nodeCount or productDepth.

The encoding of the source's model, with edge constants on the sum gates and size as Cslib.Circuits.Formula.nodeCount, is original.

Main definitions

• Cslib.Circuits.Arithmetic.SigmaPiOp, Cslib.Circuits.Arithmetic.sigmaPiSignature: sum gates with edge constants and product gates of every arity, and constants.
• Cslib.Circuits.Arithmetic.sigmaPiInterpretationWith, Cslib.Circuits.Arithmetic.sigmaPiInterpretation: their meaning in a commutative semiring.
• Cslib.Circuits.Arithmetic.SigmaPiOp.mulCost: product gates cost one.
• Cslib.Circuits.Arithmetic.SPFormula: formulas over sigmaPiSignature K, with the helpers SPFormula.add, SPFormula.mul, SPFormula.const and SPFormula.zero.
• Cslib.Circuits.Arithmetic.SPFormula.productDepth: the largest number of product gates on a root-to-leaf path.
• Cslib.Circuits.Arithmetic.SPFormula.polynomial: the polynomial computed formally.
• Cslib.Circuits.Arithmetic.SPFormula.IsSetMultilinear: syntactically set-multilinear formulas.

Main results

• Cslib.Circuits.Arithmetic.SPFormula.polynomial_add, Cslib.Circuits.Arithmetic.SPFormula.polynomial_mul: sum gates compute linear combinations and product gates products.
• Cslib.Circuits.Arithmetic.SPFormula.aeval_polynomial, Cslib.Circuits.Arithmetic.SPFormula.eval_polynomial: evaluating the computed polynomial is evaluating the formula.
• Cslib.Circuits.Arithmetic.SPFormula.productDepth_le_depth: product-depth is at most depth.
• Cslib.Circuits.Arithmetic.SPFormula.isSetMultilinear_mul_iff and its siblings: inversion of the set-multilinearity predicate.
• Cslib.Circuits.Arithmetic.SPFormula.IsSetMultilinear.isHomogeneous (original): a set-multilinear formula on S computes a homogeneous polynomial of degree #S.

References

• N. Limaye, S. Srinivasan, S. Tavenas, Superpolynomial lower bounds against low-depth algebraic circuits, ECCC TR21-081 Revision 1, §1, pp. 1–2, and footnotes 1 and 2

inductive Cslib.Circuits.Arithmetic.SigmaPiOp (K : Type u) : Type u

The operations of unbounded fan-in arithmetic formulas: a sum gate of m arguments with edge constants c, a product gate of m arguments, and a constant.

• add {K : Type u} (m : ℕ) (c : Fin m → K) : SigmaPiOp K

  The linear combination ∑ j, c j * x j of m arguments.

• mul {K : Type u} (m : ℕ) : SigmaPiOp K

  The product of m arguments.

• const {K : Type u} (a : K) : SigmaPiOp K

  A constant.

@[reducible, inline]

abbrev Cslib.Circuits.Arithmetic.SigmaPiOp.arity {K : Type u} : SigmaPiOp K → ℕ

The arity of an operation: m for a sum or product gate of m arguments, zero for a constant.

@[reducible, inline]

abbrev Cslib.Circuits.Arithmetic.sigmaPiSignature (K : Type u) : Signature

The signature of sum gates with edge constants and product gates of unbounded fan-in, and constants. It is reducible, so that case analysis on its operations sees their arities.

def Cslib.Circuits.Arithmetic.sigmaPiInterpretationWith (K : Type u) {R : Type u_1} [CommSemiring R] (constant : K → R) : Interpretation (sigmaPiSignature K) R

Sum and product gates in a commutative semiring R, with constant symbols, edge constants included, interpreted by constant. For example, MvPolynomial.C interprets field constants as constant polynomials.

def Cslib.Circuits.Arithmetic.sigmaPiInterpretation (K : Type u) [CommSemiring K] : Interpretation (sigmaPiSignature K) K

Sum and product gates, and constants, in K itself.

@[simp]

theorem Cslib.Circuits.Arithmetic.sigmaPiInterpretationWith_add {K : Type u} {R : Type u_1} [CommSemiring R] (constant : K → R) (m : ℕ) (c : Fin m → K) (x : Fin m → R) : sigmaPiInterpretationWith K constant (SigmaPiOp.add m c) x = ∑ j : Fin m, constant (c j) * x j

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

@[simp]

theorem Cslib.Circuits.Arithmetic.sigmaPiInterpretationWith_mul {K : Type u} {R : Type u_1} [CommSemiring R] (constant : K → R) (m : ℕ) (x : Fin m → R) : sigmaPiInterpretationWith K constant (SigmaPiOp.mul m) x = ∏ j : Fin m, x j

A product gate computes the product of its arguments.

@[simp]

theorem Cslib.Circuits.Arithmetic.sigmaPiInterpretationWith_const {K : Type u} {R : Type u_1} [CommSemiring R] (constant : K → R) (a : K) (x : Fin 0 → R) : sigmaPiInterpretationWith K constant (SigmaPiOp.const a) x = constant a

A constant gate computes its constant.

def Cslib.Circuits.Arithmetic.SigmaPiOp.mulCost {K : Type u} : SigmaPiOp K → ℕ

The cost of an operation in the product-depth: product gates cost one, sum gates and constants nothing.

@[simp]

theorem Cslib.Circuits.Arithmetic.SigmaPiOp.mulCost_add {K : Type u} (m : ℕ) (c : Fin m → K) : (add m c).mulCost = 0

A sum gate does not count towards the product-depth.

@[simp]

theorem Cslib.Circuits.Arithmetic.SigmaPiOp.mulCost_mul {K : Type u} (m : ℕ) : (mul m).mulCost = 1

A product gate counts one towards the product-depth.

@[simp]

theorem Cslib.Circuits.Arithmetic.SigmaPiOp.mulCost_const {K : Type u} (a : K) : (const a).mulCost = 0

A constant does not count towards the product-depth.

theorem Cslib.Circuits.Arithmetic.SigmaPiOp.mulCost_le_one {K : Type u} (op : SigmaPiOp K) : op.mulCost ≤ 1

Every operation costs at most one in the product-depth.

@[reducible, inline]

abbrev Cslib.Circuits.Arithmetic.SPFormula (K : Type u) (n : ℕ) : Type u

Arithmetic formulas of unbounded fan-in over K in n variables.

@[reducible, inline]

abbrev Cslib.Circuits.Arithmetic.SPFormula.add {K : Type u} {n m : ℕ} (c : Fin m → K) (F : Fin m → SPFormula K n) : SPFormula K n

The sum gate with edge constants c over the formulas F.

@[reducible, inline]

abbrev Cslib.Circuits.Arithmetic.SPFormula.mul {K : Type u} {n m : ℕ} (F : Fin m → SPFormula K n) : SPFormula K n

The product gate over the formulas F.

@[reducible, inline]

abbrev Cslib.Circuits.Arithmetic.SPFormula.const {K : Type u} {n : ℕ} (a : K) : SPFormula K n

The constant a.

@[reducible, inline]

abbrev Cslib.Circuits.Arithmetic.SPFormula.zero {K : Type u} {n : ℕ} : SPFormula K n

The formula 0: a sum gate without arguments. It computes 0 and is set-multilinear on every set of blocks (SPFormula.isSetMultilinear_zero).

Product-depth and size

The size of a formula is the generic Cslib.Circuits.Formula.nodeCount, the size in the sense of [LimayeSrinivasanTavenas2021, §1, p. 1]: its operation nodes, constants included, and its input leaves.

def Cslib.Circuits.Arithmetic.SPFormula.productDepth {K : Type u} {n : ℕ} (F : SPFormula K n) : ℕ

The product-depth: the largest number of product gates on a path from the root to a leaf.

@[simp]

theorem Cslib.Circuits.Arithmetic.SPFormula.productDepth_input {K : Type u} {n : ℕ} (i : Fin n) : productDepth (Formula.input i) = 0

An input has product-depth zero.

@[simp]

theorem Cslib.Circuits.Arithmetic.SPFormula.productDepth_add {K : Type u} {n m : ℕ} (c : Fin m → K) (F : Fin m → SPFormula K n) : (add c F).productDepth = Finset.univ.sup fun (j : Fin m) => (F j).productDepth

A sum gate has the largest product-depth of its arguments.

@[simp]

theorem Cslib.Circuits.Arithmetic.SPFormula.productDepth_mul {K : Type u} {n m : ℕ} (F : Fin m → SPFormula K n) : (mul F).productDepth = (Finset.univ.sup fun (j : Fin m) => (F j).productDepth) + 1

A product gate is one deeper than its arguments.

@[simp]

theorem Cslib.Circuits.Arithmetic.SPFormula.productDepth_const {K : Type u} {n : ℕ} (a : K) : (const a).productDepth = 0

A constant has product-depth zero.

theorem Cslib.Circuits.Arithmetic.SPFormula.productDepth_zero {K : Type u} {n : ℕ} : zero.productDepth = 0

The formula 0 has product-depth zero.

theorem Cslib.Circuits.Arithmetic.SPFormula.productDepth_le_depth {K : Type u} {n : ℕ} (F : SPFormula K n) : F.productDepth ≤ Formula.depth F

The product-depth is at most the depth.

@[simp]

theorem Cslib.Circuits.Arithmetic.SPFormula.nodeCount_const {K : Type u} {n : ℕ} (a : K) : Formula.nodeCount (const a) = 1

A constant is one node; the size of the source counts constant leaves.

@[simp]

theorem Cslib.Circuits.Arithmetic.SPFormula.nodeCount_zero {K : Type u} {n : ℕ} : Formula.nodeCount zero = 1

The formula 0 is one node.

The computed polynomial

noncomputable def Cslib.Circuits.Arithmetic.SPFormula.polynomial {K : Type u} {n : ℕ} [CommSemiring K] (F : SPFormula K n) : MvPolynomial (Fin n) K

The polynomial computed formally by a formula: the formula evaluated in MvPolynomial (Fin n) K at the variables, a constant a denoting C a.

@[simp]

theorem Cslib.Circuits.Arithmetic.SPFormula.polynomial_input {K : Type u} {n : ℕ} [CommSemiring K] (i : Fin n) : polynomial (Formula.input i) = MvPolynomial.X i

An input computes its variable.

@[simp]

theorem Cslib.Circuits.Arithmetic.SPFormula.polynomial_add {K : Type u} {n : ℕ} [CommSemiring K] {m : ℕ} (c : Fin m → K) (F : Fin m → SPFormula K n) : (add c F).polynomial = ∑ j : Fin m, MvPolynomial.C (c j) * (F j).polynomial

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

@[simp]

theorem Cslib.Circuits.Arithmetic.SPFormula.polynomial_mul {K : Type u} {n : ℕ} [CommSemiring K] {m : ℕ} (F : Fin m → SPFormula K n) : (mul F).polynomial = ∏ j : Fin m, (F j).polynomial

A product gate computes the product of its arguments.

@[simp]

theorem Cslib.Circuits.Arithmetic.SPFormula.polynomial_const {K : Type u} {n : ℕ} [CommSemiring K] (a : K) : (const a).polynomial = MvPolynomial.C a

A constant computes the constant polynomial.

theorem Cslib.Circuits.Arithmetic.SPFormula.polynomial_zero {K : Type u} {n : ℕ} [CommSemiring K] : zero.polynomial = 0

The formula 0 computes 0.

theorem Cslib.Circuits.Arithmetic.SPFormula.aeval_polynomial {K : Type u} {n : ℕ} [CommSemiring K] {R : Type u_1} [CommSemiring R] [Algebra K R] (F : SPFormula K n) (x : Fin n → R) : (MvPolynomial.aeval x) F.polynomial = Formula.eval F (sigmaPiInterpretationWith K ⇑(algebraMap K R)) x

Evaluating the polynomial computed by a formula at a point of a commutative K-algebra is evaluating the formula there.

@[simp]

theorem Cslib.Circuits.Arithmetic.SPFormula.eval_polynomial {K : Type u} {n : ℕ} [CommSemiring K] (F : SPFormula K n) (x : Fin n → K) : (MvPolynomial.eval x) F.polynomial = Formula.eval F (sigmaPiInterpretation K) x

Evaluating the polynomial computed by a formula at a point of K is evaluating the formula under sigmaPiInterpretation K.

Set-multilinear formulas

inductive Cslib.Circuits.Arithmetic.SPFormula.IsSetMultilinear {K : Type u} {n d : ℕ} (blk : Fin n → Fin d) : SPFormula K n → Finset (Fin d) → Prop

A formula is set-multilinear on the set S of blocks, for the partition of the variables into blocks given by blk, when every input is set-multilinear on its own block, every constant on no block, the arguments of a sum gate are all set-multilinear on S, and the arguments of a product gate are set-multilinear on pairwise disjoint sets of blocks whose union is S.

This is a syntactic strengthening, original to this formalization, of the semantic definition of [LimayeSrinivasanTavenas2021, §1, p. 2], where each gate must compute a set-multilinear polynomial in a subset of the blocks; see the module docstring.

• input {K : Type u} {n d : ℕ} {blk : Fin n → Fin d} (i : Fin n) : IsSetMultilinear blk (Formula.input i) {blk i}

  An input is set-multilinear on its own block.

• const {K : Type u} {n d : ℕ} {blk : Fin n → Fin d} (a : K) : IsSetMultilinear blk (SPFormula.const a) ∅

  A constant is set-multilinear on no block.

• add {K : Type u} {n d : ℕ} {blk : Fin n → Fin d} {m : ℕ} (c : Fin m → K) (F : Fin m → SPFormula K n) (S : Finset (Fin d)) (hF : ∀ (j : Fin m), IsSetMultilinear blk (F j) S) : IsSetMultilinear blk (SPFormula.add c F) S

  A sum gate is set-multilinear on S when all its arguments are.

• mul {K : Type u} {n d : ℕ} {blk : Fin n → Fin d} {m : ℕ} (F : Fin m → SPFormula K n) (T : Fin m → Finset (Fin d)) (hT : Pairwise (Function.onFun Disjoint T)) (hF : ∀ (j : Fin m), IsSetMultilinear blk (F j) (T j)) : IsSetMultilinear blk (SPFormula.mul F) (Finset.univ.biUnion T)

  A product gate is set-multilinear on the union of pairwise disjoint sets of blocks on which its arguments are set-multilinear.

theorem Cslib.Circuits.Arithmetic.SPFormula.isSetMultilinear_input_iff {K : Type u} {n d : ℕ} {blk : Fin n → Fin d} {i : Fin n} {S : Finset (Fin d)} : IsSetMultilinear blk (Formula.input i) S ↔ S = {blk i}

An input is set-multilinear exactly on its own block.

theorem Cslib.Circuits.Arithmetic.SPFormula.isSetMultilinear_const_iff {K : Type u} {n d : ℕ} {blk : Fin n → Fin d} {a : K} {S : Finset (Fin d)} : IsSetMultilinear blk (const a) S ↔ S = ∅

A constant is set-multilinear exactly on no block.

theorem Cslib.Circuits.Arithmetic.SPFormula.isSetMultilinear_add_iff {K : Type u} {n d : ℕ} {blk : Fin n → Fin d} {m : ℕ} {c : Fin m → K} {F : Fin m → SPFormula K n} {S : Finset (Fin d)} : IsSetMultilinear blk (add c F) S ↔ ∀ (j : Fin m), IsSetMultilinear blk (F j) S

A sum gate is set-multilinear on S exactly when all its arguments are.

theorem Cslib.Circuits.Arithmetic.SPFormula.isSetMultilinear_mul_iff {K : Type u} {n d : ℕ} {blk : Fin n → Fin d} {m : ℕ} {F : Fin m → SPFormula K n} {S : Finset (Fin d)} : IsSetMultilinear blk (mul F) S ↔ ∃ (T : Fin m → Finset (Fin d)), Pairwise (Function.onFun Disjoint T) ∧ (∀ (j : Fin m), IsSetMultilinear blk (F j) (T j)) ∧ S = Finset.univ.biUnion T

A product gate is set-multilinear on S exactly when its arguments are set-multilinear on pairwise disjoint sets of blocks whose union is S.

theorem Cslib.Circuits.Arithmetic.SPFormula.isSetMultilinear_zero {K : Type u} {n d : ℕ} {blk : Fin n → Fin d} (S : Finset (Fin d)) : IsSetMultilinear blk zero S

The formula 0, a sum gate without arguments, is set-multilinear on every set of blocks.

theorem Cslib.Circuits.Arithmetic.SPFormula.IsSetMultilinear.isHomogeneous {K : Type u} {n d : ℕ} {blk : Fin n → Fin d} [CommSemiring K] {F : SPFormula K n} {S : Finset (Fin d)} (h : IsSetMultilinear blk F S) : F.polynomial.IsHomogeneous S.card

A set-multilinear formula on S computes a homogeneous polynomial of degree #S (original).