Constant-depth arithmetic circuits of unbounded fan-in

Circuits in the model of Limaye, Srinivasan and Tavenas [LimayeSrinivasanTavenas2021, §1, p. 1, and footnote 1] (paraphrased): a directed acyclic graph whose leaves are variables or constants from the field, whose sum gates compute linear combinations of their children with constants on the edges, and whose product gates compute products of their children; the size is the number of nodes and the product-depth the largest number of product gates on a path from the root to a leaf.

Here a circuit is a straight-line program of the library over sigmaPiSignature K with one output (SPCircuit K N, a Cslib.Circuits.Circuit), the formulas of Complexity.Computability.Circuit.Arithmetic.SigmaPi with sharing. It computes a polynomial formally (SPCircuit.polynomial): it is evaluated in MvPolynomial (Fin N) K at the variables, as formulas are. Its product-depth (SPCircuit.productDepth) is the generic weighted depth Cslib.Circuits.Circuit.depthWith in which product gates cost one and the other operations nothing.

Size. Cslib.Circuits.Circuit.size counts the gates, constants included, but not the N input wires, so the node count of the source is C.size + N. The source's circuits are directed acyclic graphs without multiple edges (our reading of §1 and footnote 1). A program line, in contrast, may read a wire several times. For sum gates this is harmless: the edge constants of repeated wires add up. For product gates it is not: a single product gate reading the same input m times computes x ^ m at cost one, which a graph without multiple edges cannot do. So product gates read pairwise distinct wires (SPCircuit.IsSimple), this formalization's rendering of the absence of multiple edges, an original convention. Measuring the size instead by the wires read would allow multiple edges without a hypothesis, but would depart from the source's node count.

Unfolding. A circuit unfolds into a formula computing the same polynomial (SPCircuit.toSPFormula): unfold its output into a tree (Cslib.Circuits.Circuit.toFormula) and merge consecutive sum gates (SPFormula.flatten). The product-depth does not increase (SPCircuit.productDepth_toSPFormula_le) and a simple circuit of product-depth Δ unfolds into at most (C.size + N + 1) ^ (2 Δ + 1) nodes (SPCircuit.nodeCount_toSPFormula_le, original): along a path of the formula sum and product gates alternate, a sum gate reads at most one formula for each of the C.size + N wires and a product gate at most C.size + N distinct wires. The source uses such a step without proof, with the bound s ^ (2Δ) [LimayeSrinivasanTavenas2021, proof of Lemma 15, §5, p. 12], which depends on the size convention.

Main definitions

• Cslib.Circuits.Arithmetic.SPCircuit: circuits of unbounded fan-in with one output.
• Cslib.Circuits.Arithmetic.SPCircuit.IsSimple: product gates read pairwise distinct wires.
• Cslib.Circuits.Arithmetic.SPFormula.IsSimple: product gates of a formula have pairwise distinct arguments.
• Cslib.Circuits.Arithmetic.SPCircuit.productDepth, Cslib.Circuits.Arithmetic.SPCircuit.polynomial: product-depth and the computed polynomial.
• Cslib.Circuits.Arithmetic.SPCircuit.toSPFormula: the unfolded formula.

Main results

• Cslib.Circuits.Arithmetic.SPCircuit.polynomial_toSPFormula: the unfolded formula computes the polynomial of the circuit.
• Cslib.Circuits.Arithmetic.SPCircuit.productDepth_toSPFormula_le: it is no deeper in products.
• Cslib.Circuits.Arithmetic.SPCircuit.nodeCount_toSPFormula_le (original): it has at most (C.size + N + 1) ^ (2 * C.productDepth + 1) nodes.
• Cslib.Circuits.Arithmetic.SPCircuit.isSimple_toCircuit: conversely, the circuit of a simple formula is simple, computes its polynomial (SPCircuit.polynomial_toCircuit) and is no deeper in products (SPCircuit.productDepth_toCircuit_le).

References

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

@[reducible, inline]

abbrev Cslib.Circuits.Arithmetic.SPCircuit (K : Type u) (N : ℕ) : Type u

Arithmetic circuits of unbounded fan-in over K in N variables, with one output.

inductive Cslib.Circuits.Arithmetic.SPFormula.IsSimple {K : Type u} {N : ℕ} : SPFormula K N → Prop

A formula is simple when the arguments of each of its product gates are pairwise distinct formulas. Its circuit is then simple (SPCircuit.isSimple_toCircuit).

• input {K : Type u} {N : ℕ} (i : Fin N) : IsSimple (Formula.input i)

  An input is simple.

• gate {K : Type u} {N : ℕ} (op : SigmaPiOp K) (args : Fin op.arity → SPFormula K N) (hmul : ∀ (m : ℕ), op = SigmaPiOp.mul m → Function.Injective args) (hargs : ∀ (j : Fin op.arity), (args j).IsSimple) : IsSimple (Formula.gate op args)

  An operation node is simple when its arguments are, and pairwise distinct if it is a product gate.

def Cslib.Circuits.Arithmetic.SPCircuit.IsSimple {K : Type u} {N : ℕ} (C : SPCircuit K N) : Prop

A circuit is simple when each of its product gates reads pairwise distinct wires, as in a graph without multiple edges. Sum gates may read a wire several times.

def Cslib.Circuits.Arithmetic.SPCircuit.productDepth {K : Type u} {N : ℕ} (C : SPCircuit K N) : ℕ

The product-depth: the largest number of product gates on a path from the output to an input.

noncomputable def Cslib.Circuits.Arithmetic.SPCircuit.polynomial {K : Type u} {N : ℕ} [CommSemiring K] (C : SPCircuit K N) : MvPolynomial (Fin N) K

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

theorem Cslib.Circuits.Arithmetic.SPCircuit.polynomial_toFormula {K : Type u} {N : ℕ} [CommSemiring K] (C : SPCircuit K N) : SPFormula.polynomial (Circuit.toFormula C 0) = C.polynomial

The formula unfolding the output computes the polynomial of the circuit.

noncomputable def Cslib.Circuits.Arithmetic.SPCircuit.toSPFormula {K : Type u} {N : ℕ} [Semiring K] (C : SPCircuit K N) : SPFormula K N

The unfolded formula of a circuit: its output unfolded into a tree, with consecutive sum gates merged.

@[simp]

theorem Cslib.Circuits.Arithmetic.SPCircuit.polynomial_toSPFormula {K : Type u} {N : ℕ} [CommSemiring K] (C : SPCircuit K N) : C.toSPFormula.polynomial = C.polynomial

The unfolded formula computes the polynomial of the circuit.

theorem Cslib.Circuits.Arithmetic.SPCircuit.productDepth_toSPFormula_le {K : Type u} {N : ℕ} [Semiring K] (C : SPCircuit K N) : C.toSPFormula.productDepth ≤ C.productDepth

The unfolded formula is no deeper in products than the circuit.

theorem Cslib.Circuits.Arithmetic.SPCircuit.nodeCount_toSPFormula_le {K : Type u} {N : ℕ} [Semiring K] {C : SPCircuit K N} (hC : C.IsSimple) : Formula.nodeCount C.toSPFormula ≤ (C.size + N + 1) ^ (2 * C.productDepth + 1)

Size of the unfolded formula (original): a simple circuit with C.size gates and N inputs, of product-depth Δ, unfolds into a formula of at most (C.size + N + 1) ^ (2 Δ + 1) nodes.

Formulas as circuits

@[simp]

theorem Cslib.Circuits.Arithmetic.SPCircuit.polynomial_toCircuit {K : Type u} {N : ℕ} [CommSemiring K] (F : SPFormula K N) : polynomial (Formula.toCircuit F) = F.polynomial

The circuit of a formula computes the polynomial of the formula.

theorem Cslib.Circuits.Arithmetic.SPCircuit.productDepth_toCircuit_le {K : Type u} {N : ℕ} (F : SPFormula K N) : productDepth (Formula.toCircuit F) ≤ F.productDepth

The circuit of a formula is no deeper in products than the formula.

theorem Cslib.Circuits.Arithmetic.SPCircuit.isSimple_toCircuit {K : Type u} {N : ℕ} {F : SPFormula K N} (hF : F.IsSimple) : IsSimple (Formula.toCircuit F)

The circuit of a simple formula is simple.