Synthesis over the full binary basis

Over the full binary basis fullInterpretation (k := 2) every constant and every operation with at most two arguments is one gate. This module records the synthesis rules used to count gates of algebraic computations over a carrier U: an operation with one or two available arguments costs one gate (Synthesis.full_unary, Synthesis.full_binary_mem), a sum of N available functions over an additive commutative monoid costs N + 1 gates, one of them for the constant zero (Synthesis.full_sum), and a sum of N products of available functions over a semiring costs 2 * N + 1 gates (Synthesis.full_dot). A chain v 0 = c, v (i + 1) = op i (v i) (g i x) of length len, fed by available functions g i, costs len + 1 gates for all of its values (Synthesis.full_chain); chains compute prefix tests such as the first nonzero entry of a vector. Applied to a field, this counts field operations, with every operation that depends on at most two field elements, including tests and selections, charged one gate.

Main definitions

• Cslib.Circuits.Synthesis.chainValue: the values of a chain.

Main results

• Cslib.Circuits.Synthesis.full_unary: one gate for an operation on one available function.
• Cslib.Circuits.Synthesis.full_binary_mem: one gate for an operation on two available functions.
• Cslib.Circuits.Synthesis.full_sum: N + 1 gates for a sum of N available functions.
• Cslib.Circuits.Synthesis.full_dot: 2 * N + 1 gates for a sum of N products.
• Cslib.Circuits.Synthesis.full_chain: len + 1 gates for all values of a chain.

References

• [P. Bürgisser, M. Clausen, M. A. Shokrollahi, Algebraic Complexity Theory] [BCS97]

theorem Cslib.Circuits.Synthesis.full_unary {U : Type u_1} {n : ℕ} {s : Set ((Fin n → U) → U)} {f : (Fin n → U) → U} (op : U → U) (hf : f ∈ s) : Synthesis fullInterpretation s {fun (x : Fin n → U) => op (f x)} 1

An operation applied to one available function costs one gate of the full binary basis.

theorem Cslib.Circuits.Synthesis.full_binary_mem {U : Type u_1} {n : ℕ} {s : Set ((Fin n → U) → U)} {f g : (Fin n → U) → U} (op : U → U → U) (hf : f ∈ s) (hg : g ∈ s) : Synthesis fullInterpretation s {fun (x : Fin n → U) => op (f x) (g x)} 1

An operation applied to two available functions costs one gate of the full binary basis.

theorem Cslib.Circuits.Synthesis.full_sum {U : Type u_1} {n : ℕ} {s : Set ((Fin n → U) → U)} [AddCommMonoid U] {ι : Type u_2} (S : Finset ι) (f : ι → (Fin n → U) → U) (hf : ∀ i ∈ S, f i ∈ s) : Synthesis fullInterpretation s {fun (x : Fin n → U) => ∑ i ∈ S, f i x} (S.card + 1)

A sum of available functions, indexed by a finset S, costs #S + 1 gates of the full binary basis: one addition for each summand and a constant zero to start from.

theorem Cslib.Circuits.Synthesis.full_dot {U : Type u_1} {n : ℕ} {s : Set ((Fin n → U) → U)} [NonUnitalNonAssocSemiring U] {ι : Type u_2} (S : Finset ι) (f g : ι → (Fin n → U) → U) (hf : ∀ i ∈ S, f i ∈ s) (hg : ∀ i ∈ S, g i ∈ s) : Synthesis fullInterpretation s {fun (x : Fin n → U) => ∑ i ∈ S, f i x * g i x} (2 * S.card + 1)

A sum of products of available functions, indexed by a finset S, costs 2 * #S + 1 gates of the full binary basis.

def Cslib.Circuits.Synthesis.chainValue {U : Type u_1} {n : ℕ} (c : U) (op : ℕ → U → U → U) (g : ℕ → (Fin n → U) → U) : ℕ → (Fin n → U) → U

The values of a chain: v 0 = c and v (i + 1) = op i (v i) (g i x).

theorem Cslib.Circuits.Synthesis.full_chain {U : Type u_1} {n : ℕ} {s : Set ((Fin n → U) → U)} (c : U) (op : ℕ → U → U → U) (g : ℕ → (Fin n → U) → U) (len : ℕ) (hg : ∀ i < len, g i ∈ s) : Synthesis fullInterpretation s (Set.range fun (i : Fin (len + 1)) => chainValue c op g ↑i) (len + 1)

All values v 0, …, v len of a chain of length len fed by available functions cost len + 1 gates of the full binary basis: a constant and one binary gate per link.