p-families, p-projections and Valiant's class VP

Valiant's algebraic analogue of P [Val79a], in the form of Bürgisser, Chapter 2. A family of polynomials over K has, for every n, a polynomial poly n in vars n variables. It is a p-family when the number of variables and the total degree are polynomially bounded in n. A p-family is in VP K when it is computed by arithmetic circuits of polynomially bounded size.

Arithmetic circuits are the library's circuits over Cslib.Circuits.arithSignature K: addition and multiplication of fan-in two and a constant gate for each element of K. A circuit computes a polynomial formally: it is evaluated in MvPolynomial (Fin n) K at the variables (Cslib.Circuits.Circuit.polynomial). Over a finite field this is stronger than computing the polynomial function. Size counts every gate, constant gates included, and there is no subtraction gate. Bürgisser counts arithmetic operations, subtraction among them, with constants free; translating between the two conventions changes sizes by at most a constant factor and does not change the class (a remark, not formalized here).

The definitions are those of the literature, with three points made explicit.

• Degree. The degree bound is part of the definition of VP, as in Valiant's. Small circuits alone do not suffice: X ^ 2 ^ n has circuits with at most n gates but is not in VP (exists_circuit_pow_two_pow, powTwoPowFamily_not_mem_VP).
• Uniformity. VP is nonuniform. Nothing relates the circuits for different n, and no machine is required to construct them.
• Coefficients. Valiant works over a field. The definitions make sense over every commutative semiring K, and are stated there. Hypotheses on K, such as its characteristic, appear only in the theorems that need them.

A polynomial P is a projection of Q when P arises from Q by substituting for each variable of Q a variable of P or a constant. A family f is a p-projection of g when each f n is a projection of g (t n) for a polynomially bounded t. Projections are Valiant's reductions; VP is closed under them.

Main definitions

• Cslib.Circuits.Circuit.polynomial: the formal polynomial computed by an arithmetic circuit.
• Cslib.Circuits.Arithmetic.PolynomialFamily, PolynomialFamily.IsPFamily: families of polynomials and p-families.
• Cslib.Circuits.Arithmetic.projection, Cslib.Circuits.Arithmetic.IsProjection: substitution of variables and constants, and projections.
• Cslib.Circuits.Arithmetic.PolynomialFamily.IsPProjection: p-projections.
• Cslib.Circuits.Arithmetic.projectionCircuit: the circuit supplying a projection's substitution.
• Cslib.Circuits.Arithmetic.VP: Valiant's class VP.
• Cslib.Circuits.Arithmetic.powTwoPowFamily: the family X ^ 2 ^ n.

Main results

• Cslib.Circuits.Circuit.aeval_polynomial: evaluating the computed polynomial in a commutative algebra is evaluating the circuit there; Cslib.Circuits.Circuit.eval_polynomial is the case of the base ring.
• Cslib.Circuits.Arithmetic.IsProjection.trans, Cslib.Circuits.Arithmetic.PolynomialFamily.IsPProjection.trans: projections compose.
• Cslib.Circuits.Arithmetic.totalDegree_projection_le: projections do not raise the degree.
• Cslib.Circuits.Synthesis.arith_const, Cslib.Circuits.Synthesis.arith_add, Cslib.Circuits.Synthesis.arith_mul, Cslib.Circuits.Synthesis.arith_sum: synthesis rules for arithmetic circuits.
• Cslib.Circuits.Synthesis.exists_circuit_polynomial: a synthesis bound gives a circuit computing the polynomial.
• Cslib.Circuits.Arithmetic.VP.of_isPProjection: VP is closed under p-projections.
• Cslib.Circuits.Arithmetic.VP.of_synthesis: p-families synthesized within a polynomial budget are in VP.
• Cslib.Circuits.Arithmetic.exists_circuit_pow_two_pow, Cslib.Circuits.Arithmetic.powTwoPowFamily_not_mem_VP: repeated squaring has small circuits but is not in VP, whose definition bounds the degree.

References

• L. G. Valiant, Completeness classes in algebra
• P. Bürgisser, Completeness and Reduction in Algebraic Complexity Theory, Chapter 2

noncomputable def Cslib.Circuits.Circuit.polynomial {K : Type u} [CommSemiring K] {n m : ℕ} (c : Circuit (arithSignature K) n m) (j : Fin m) : MvPolynomial (Fin n) K

The formal polynomial computed at output j of an arithmetic circuit with constants from K: the circuit evaluated in MvPolynomial (Fin n) K at the variables, the constant symbol a denoting the constant polynomial C a.

theorem Cslib.Circuits.Circuit.aeval_polynomial {K : Type u} [CommSemiring K] {n m : ℕ} {R : Type u_1} [CommSemiring R] [Algebra K R] (c : Circuit (arithSignature K) n m) (x : Fin n → R) (j : Fin m) : (MvPolynomial.aeval x) (c.polynomial j) = c.eval (arithInterpretationWith K ⇑(algebraMap K R)) x j

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

theorem Cslib.Circuits.Circuit.aeval_polynomial_mvPolynomial {K : Type u} [CommSemiring K] {n m : ℕ} {σ : Type u_1} (c : Circuit (arithSignature K) n m) (x : Fin n → MvPolynomial σ K) (j : Fin m) : (MvPolynomial.aeval x) (c.polynomial j) = c.eval (arithInterpretationWith K ⇑MvPolynomial.C) x j

Substituting polynomials for the variables of the polynomial computed by a circuit is evaluating the circuit at those polynomials.

@[simp]

theorem Cslib.Circuits.Circuit.eval_polynomial {K : Type u} [CommSemiring K] {n m : ℕ} (c : Circuit (arithSignature K) n m) (x : Fin n → K) (j : Fin m) : (MvPolynomial.eval x) (c.polynomial j) = c.eval (arithInterpretation K) x j

Evaluating the formal polynomial computed by an arithmetic circuit at x : Fin n → K agrees with evaluating the circuit under arithInterpretation K.

Synthesis of arithmetic circuits

theorem Cslib.Circuits.Synthesis.arith_const {K : Type u} {n : ℕ} {R : Type u_1} {constant : K → R} {s : Set ((Fin n → R) → R)} [Add R] [Mul R] (a : K) : Synthesis (arithInterpretationWith K constant) s {fun (x : Fin n → R) => constant a} 1

A constant costs one gate.

theorem Cslib.Circuits.Synthesis.arith_add {K : Type u} {n : ℕ} {R : Type u_1} {constant : K → R} {s : Set ((Fin n → R) → R)} {f g : (Fin n → R) → R} [Add R] [Mul R] (hf : f ∈ s) (hg : g ∈ s) : Synthesis (arithInterpretationWith K constant) s {fun (x : Fin n → R) => f x + g x} 1

The sum of two available functions costs one gate.

theorem Cslib.Circuits.Synthesis.arith_mul {K : Type u} {n : ℕ} {R : Type u_1} {constant : K → R} {s : Set ((Fin n → R) → R)} {f g : (Fin n → R) → R} [Add R] [Mul R] (hf : f ∈ s) (hg : g ∈ s) : Synthesis (arithInterpretationWith K constant) s {fun (x : Fin n → R) => f x * g x} 1

The product of two available functions costs one gate.

theorem Cslib.Circuits.Synthesis.arith_sum {K : Type u} {n : ℕ} {R : Type u_1} {constant : K → R} {s : Set ((Fin n → R) → R)} {ι : Type u_2} [AddCommMonoid R] [Mul R] (indices : Finset ι) (summand : ι → (Fin n → R) → R) (cost : ι → ℕ) (hzero : (fun (x : Fin n → R) => 0) ∈ s) (h : ∀ i ∈ indices, Synthesis (arithInterpretationWith K constant) s {summand i} (cost i)) : Synthesis (arithInterpretationWith K constant) s {fun (x : Fin n → R) => ∑ i ∈ indices, summand i x} (∑ i ∈ indices, (cost i + 1))

A finite sum costs its summands and one addition each, when zero is available.

theorem Cslib.Circuits.Synthesis.exists_circuit_polynomial {K : Type u} [CommSemiring K] {n : ℕ} {F : (Fin n → MvPolynomial (Fin n) K) → MvPolynomial (Fin n) K} {cost : ℕ} (h : Synthesis (arithInterpretationWith K ⇑MvPolynomial.C) (inputs n) {F} cost) : ∃ (c : Circuit (arithSignature K) n 1), c.polynomial 0 = F MvPolynomial.X ∧ c.size ≤ cost

A synthesis bound on a function F from the inputs gives a circuit, within the bound, computing the polynomial F X.

structure Cslib.Circuits.Arithmetic.PolynomialFamily (K : Type u) [CommSemiring K] : Type u

A family of polynomials over K: for every n, a polynomial poly n in vars n variables.

• vars : ℕ → ℕ

  The number of variables of each member.

• poly (n : ℕ) : MvPolynomial (Fin (self.vars n)) K

  The members of the family.

def Cslib.Circuits.Arithmetic.PolynomialFamily.IsPFamily {K : Type u} [CommSemiring K] (f : PolynomialFamily K) : Prop

A p-family Bürgisser, Chapter 2: the number of variables and the total degree are polynomially bounded.

Projections

noncomputable def Cslib.Circuits.Arithmetic.projection {K : Type u} [CommSemiring K] {σ : Type u_1} {τ : Type u_2} (ρ : τ → σ ⊕ K) : MvPolynomial τ K →ₐ[K] MvPolynomial σ K

Substitute for each variable i of a polynomial over τ the variable X k when ρ i = Sum.inl k, and the constant C a when ρ i = Sum.inr a.

@[simp]

theorem Cslib.Circuits.Arithmetic.projection_X {K : Type u} [CommSemiring K] {σ : Type u_1} {τ : Type u_2} (ρ : τ → σ ⊕ K) (i : τ) : (projection ρ) (MvPolynomial.X i) = Sum.elim MvPolynomial.X (fun (a : K) => MvPolynomial.C a) (ρ i)

theorem Cslib.Circuits.Arithmetic.projection_C {K : Type u} [CommSemiring K] {σ : Type u_1} {τ : Type u_2} (ρ : τ → σ ⊕ K) (a : K) : (projection ρ) (MvPolynomial.C a) = MvPolynomial.C a

@[simp]

theorem Cslib.Circuits.Arithmetic.projection_inl {K : Type u} [CommSemiring K] {σ : Type u_1} : projection Sum.inl = AlgHom.id K (MvPolynomial σ K)

Substituting every variable for itself changes nothing.

theorem Cslib.Circuits.Arithmetic.projection_projection {K : Type u} [CommSemiring K] {σ : Type u_1} {τ : Type u_2} {υ : Type u_3} (ρ : σ → υ ⊕ K) (ρ' : τ → σ ⊕ K) (P : MvPolynomial τ K) : (projection ρ) ((projection ρ') P) = (projection fun (i : τ) => Sum.elim ρ Sum.inr (ρ' i)) P

Two successive projections are one projection: a variable substituted for a variable is substituted in turn, and a constant stays.

def Cslib.Circuits.Arithmetic.IsProjection {K : Type u} [CommSemiring K] {σ : Type u_1} {τ : Type u_2} (P : MvPolynomial σ K) (Q : MvPolynomial τ K) : Prop

P is a projection of Q [Val79a]: substituting for each variable of Q a variable of P or a constant of K gives P.

theorem Cslib.Circuits.Arithmetic.IsProjection.refl {K : Type u} [CommSemiring K] {σ : Type u_1} (P : MvPolynomial σ K) : IsProjection P P

Every polynomial is a projection of itself.

theorem Cslib.Circuits.Arithmetic.IsProjection.trans {K : Type u} [CommSemiring K] {σ : Type u_1} {τ : Type u_2} {υ : Type u_3} {P : MvPolynomial υ K} {Q : MvPolynomial σ K} {R : MvPolynomial τ K} (hPQ : IsProjection P Q) (hQR : IsProjection Q R) : IsProjection P R

A projection of a projection is a projection.

theorem Cslib.Circuits.Arithmetic.totalDegree_projection_le {K : Type u} [CommSemiring K] {σ : Type u_1} {τ : Type u_2} (ρ : τ → σ ⊕ K) (P : MvPolynomial τ K) : ((projection ρ) P).totalDegree ≤ P.totalDegree

Projections do not raise the total degree.

def Cslib.Circuits.Arithmetic.PolynomialFamily.IsPProjection {K : Type u} [CommSemiring K] (f g : PolynomialFamily K) : Prop

f is a p-projection of g Valiant1979Algebra; Bürgisser, Chapter 2: for a polynomially bounded t, every f.poly n is a projection of g.poly (t n).

theorem Cslib.Circuits.Arithmetic.PolynomialFamily.IsPProjection.refl {K : Type u} [CommSemiring K] (f : PolynomialFamily K) : f.IsPProjection f

Every family is a p-projection of itself.

theorem Cslib.Circuits.Arithmetic.PolynomialFamily.IsPProjection.trans {K : Type u} [CommSemiring K] {f g h : PolynomialFamily K} (hfg : f.IsPProjection g) (hgh : g.IsPProjection h) : f.IsPProjection h

A p-projection of a p-projection is a p-projection.

Circuits for projections

def Cslib.Circuits.Arithmetic.projectionCircuit {K : Type u} {n m : ℕ} (ρ : Fin m → Fin n ⊕ K) : Circuit (arithSignature K) n m

The circuit supplying the substitution of a projection: output i is input k when ρ i = Sum.inl k, and a constant gate for a when ρ i = Sum.inr a.

@[simp]

theorem Cslib.Circuits.Arithmetic.eval_projectionCircuit {K : Type u} {n m : ℕ} {R : Type u_1} [Add R] [Mul R] (constant : K → R) (ρ : Fin m → Fin n ⊕ K) (x : Fin n → R) (i : Fin m) : (projectionCircuit ρ).eval (arithInterpretationWith K constant) x i = Sum.elim x constant (ρ i)

theorem Cslib.Circuits.Arithmetic.size_projectionCircuit_le {K : Type u} {n m : ℕ} (ρ : Fin m → Fin n ⊕ K) : (projectionCircuit ρ).size ≤ m

The substitution of a projection needs at most one gate per substituted variable.

theorem Cslib.Circuits.Arithmetic.polynomial_comp_projectionCircuit {K : Type u} [CommSemiring K] {n m p : ℕ} (c : Circuit (arithSignature K) m p) (ρ : Fin m → Fin n ⊕ K) (j : Fin p) : (c.comp (projectionCircuit ρ)).polynomial j = (projection ρ) (c.polynomial j)

Feeding the substitution of a projection to a circuit computes the projection of its polynomial.

The class VP

def Cslib.Circuits.Arithmetic.VP (K : Type u) [CommSemiring K] : Set (PolynomialFamily K)

Valiant's class VP over K Valiant1979Algebra; Bürgisser, Chapter 2: the p-families computed, for some polynomially bounded size function, by arithmetic circuits of that size. Nothing relates the circuits for different n: the class is nonuniform. The circuits compute the members as formal polynomials, and their degrees are bounded by the p-family condition.

theorem Cslib.Circuits.Arithmetic.VP.isPFamily {K : Type u} [CommSemiring K] {f : PolynomialFamily K} (hf : f ∈ VP K) : f.IsPFamily

theorem Cslib.Circuits.Arithmetic.VP.of_isPProjection {K : Type u} [CommSemiring K] {f g : PolynomialFamily K} (hg : g ∈ VP K) (hfg : f.IsPProjection g) (hvars : PolynomiallyBounded f.vars) : f ∈ VP K

VP is closed under p-projections Bürgisser, Chapter 2. A projection cannot raise the degree, but f may have arbitrarily many variables that it does not use, so the number of variables of f is required to be polynomially bounded.

theorem Cslib.Circuits.Arithmetic.VP.of_synthesis {K : Type u} [CommSemiring K] {f : PolynomialFamily K} (hf : f.IsPFamily) {cost : ℕ → ℕ} (hcost : PolynomiallyBounded cost) (F : (n : ℕ) → (Fin (f.vars n) → MvPolynomial (Fin (f.vars n)) K) → MvPolynomial (Fin (f.vars n)) K) (hF : ∀ (n : ℕ), F n MvPolynomial.X = f.poly n) (h : ∀ (n : ℕ), Synthesis (arithInterpretationWith K ⇑MvPolynomial.C) (inputs (f.vars n)) {F n} (cost n)) : f ∈ VP K

A p-family is in VP when, within a polynomially bounded budget, each member f.poly n is F n X for a function F n synthesized from the inputs.

Degree is part of the definition

noncomputable def Cslib.Circuits.Arithmetic.powTwoPowFamily (K : Type u) [CommSemiring K] : PolynomialFamily K

The family X ^ 2 ^ n of powers of one variable.

theorem Cslib.Circuits.Arithmetic.exists_circuit_pow_two_pow {K : Type u} [CommSemiring K] (n : ℕ) : ∃ (c : Circuit (arithSignature K) 1 1), c.polynomial 0 = (powTwoPowFamily K).poly n ∧ c.size ≤ n

Repeated squaring computes X ^ 2 ^ n with at most n gates.

theorem Cslib.Circuits.Arithmetic.powTwoPowFamily_not_mem_VP {K : Type u} [CommSemiring K] [Nontrivial K] : powTwoPowFamily K ∉ VP K

VP bounds the degree. Over a nontrivial K, the family X ^ 2 ^ n has circuits with n gates (exists_circuit_pow_two_pow) but is not in VP: its degree 2 ^ n is not polynomially bounded.