Matrix multiplication algorithms

DefinitionRectangular matrix accumulation#✓fully proved

Let \(\alpha\) be a type with an addition and a multiplication, and let \(A\), \(B\), \(C\) be \(p \times q\), \(q \times r\) and \(p \times r\) matrices over \(\alpha\), stored as vectors of rows. Rectangular matrix accumulation adds the product \(AB\) to the accumulator \(C\): for \(i < p\), then \(j < r\), then \(k < q\), each in increasing order, it replaces \(C_{ij}\) by \(C_{ij} + A_{ik} B_{kj}\). It returns the final matrix together with a cost pair (scalar multiplications, scalar additions), charging one of each for every such update.

public def rectangularMatrixAccumulate {α : Type u} [Add α] [Mul α]
    {p q r : Nat} (A : _root_.Vector (_root_.Vector α q) p)
    (B : _root_.Vector (_root_.Vector α r) q) (C : _root_.Vector (_root_.Vector α r) p) :
    TimeM (Nat × Nat) (_root_.Vector (_root_.Vector α r) p) :=
  scanRows A B p 0 (by omega) (pure C)

Used by 9

Used bySquare matrix accumulation · Operation count of square matrix accumulation · Entries of rectangular matrix accumulation · Rectangular matrix accumulation computes \(C + AB\) · Operation count of rectangular matrix accumulation · Rectangular matrix accumulation with zero inner dimension · Freivalds trial · Acceptance criterion of the Freivalds trial · Cost of the Freivalds trial

DefinitionSquare matrix accumulation#✓fully proved

Let \(\alpha\) be a type with an addition and a multiplication, and let \(A\), \(B\), \(C\) be \(n \times n\) matrices over \(\alpha\), stored as vectors of rows. Square matrix accumulation on \(A\), \(B\), \(C\) is rectangular matrix accumulation on \(A\), \(B\), \(C\) with all three dimensions equal to \(n\): it adds \(AB\) to the accumulator \(C\) and returns the result with its cost pair (scalar multiplications, scalar additions).

public def matrixAccumulate {α : Type u} [Add α] [Mul α] {n : Nat}
    (A B C : _root_.Vector (_root_.Vector α n) n) :
    TimeM (Nat × Nat) (_root_.Vector (_root_.Vector α n) n) :=
  rectangularMatrixAccumulate A B C

Uses 1 · Used by 11

Statement usesRectangular matrix accumulation

Used bySquare matrix accumulation computes \(C + AB\) · Operation count of square matrix accumulation · FASTER-APSP · FASTER-APSP returns a power of the input matrix · Operation counts of FASTER-APSP · One min-plus multiplication extends shortest paths by one edge · Entries of the min-plus matrix accumulator · Min-plus matrix powers give shortest path weights with at most \(r\) edges · Slow all-pairs shortest paths (SLOW-APSP) · SLOW-APSP returns a min-plus matrix power · Exact operation counts of SLOW-APSP

TheoremEntries of rectangular matrix accumulation#✓fully proved

Let \(\alpha\) be a commutative additive monoid with a multiplication, and let \(A\), \(B\), \(C\) be \(p \times q\), \(q \times r\) and \(p \times r\) matrices over \(\alpha\), stored as vectors of rows. For all \(i < p\) and \(j < r\), the \((i, j)\) entry of the matrix returned by rectangular matrix accumulation on \(A\), \(B\), \(C\) is \(C_{ij} + \sum_{k < q} A_{ik} B_{kj}\).

theorem rectangularMatrixAccumulate_apply {α : Type u} [AddCommMonoid α] [Mul α]
    {p q r : Nat} (A : _root_.Vector (_root_.Vector α q) p)
    (B : _root_.Vector (_root_.Vector α r) q) (C : _root_.Vector (_root_.Vector α r) p)
    (i : Fin p) (j : Fin r) :
    ((rectangularMatrixAccumulate A B C).ret.get i).get j =
      (C.get i).get j + ∑ k : Fin q, (A.get i).get k * (B.get k).get j

Uses 1 · Used by 2

Statement usesRectangular matrix accumulation

Used byRectangular matrix accumulation computes \(C + AB\) · Acceptance criterion of the Freivalds trial

TheoremRectangular matrix accumulation computes \(C + AB\)#✓fully proved

Let \(\alpha\) be a commutative additive monoid with a multiplication, and let \(A\), \(B\), \(C\) be \(p \times q\), \(q \times r\) and \(p \times r\) matrices over \(\alpha\), stored as vectors of rows. The matrix returned by rectangular matrix accumulation on \(A\), \(B\), \(C\) equals \(C + AB\), where \(AB\) is the matrix product, \((AB)_{ij} = \sum_{k < q} A_{ik} B_{kj}\).

theorem rectangularMatrixAccumulate_ret {α : Type u} [AddCommMonoid α] [Mul α]
    {p q r : Nat} (A : _root_.Vector (_root_.Vector α q) p)
    (B : _root_.Vector (_root_.Vector α r) q) (C : _root_.Vector (_root_.Vector α r) p) :
    Matrix.of (fun i j => ((rectangularMatrixAccumulate A B C).ret.get i).get j) =
      Matrix.of (fun i j => (C.get i).get j) +
        Matrix.of (fun i k => (A.get i).get k) * Matrix.of (fun k j => (B.get k).get j)

Uses 2 · Used by 1

Statement usesRectangular matrix accumulation

Proof usesEntries of rectangular matrix accumulation

Used bySquare matrix accumulation computes \(C + AB\)

TheoremOperation count of rectangular matrix accumulation#✓fully proved

Let \(\alpha\) be a type with an addition and a multiplication, and let \(A\), \(B\), \(C\) be \(p \times q\), \(q \times r\) and \(p \times r\) matrices over \(\alpha\). Rectangular matrix accumulation on \(A\), \(B\), \(C\) has cost \((pqr, pqr)\): it charges exactly \(pqr\) scalar multiplications and exactly \(pqr\) scalar additions.

theorem rectangularMatrixAccumulate_time {α : Type u} [Add α] [Mul α]
    {p q r : Nat} (A : _root_.Vector (_root_.Vector α q) p)
    (B : _root_.Vector (_root_.Vector α r) q) (C : _root_.Vector (_root_.Vector α r) p) :
    (rectangularMatrixAccumulate A B C).time = (p * q * r, p * q * r)

Uses 1 · Used by 2

Statement usesRectangular matrix accumulation

Used byOperation count of square matrix accumulation · Cost of the Freivalds trial

TheoremRectangular matrix accumulation with zero inner dimension#✓fully proved

Let \(\alpha\) be a type with an addition and a multiplication. If \(A\) is a \(p \times 0\) matrix, \(B\) a \(0 \times r\) matrix and \(C\) a \(p \times r\) matrix over \(\alpha\), then rectangular matrix accumulation on \(A\), \(B\), \(C\) returns \(C\) unchanged at cost \((0, 0)\).

theorem rectangularMatrixAccumulate_zero_inner {α : Type u} [Add α] [Mul α]
    {p r : Nat} (A : _root_.Vector (_root_.Vector α 0) p)
    (B : _root_.Vector (_root_.Vector α r) 0) (C : _root_.Vector (_root_.Vector α r) p) :
    rectangularMatrixAccumulate A B C = (pure C : TimeM (Nat × Nat) _)

Uses 1

Statement usesRectangular matrix accumulation

TheoremSquare matrix accumulation computes \(C + AB\)#✓fully proved

Let \(\alpha\) be a commutative additive monoid with a multiplication, and let \(A\), \(B\), \(C\) be \(n \times n\) matrices over \(\alpha\), stored as vectors of rows. The matrix returned by square matrix accumulation on \(A\), \(B\), \(C\) equals \(C + AB\), where \(AB\) is the matrix product, \((AB)_{ij} = \sum_{k < n} A_{ik} B_{kj}\).

theorem matrixAccumulate_ret {α : Type u} [AddCommMonoid α] [Mul α] {n : Nat}
    (A B C : _root_.Vector (_root_.Vector α n) n) :
    Matrix.of (fun i j => ((matrixAccumulate A B C).ret.get i).get j) =
      Matrix.of (fun i j => (C.get i).get j) +
        Matrix.of (fun i k => (A.get i).get k) * Matrix.of (fun k j => (B.get k).get j)

Uses 2 · Used by 4

Statement usesSquare matrix accumulation

Proof usesRectangular matrix accumulation computes \(C + AB\)

Used byFASTER-APSP returns a power of the input matrix · Entries of the min-plus matrix accumulator · Min-plus matrix powers give shortest path weights with at most \(r\) edges · SLOW-APSP returns a min-plus matrix power

TheoremOperation count of square matrix accumulation#✓fully proved

Let \(\alpha\) be a type with an addition and a multiplication, and let \(A\), \(B\), \(C\) be \(n \times n\) matrices over \(\alpha\). Square matrix accumulation on \(A\), \(B\), \(C\) has cost \((n^3, n^3)\): it charges exactly \(n^3\) scalar multiplications and exactly \(n^3\) scalar additions.

theorem matrixAccumulate_time {α : Type u} [Add α] [Mul α] {n : Nat}
    (A B C : _root_.Vector (_root_.Vector α n) n) :
    (matrixAccumulate A B C).time = (n ^ 3, n ^ 3)

Uses 3 · Used by 2

Statement usesSquare matrix accumulation

Proof usesRectangular matrix accumulation · Operation count of rectangular matrix accumulation

Used byOperation counts of FASTER-APSP · Exact operation counts of SLOW-APSP

DefinitionRecursive matrix multiply-accumulate#✓fully proved

Let \(\alpha\) be a type with an addition and a multiplication, let \(k\) be a natural number and \(n = 2^k\), and let \(A\), \(B\), \(C\) be \(n \times n\) matrices over \(\alpha\), stored as vectors of rows. The procedure adds the product of \(A\) and \(B\) to the accumulator \(C\) by the eight-call recursion of CLRS. When \(n = 1\), writing \(a\), \(b\), \(c\) for the single entries of \(A\), \(B\), \(C\), it replaces \(c\) by \(c + ab\). Otherwise it splits each matrix \(M\) into four \((n/2) \times (n/2)\) quadrants \(M_{11}\) (top left), \(M_{12}\) (top right), \(M_{21}\) (bottom left) and \(M_{22}\) (bottom right), and updates, in this order, \(C_{11} \gets C_{11} + A_{11} B_{11}\), \(C_{12} \gets C_{12} + A_{11} B_{12}\), \(C_{21} \gets C_{21} + A_{21} B_{11}\), \(C_{22} \gets C_{22} + A_{21} B_{12}\), then \(C_{11} \gets C_{11} + A_{12} B_{21}\), \(C_{12} \gets C_{12} + A_{12} B_{22}\), \(C_{21} \gets C_{21} + A_{22} B_{21}\), \(C_{22} \gets C_{22} + A_{22} B_{22}\), each by a recursive call on the accumulator left by the previous one. It returns the final accumulator together with two counters: the number of scalar multiplications and the number of accumulator additions.

Only these two operations are charged; calls, indexing and allocation are free.

public def recursiveMatrixAccumulate {α : Type u} [Add α] [Mul α] (k : Nat)
    (A B C : _root_.Vector (_root_.Vector α (2 ^ k)) (2 ^ k)) :
    TimeM (Nat × Nat) (_root_.Vector (_root_.Vector α (2 ^ k)) (2 ^ k)) :=
  accumulateBlock A B k 0 0 0 (by simp) (by simp) (by simp) C

Used by 3

Used byEntries of the recursive matrix multiply-accumulate · Correctness of the recursive matrix multiply-accumulate · Operation count of the recursive matrix multiply-accumulate

TheoremEntries of the recursive matrix multiply-accumulate#✓fully proved

Let \(\alpha\) be an additive commutative monoid with a multiplication, let \(k\) be a natural number and \(n = 2^k\), and let \(A = (a_{ij})\), \(B = (b_{ij})\), \(C = (c_{ij})\) be \(n \times n\) matrices over \(\alpha\), with indices running from \(0\) to \(n - 1\). For all indices \(i, j < n\), entry \((i, j)\) of the matrix returned by the recursive multiply-accumulate procedure on \(A\), \(B\), \(C\) equals \(c_{ij} + \sum_{t < n} a_{it} b_{tj}\).

theorem recursiveMatrixAccumulate_apply {α : Type u} [AddCommMonoid α] [Mul α] (k : Nat)
    (A B C : _root_.Vector (_root_.Vector α (2 ^ k)) (2 ^ k)) (i j : Fin (2 ^ k)) :
    ((recursiveMatrixAccumulate k A B C).ret.get i).get j =
      (C.get i).get j + ∑ t : Fin (2 ^ k), (A.get i).get t * (B.get t).get j

Uses 1 · Used by 1

Statement usesRecursive matrix multiply-accumulate

Used byCorrectness of the recursive matrix multiply-accumulate

TheoremCorrectness of the recursive matrix multiply-accumulate#✓fully proved

Let \(\alpha\) be an additive commutative monoid with a multiplication, let \(k\) be a natural number and \(n = 2^k\), and let \(A = (a_{ij})\), \(B = (b_{ij})\), \(C\) be \(n \times n\) matrices over \(\alpha\), with indices running from \(0\) to \(n - 1\). Viewed as a matrix, the result returned by the recursive multiply-accumulate procedure on \(A\), \(B\), \(C\) equals \(C + AB\), where \(AB\) is the matrix product with entries \((AB)_{ij} = \sum_{t < n} a_{it} b_{tj}\).

theorem recursiveMatrixAccumulate_ret {α : Type u} [AddCommMonoid α] [Mul α] (k : Nat)
    (A B C : _root_.Vector (_root_.Vector α (2 ^ k)) (2 ^ k)) :
    _root_.Matrix.of (fun i j => ((recursiveMatrixAccumulate k A B C).ret.get i).get j) =
      _root_.Matrix.of (fun i j => (C.get i).get j) +
        _root_.Matrix.of (fun i j => (A.get i).get j) *
          _root_.Matrix.of (fun i j => (B.get i).get j)

Uses 2

Statement usesRecursive matrix multiply-accumulate

Proof usesEntries of the recursive matrix multiply-accumulate

TheoremOperation count of the recursive matrix multiply-accumulate#✓fully proved

Let \(\alpha\) be a type with an addition and a multiplication, let \(k\) be a natural number and \(n = 2^k\), and let \(A\), \(B\), \(C\) be \(n \times n\) matrices over \(\alpha\). The recursive multiply-accumulate procedure on \(A\), \(B\), \(C\) performs exactly \(8^k\) scalar multiplications and exactly \(8^k\) accumulator additions. Since \(8^k = n^3\), each count is the cube of the dimension.

Calls, indexing and allocation are uncharged.

theorem recursiveMatrixAccumulate_time {α : Type u} [Add α] [Mul α] (k : Nat)
    (A B C : _root_.Vector (_root_.Vector α (2 ^ k)) (2 ^ k)) :
    (recursiveMatrixAccumulate k A B C).time = (8 ^ k, 8 ^ k)

Uses 1

Statement usesRecursive matrix multiply-accumulate

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.