Matrix multiplication: Model

inductive MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate (F : Type u_1) (Input : Type u_2) (Register : Type u_3) : Type (max (max u_1 u_2) u_3)

Arithmetic gates over a field with explicit input and register references.

• literal {F : Type u_1} {Input : Type u_2} {Register : Type u_3} : F → Gate F Input Register
• input {F : Type u_1} {Input : Type u_2} {Register : Type u_3} : Input → Gate F Input Register
• add {F : Type u_1} {Input : Type u_2} {Register : Type u_3} : Register → Register → Gate F Input Register
• sub {F : Type u_1} {Input : Type u_2} {Register : Type u_3} : Register → Register → Gate F Input Register
• mul {F : Type u_1} {Input : Type u_2} {Register : Type u_3} : Register → Register → Gate F Input Register

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.eval {F : Type u_1} {Input : Type u_2} {Register : Type u_3} [Field F] (inputs : Input → F) (registers : Register → F) : Gate F Input Register → F

Interpret a gate using the current input values and register contents.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.eval inputs registers (MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.literal z) = z
• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.eval inputs registers (MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.input i) = inputs i
• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.eval inputs registers (MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.add i j) = registers i + registers j
• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.eval inputs registers (MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.sub i j) = registers i - registers j
• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.eval inputs registers (MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.mul i j) = registers i * registers j

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.cost {F : Type u_1} {Input : Type u_2} {Register : Type u_3} : Gate F Input Register → ℕ

Charge one operation for arithmetic gates and none for input or literal loading.

Equations

• (MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.literal z).cost = 0
• (MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.input i).cost = 0
• (MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.add i j).cost = 1
• (MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.sub i j).cost = 1
• (MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.mul i j).cost = 1

inductive MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program (F : Type u_1) (Input : Type u_2) : ℕ → Type (max u_1 u_2)

A division-free straight-line program indexed by its number of allocated registers.

• nil {F : Type u_1} {Input : Type u_2} : Program F Input 0
• step {F : Type u_1} {Input : Type u_2} {r : ℕ} : Program F Input r → Gate F Input (Fin r) → Program F Input (r + 1)

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.eval {F : Type u_1} {Input : Type u_2} [Field F] {r : ℕ} : Program F Input r → (Input → F) → Fin r → F

Evaluate every register of a field-valued straight-line program.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.nil.eval x✝ = Fin.elim0
• (p.step g).eval x✝ = fun (i : Fin (n + 1)) => Fin.cases (MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Gate.eval x✝ (p.eval x✝) g) (p.eval x✝) i

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.cost {F : Type u_1} {Input : Type u_2} {r : ℕ} : Program F Input r → ℕ

Total number of arithmetic operations in a straight-line program.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.Program.nil.cost = 0
• (p.step g).cost = p.cost + g.cost

@[reducible, inline]

abbrev MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.MatrixInput (a b c : ℕ) : Type

Disjoint entry positions of the left and right rectangular matrix inputs.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.MatrixInput a b c = (Fin a × Fin b ⊕ Fin b × Fin c)

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.matrixInputs {F : Type u_1} {a b c : ℕ} (A : Matrix (Fin a) (Fin b) F) (B : Matrix (Fin b) (Fin c) F) : MatrixInput a b c → F

Assemble the two matrices into the program's disjoint input space.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.matrixInputs A B (Sum.inl (i, j)) = A i j
• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.matrixInputs A B (Sum.inr (j, k)) = B j k

structure MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm (F : Type u_1) (a b c : ℕ) : Type u_1

A straight-line program with designated registers for rectangular matrix-product entries.

• registers : ℕ

  Number of registers used by the matrix multiplication program.

• program : Program F (MatrixInput a b c) self.registers

  The straight-line program underlying the matrix algorithm.

• output : Fin a → Fin c → Fin self.registers

  Register location of each output matrix entry.

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.eval {F : Type u_1} [Field F] {a b c : ℕ} (P : MatrixAlgorithm F a b c) (A : Matrix (Fin a) (Fin b) F) (B : Matrix (Fin b) (Fin c) F) : Matrix (Fin a) (Fin c) F

Evaluate the algorithm's output matrix on its two input matrices.

Equations

• P.eval A B i k = P.program.eval (MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.matrixInputs A B) (P.output i k)

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.Correct {F : Type u_1} [Field F] {a b c : ℕ} (P : MatrixAlgorithm F a b c) : Prop

The program computes the matrix product for every pair of inputs.

Equations

• P.Correct = ∀ (A : Matrix (Fin a) (Fin b) F) (B : Matrix (Fin b) (Fin c) F), P.eval A B = A * B

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.MatrixAlgorithm.cost {F : Type u_1} {a b c : ℕ} (P : MatrixAlgorithm F a b c) : ℕ

Arithmetic operation count of the matrix multiplication program.

Equations

• P.cost = P.program.cost

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.AdmissibleExponent (F : Type u_1) [Field F] (τ : ℝ) : Prop

Positive slack, one uniform constant, and a correct program at every size.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.omega (F : Type u_1) [Field F] : ℝ

The infimum of admissible arithmetic matrix multiplication exponents over the given field.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.omega F = sInf {τ : ℝ | MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.AdmissibleExponent F τ}

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.innerSize (n : ℕ) (k : ℝ) : ℕ

The inner dimension of an n × n^k by n^k × n multiplication.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.innerSize n k = ⌈↑n ^ k⌉₊

def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RectangularAdmissibleExponent (F : Type u_1) [Field F] (k τ : ℝ) : Prop

Uniform arithmetic cost bounds for n by ceil(n^k) by n multiplication, with positive slack.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangularOmega (F : Type u_1) [Field F] (k : ℝ) : ℝ

The infimum of admissible arithmetic exponents at a fixed rectangular shape.

Equations

• MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.rectangularOmega F k = sInf {τ : ℝ | MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.RectangularAdmissibleExponent F k τ}

noncomputable def MatrixMultiplicationAllFields.MatrixMultiplication.Arithmetic.complexAlpha : ℝ

The dual exponent is a supremum of exact exponent-two rectangular shapes.

Equations

• One or more equations did not get rendered due to their size.