Documentation

Complexity.Computability.Circuit.Arithmetic.VNP

Valiant's class VNP and VNP-completeness #

Valiant's algebraic analogue of NP [Val79a], in the form of Bürgisser, Chapter 2. A family f is in VNP K when it is p-definable: there are a polynomially bounded m and a family g in VP K such that

f n (X) = ∑ e ∈ {0, 1} ^ m n, g n (X, e),

the m n variables of g n after the first f.vars n being replaced by 0 or 1 (Cslib.Circuits.Arithmetic.booleanSum). The number of variables and the degree of g, and hence of f, are polynomially bounded, and g has polynomial-size circuits; as for VP, nothing relates different n, so VNP is nonuniform. The definition makes sense over every commutative semiring K.

A family is VNP-complete when it lies in VNP K and every family in VNP K is a p-projection of it. A VNP-complete family is in VP exactly when VNP ⊆ VP. Valiant's theorem that the permanent is VNP-complete over fields of characteristic other than two is not proved here.

Main definitions #

Main results #

References #

source
def Cslib.Circuits.Arithmetic.booleanAssignment {K : Type u} [CommSemiring K] {n m : ℕ} (e : Fin m → Bool) :
Fin (n + m) → Fin n ⊕ K

Keep the first n variables and substitute the Boolean value e i, as 0 or 1, for variable n + i.

Instances For
    source
    noncomputable def Cslib.Circuits.Arithmetic.booleanSum {K : Type u} [CommSemiring K] {n : ℕ} (m : ℕ) (P : MvPolynomial (Fin (n + m)) K) :
    MvPolynomial (Fin n) K

    The Boolean sum ∑ e ∈ {0, 1} ^ m, P (X, e): the sum, over all Boolean values for the last m variables, of the polynomial in the first n variables obtained by substituting them.

    Instances For
      source
      @[simp]
      theorem Cslib.Circuits.Arithmetic.booleanSum_zero {K : Type u} [CommSemiring K] {n : ℕ} (P : MvPolynomial (Fin (n + 0)) K) :
      booleanSum 0 P = P

      A Boolean sum over no variables is the polynomial itself.

      source
      def Cslib.Circuits.Arithmetic.liftProjection {K : Type u} {n m k : ℕ} (ρ : Fin k → Fin n ⊕ K) :
      Fin (k + m) → Fin (n + m) ⊕ K

      Lift a projection of the first k of k + m variables to all of them, keeping the last m variables.

      Instances For
        source
        theorem Cslib.Circuits.Arithmetic.projection_booleanSum {K : Type u} [CommSemiring K] {n m k : ℕ} (ρ : Fin k → Fin n ⊕ K) (P : MvPolynomial (Fin (k + m)) K) :
        (projection ρ) (booleanSum m P) = booleanSum m ((projection (liftProjection ρ)) P)

        A projection of a Boolean sum is the Boolean sum of a projection: substitution for the first variables commutes with summing over the last.

        source
        theorem Cslib.Circuits.Arithmetic.totalDegree_booleanSum_le {K : Type u} [CommSemiring K] {n m : ℕ} (P : MvPolynomial (Fin (n + m)) K) :
        (booleanSum m P).totalDegree ≤ P.totalDegree

        A Boolean sum has no larger degree than the summed polynomial.

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

        Valiant's class VNP over K Valiant1979Algebra; Bürgisser, Chapter 2: the families f with f n = booleanSum (m n) (g n) for a family g in VP K whose members have f.vars n + m n variables. The class is nonuniform, like VP.

        Instances For
          source
          theorem Cslib.Circuits.Arithmetic.VP_subset_VNP {K : Type u} [CommSemiring K] :
          VP K ⊆ VNP K

          Every family in VP is in VNP, summing over no variables.

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

          The members of VNP are p-families.

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

          VNP is closed under p-projections Bürgisser, Chapter 2. As for VP, the number of variables is required to be polynomially bounded.

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

          A family is VNP-complete over K Valiant1979Algebra; Bürgisser, Chapter 2 when it is in VNP K and every family in VNP K is a p-projection of it.

          Instances For
            source
            theorem Cslib.Circuits.Arithmetic.IsVNPComplete.VNP_subset_VP {K : Type u} [CommSemiring K] {f : PolynomialFamily K} (hf : IsVNPComplete f) (hVP : f ∈ VP K) :
            VNP K ⊆ VP K

            If a VNP-complete family is in VP, then VNP ⊆ VP.

            source
            theorem Cslib.Circuits.Arithmetic.IsVNPComplete.mem_VP_iff {K : Type u} [CommSemiring K] {f : PolynomialFamily K} (hf : IsVNPComplete f) :
            f ∈ VP K ↔ VNP K ⊆ VP K

            A VNP-complete family is in VP exactly when VNP ⊆ VP: Valiant's hypothesis VP ≠ VNP says that no VNP-complete family has polynomial-size circuits.