Arithmetic circuits

11 fully proved

Algebraic

InductiveArithmetic operand#✓fully proved

An arithmetic operand over \(F\) with inputs indexed by \(A\) and \(n\) nodes is a constant \(x \in F\), an input \(a \in A\), or a reference to a node \(i < n\).

public inductive ArithmeticOperand (F : Type u) (A : Type v) (n : ℕ)
  | constant : F → ArithmeticOperand F A n
  | input : A → ArithmeticOperand F A n
  | node : Fin n → ArithmeticOperand F A n

Used by 12

Used byOuter-product matrix circuit · The outer-product matrix circuit computes the matrix product · Lower bound for matrix multiplication circuits · Outputs of a matrix multiplication circuit are gates · Arithmetic circuit · Arithmetic gate · Operand evaluation · Gate evaluation · Circuit evaluation · Extensionality for arithmetic circuits · Outer-product circuit · Correctness of the outer-product circuit

InductiveArithmetic gate#✓fully proved

An arithmetic gate over \(F\) with inputs indexed by \(A\) and \(n\) prior nodes is an addition, a subtraction or a multiplication of two arithmetic operands, each of which is a constant in \(F\), an input \(a \in A\) or a reference to a node \(i < n\).

public inductive ArithmeticGate (F : Type u) (A : Type v) (n : ℕ)
  | add : ArithmeticOperand F A n → ArithmeticOperand F A n → ArithmeticGate F A n
  | sub : ArithmeticOperand F A n → ArithmeticOperand F A n → ArithmeticGate F A n
  | mul : ArithmeticOperand F A n → ArithmeticOperand F A n → ArithmeticGate F A n

Uses 1 · Used by 8

Statement usesArithmetic operand

Used byOuter-product matrix circuit · The outer-product matrix circuit computes the matrix product · Arithmetic circuit · Gate evaluation · Value of a gate in a circuit · Extensionality for arithmetic circuits · Outer-product circuit · Correctness of the outer-product circuit

StructureArithmetic circuit#✓fully proved

An arithmetic circuit over \(F\) with inputs indexed by \(A\) and outputs indexed by \(B\) consists of a size \(s \in \mathbb{N}\), a gate \(g_i\) for each \(i < s\), and an output operand for each \(b \in B\). Each gate \(g_i\) is an addition, subtraction or multiplication of two operands, each a constant in \(F\), an input \(a \in A\) or an earlier gate \(g_j\) with \(j < i\); an output operand is a constant in \(F\), an input or any gate \(g_j\) with \(j < s\).

Constants and inputs are free; each gate counts as one scalar operation.

public structure ArithmeticCircuit (F : Type u) (A : Type v) (B : Type w) where
  size : ℕ
  gate (i : Fin size) : ArithmeticGate F A i.val
  output : B → ArithmeticOperand F A size

Uses 2 · Used by 17

Statement usesArithmetic gate · Arithmetic operand

Used byAdmissible rectangular circuit exponents · Exponent two is admissible at aspect zero · Matrix arithmetic circuit · Admissible circuit exponents are upward closed · Outer-product matrix circuit · The outer-product matrix circuit computes the matrix product · Size of the outer-product matrix circuit · Lower bound for matrix multiplication circuits · Outputs of a matrix multiplication circuit are gates · Upper bounds on the rectangular circuit exponent · Admissible rectangular circuit exponents are at least two · Circuit evaluation · Value of a gate in a circuit · Extensionality for arithmetic circuits · Outer-product circuit · Correctness of the outer-product circuit · Size of the outer-product circuit

DefinitionOperand evaluation#✓fully proved

Let \(F\) and \(A\) be types and \(n \in \mathbb{N}\). Given a value in \(F\) for each input \(a \in A\) and a value in \(F\) for each node \(i < n\), an arithmetic operand over \(F\) with inputs indexed by \(A\) and \(n\) nodes evaluates as follows: a constant \(x\) evaluates to \(x\), an input \(a\) to its assigned value, and a reference to node \(i\) to the value given for node \(i\).

def ArithmeticOperand.evaluate {F : Type u} {A : Type v} {n : ℕ}
    (input : A → F) (computed : Fin n → F) : ArithmeticOperand F A n → F
  | .constant x => x
  | .input a => input a
  | .node i => computed i

Uses 1 · Used by 5

Statement usesArithmetic operand

Used byThe outer-product matrix circuit computes the matrix product · Lower bound for matrix multiplication circuits · Gate evaluation · Circuit evaluation · Correctness of the outer-product circuit

DefinitionGate evaluation#✓fully proved

Let \(F\) be a type with addition, subtraction and multiplication, let \(A\) be a type and let \(n \in \mathbb{N}\). Given a value in \(F\) for each input \(a \in A\) and a value in \(F\) for each node \(i < n\), write \(v(x)\) for the value of an arithmetic operand \(x\): a constant evaluates to itself, an input \(a\) to its assigned value and a reference to node \(i\) to the value given for node \(i\). An arithmetic gate over \(F\) with inputs indexed by \(A\) and \(n\) prior nodes that adds, subtracts or multiplies the operands \(x\) and \(y\) evaluates to \(v(x) + v(y)\), \(v(x) - v(y)\) or \(v(x) \cdot v(y)\) respectively.

def ArithmeticGate.evaluate {F : Type u} {A : Type v} {n : ℕ}
    [Add F] [Sub F] [Mul F] (input : A → F) (computed : Fin n → F) :
    ArithmeticGate F A n → F
  | .add a b => a.evaluate input computed + b.evaluate input computed
  | .sub a b => a.evaluate input computed - b.evaluate input computed
  | .mul a b => a.evaluate input computed * b.evaluate input computed

Uses 3 · Used by 3

Statement usesArithmetic gate · Arithmetic operand · Operand evaluation

Used byThe outer-product matrix circuit computes the matrix product · Value of a gate in a circuit · Correctness of the outer-product circuit

Arithmetic Circuit

TheoremExtensionality for arithmetic circuits#✓fully proved

Two arithmetic circuits over \(F\) with inputs indexed by \(A\) and outputs indexed by \(B\) are equal if they have the same size, the same gate at each position and the same output operand for each \(b \in B\).

@[ext] theorem ext {F : Type u} {A : Type v} {B : Type w}
    {c d : ArithmeticCircuit F A B} (hs : c.size = d.size)
    (hg : HEq c.gate d.gate) (ho : HEq c.output d.output) : c = d

Uses 3

Statement usesArithmetic circuit · Arithmetic gate · Arithmetic operand

DefinitionValue of a gate in a circuit#✓fully proved

Let \(F\) be a type with addition, subtraction and multiplication and let \(c\) be an arithmetic circuit over \(F\) with inputs indexed by \(A\). Given a value in \(F\) for each input \(a \in A\), the value of gate \(g_i\) of \(c\) is the value of the operation of \(g_i\) on its two operands, where a constant \(x\) has value \(x\), an input has its assigned value and a reference to an earlier gate \(g_j\) with \(j < i\) takes the value of \(g_j\), defined recursively.

def evaluateNode {F : Type u} {A : Type v} {B : Type w} [Add F] [Sub F] [Mul F]
    (c : ArithmeticCircuit F A B) (input : A → F) (i : Fin c.size) : F :=
  (c.gate i).evaluate input (fun j =>
    evaluateNode c input ⟨j.val, Nat.lt_trans j.isLt i.isLt⟩)
termination_by i.val
decreasing_by exact j.isLt

Uses 3 · Used by 5

Statement usesArithmetic circuit · Arithmetic gate · Gate evaluation

Used byThe outer-product matrix circuit computes the matrix product · Lower bound for matrix multiplication circuits · Outputs of a matrix multiplication circuit are gates · Circuit evaluation · Correctness of the outer-product circuit

DefinitionCircuit evaluation#✓fully proved

Let \(F\) be a type with addition, subtraction and multiplication and let \(c\) be an arithmetic circuit over \(F\) with inputs indexed by \(A\) and outputs indexed by \(B\). Given a value in \(F\) for each input \(a \in A\), the value of \(c\) at an output \(b \in B\) is the value of the output operand of \(b\), where a constant \(x\) has value \(x\), an input has its assigned value and a reference to gate \(g_j\) has the value of \(g_j\), each gate being evaluated from the values of the gates before it.

def evaluate {F : Type u} {A : Type v} {B : Type w} [Add F] [Sub F] [Mul F]
    (c : ArithmeticCircuit F A B) (input : A → F) (b : B) : F :=
  (c.output b).evaluate input (c.evaluateNode input)

Uses 4 · Used by 5

Statement usesArithmetic circuit · Value of a gate in a circuit · Arithmetic operand · Operand evaluation

Used byCircuits that compute the matrix product · The outer-product matrix circuit computes the matrix product · Lower bound for matrix multiplication circuits · Outputs of a matrix multiplication circuit are gates · Correctness of the outer-product circuit

DefinitionOuter-product circuit#✓fully proved

For a type \(F\) of scalars and \(m, n \in \mathbb{N}\), the outer-product circuit has inputs \(a_0, \dots, a_{m-1}\) and \(b_0, \dots, b_{n-1}\), one output for each pair \((i, j)\) with \(i < m\) and \(j < n\), and exactly \(mn\) gates: the gate for \((i, j)\) multiplies \(a_i\) by \(b_j\), and the output at \((i, j)\) is that gate.

def outerProduct (F : Type u) (m n : ℕ) :
    ArithmeticCircuit F (Fin m ⊕ Fin n) (Fin m × Fin n) where
  size := m * n
  gate i := .mul (.input (.inl (finProdFinEquiv.symm i).1))
    (.input (.inr (finProdFinEquiv.symm i).2))
  output ij := .node (finProdFinEquiv ij)

Uses 3 · Used by 3

Statement usesArithmetic circuit · Arithmetic gate · Arithmetic operand

Used byOuter-product matrix circuit · Correctness of the outer-product circuit · Size of the outer-product circuit

TheoremCorrectness of the outer-product circuit#✓fully proved

Let \(F\) be a type with addition, subtraction and multiplication. For all \(m, n \in \mathbb{N}\), \(a \in F^m\), \(b \in F^n\), \(i < m\) and \(j < n\), the outer-product circuit over \(F\) evaluated on the inputs \(a\) and \(b\) has value \(a_i b_j\) at the output \((i, j)\).

theorem outerProduct_evaluate {F : Type u} [Add F] [Sub F] [Mul F] {m n : ℕ}
    (a : Fin m → F) (b : Fin n → F) (i : Fin m) (j : Fin n) :
    (outerProduct F m n).evaluate (Sum.elim a b) (i, j) = a i * b j

Uses 8

Statement usesCircuit evaluation · Outer-product circuit

Proof usesArithmetic circuit · Value of a gate in a circuit · Arithmetic gate · Gate evaluation · Arithmetic operand · Operand evaluation

TheoremSize of the outer-product circuit#✓fully proved

For every \(F\) and all \(m, n \in \mathbb{N}\), the outer-product circuit over \(F\) for \(m \times n\) outer products has exactly \(mn\) gates.

theorem outerProduct_size (F : Type u) (m n : ℕ) :
    (outerProduct F m n).size = m * n

Uses 2

Statement usesArithmetic circuit · Outer-product circuit

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.