Linearizing polynomial circuits

Affine circuits compute affine maps (Cslib.Circuits.Program.exists_affine_trace): in a circuit over the affine basis, the value of every wire is an affine function of the input.

Linearization (Cslib.Circuits.Circuit.Computes.exists_affine). Over an infinite field, a circuit with polynomial operations that computes a linear map x ↦ M x can be replaced by a circuit over the affine basis, with the same wires, that computes the same map: nonlinear operations do not help to compute linear maps, as in Strassen's theorem on linear complexity [BurgisserClausenShokrollahi1997, Chapter 13]. Each gate is replaced by its first-order Taylor expansion at the point that its arguments take on the zero input (Cslib.Circuits.taylorOp, Cslib.Circuits.Program.linearize).

To see why this works, evaluate the circuit over the dual numbers F[ε], where ε² = 0, at the input ε x. Because the operations are polynomials, a gate whose arguments are z + ε v takes the value P(z) + ε ∑_a ∂_a P(z) v_a (MvPolynomial.snd_aeval_dualNumber), where z is the value of the arguments on the zero input. So where the circuit takes the value a + ε b at ε x, the linearized circuit takes the value a + b at x (Cslib.Circuits.Program.trace_linearize). Over an infinite field a polynomial is determined by its values, so the polynomial computed at an output is the linear form ∑_j M_{ij} X_j, whose value at ε x is ε (M x)_i.

Main definitions

• Cslib.Circuits.polynomialInterpretation: the operations given by polynomials, over any algebra.
• Cslib.Circuits.taylorOp: the affine operation of the first-order Taylor expansion.
• Cslib.Circuits.Program.linearize: the linearization of a program with polynomial operations.

Main results

• Cslib.Circuits.Program.exists_affine_trace: affine circuits compute affine maps.
• Cslib.Circuits.Program.trace_linearize: the linearized program reads off the dual numbers.
• Cslib.Circuits.Circuit.Computes.exists_affine: linearization of circuits for linear maps.

References

• P. Bürgisser, M. Clausen, M. A. Shokrollahi, Algebraic Complexity Theory, Chapter 13

theorem Cslib.Circuits.Program.exists_affine_trace {F : Type u_1} {n s : ℕ} [CommRing F] (p : Program (affineSignature F) n s) (w : Wire n s) : ∃ (L : (Fin n → F) →ₗ[F] F) (b : F), ∀ (x : Fin n → F), p.trace (affineInterpretation F) x w = L x + b

Affine circuits compute affine maps. In a program over the affine basis, the value of every wire is a linear map of the input plus a constant.

Polynomial interpretations over algebras

def Cslib.Circuits.polynomialInterpretation {F : Type u_1} {σ : Signature} [CommRing F] (P : (o : σ.Op) → MvPolynomial (Fin (σ.Arity o)) F) (R : Type u_2) [CommRing R] [Algebra F R] : Interpretation σ R

The interpretation over an F-algebra R in which each operation o substitutes its arguments into the polynomial P o. Every polynomial interpretation over F is of this form (Cslib.Circuits.Interpretation.IsPolynomial).

theorem Cslib.Circuits.polynomialInterpretation_apply {F : Type u_1} {σ : Signature} [CommRing F] (P : (o : σ.Op) → MvPolynomial (Fin (σ.Arity o)) F) (R : Type u_2) [CommRing R] [Algebra F R] (o : σ.Op) (x : Fin (σ.Arity o) → R) : polynomialInterpretation P R o x = (MvPolynomial.aeval x) (P o)

An operation of a polynomial interpretation substitutes its arguments into its polynomial.

theorem Cslib.Circuits.Program.map_trace_polynomialInterpretation {F : Type u_1} {n s : ℕ} {σ : Signature} [CommRing F] (P : (o : σ.Op) → MvPolynomial (Fin (σ.Arity o)) F) {R : Type u_2} {S : Type u_3} [CommRing R] [Algebra F R] [CommRing S] [Algebra F S] (φ : R →ₐ[F] S) (p : Program σ n s) (x : Fin n → R) (w : Wire n s) : φ (p.trace (polynomialInterpretation P R) x w) = p.trace (polynomialInterpretation P S) (fun (j : Fin n) => φ (x j)) w

Evaluation of a program with polynomial operations commutes with algebra homomorphisms.

Linearization

noncomputable def Cslib.Circuits.taylorOp {F : Type u_1} [CommRing F] {k : ℕ} (P : MvPolynomial (Fin k) F) (z : Fin k → F) : (affineSignature F).Op

The affine operation computing the first-order Taylor expansion of P at z, y ↦ P(z) + ∑_a ∂_a P(z) (y_a - z_a).

theorem Cslib.Circuits.affineInterpretation_taylorOp {F : Type u_1} [CommRing F] {k : ℕ} (P : MvPolynomial (Fin k) F) (z y : Fin k → F) : affineInterpretation F (taylorOp P z) y = (MvPolynomial.eval z) P + ∑ a : Fin k, (MvPolynomial.eval z) ((MvPolynomial.pderiv a) P) * (y a - z a)

The value of the first-order Taylor expansion of P at z.

noncomputable def Cslib.Circuits.Program.linearize {F : Type u_1} {n : ℕ} [CommRing F] {σ : Signature} (P : (o : σ.Op) → MvPolynomial (Fin (σ.Arity o)) F) {s : ℕ} : Program σ n s → Program (affineSignature F) n s

The linearization of a program whose operations are the polynomials P: the program over the affine basis with the same wires, in which each gate is replaced by its first-order Taylor expansion at the point that its arguments take on the zero input.

theorem Cslib.Circuits.Program.arity_lines_linearize {F : Type u_1} {n s : ℕ} [CommRing F] {σ : Signature} (P : (o : σ.Op) → MvPolynomial (Fin (σ.Arity o)) F) (p : Program σ n s) (g : Fin s) : (affineSignature F).Arity ((linearize P p).lines g).op = σ.Arity (p.lines g).op

Linearization preserves the arity of every gate.

theorem Cslib.Circuits.Program.innerGates_linearize {F : Type u_1} {n s : ℕ} [CommRing F] {σ : Signature} (P : (o : σ.Op) → MvPolynomial (Fin (σ.Arity o)) F) (p : Program σ n s) : (linearize P p).innerGates = p.innerGates

Linearization preserves the inner gates.

theorem Cslib.Circuits.Program.fanInAtMost_linearize {F : Type u_1} {n s : ℕ} [CommRing F] {σ : Signature} (P : (o : σ.Op) → MvPolynomial (Fin (σ.Arity o)) F) (p : Program σ n s) (r : ℕ) : (linearize P p).FanInAtMost r ↔ p.FanInAtMost r

Linearization preserves fan-in.

theorem Cslib.Circuits.Program.fst_trace_dualNumber {F : Type u_1} {n s : ℕ} [CommRing F] {σ : Signature} (P : (o : σ.Op) → MvPolynomial (Fin (σ.Arity o)) F) (p : Program σ n s) (x : Fin n → F) (w : Wire n s) : TrivSqZeroExt.fst (p.trace (polynomialInterpretation P (DualNumber F)) (fun (j : Fin n) => TrivSqZeroExt.inr (x j)) w) = p.trace (polynomialInterpretation P F) 0 w

The real part of the value of a wire at the input ε x is its value at the zero input.

theorem Cslib.Circuits.Program.trace_linearize {F : Type u_1} {n s : ℕ} [CommRing F] {σ : Signature} (P : (o : σ.Op) → MvPolynomial (Fin (σ.Arity o)) F) (p : Program σ n s) (x : Fin n → F) (w : Wire n s) : (linearize P p).trace (affineInterpretation F) x w = TrivSqZeroExt.fst (p.trace (polynomialInterpretation P (DualNumber F)) (fun (j : Fin n) => TrivSqZeroExt.inr (x j)) w) + TrivSqZeroExt.snd (p.trace (polynomialInterpretation P (DualNumber F)) (fun (j : Fin n) => TrivSqZeroExt.inr (x j)) w)

The linearized program. Where the original program takes the value a + ε b at the input ε x, the linearized program takes the value a + b at the input x.

theorem Cslib.Circuits.Circuit.trace_outputs_dualNumber {F : Type u_1} {n m : ℕ} [CommRing F] {σ : Signature} (P : (o : σ.Op) → MvPolynomial (Fin (σ.Arity o)) F) [IsDomain F] [Infinite F] {c : Circuit σ n m} {M : Matrix (Fin m) (Fin n) F} (hc : c.Computes (polynomialInterpretation P F) fun (x : Fin n → F) => M.mulVec x) (x : Fin n → F) (i : Fin m) : c.program.trace (polynomialInterpretation P (DualNumber F)) (fun (j : Fin n) => TrivSqZeroExt.inr (x j)) (c.outputs i) = TrivSqZeroExt.inr (M.mulVec x i)

Over an infinite field, a circuit with polynomial operations that computes x ↦ M x takes the value ε (M x)_i at its output i on the input ε x.

theorem Cslib.Circuits.Circuit.Computes.exists_affine {F : Type u_1} {n m : ℕ} [Field F] [Infinite F] {σ : Signature} {I : Interpretation σ F} (hI : I.IsPolynomial) {c : Circuit σ n m} {M : Matrix (Fin m) (Fin n) F} (hc : c.Computes I fun (x : Fin n → F) => M.mulVec x) : ∃ (c' : Circuit (affineSignature F) n m), c'.size = c.size ∧ c'.innerSize = c.innerSize ∧ (∀ (r : ℕ), c'.FanInAtMost r ↔ c.FanInAtMost r) ∧ c'.Computes (affineInterpretation F) fun (x : Fin n → F) => M.mulVec x

Linearization. Over an infinite field, a circuit with polynomial operations computing a linear map x ↦ M x is matched by a circuit over the affine basis computing the same map, with the same number of gates, the same inner gates, and the same fan-in.