Matrix chain multiplication

InductiveParenthesization#✓fully proved

A parenthesization of \(n\) matrices is a full binary tree whose leaves are labeled by indices in \(\{0, \dots, n - 1\}\): either a single leaf naming matrix \(i\), or a product node with a left and a right parenthesization as factors. Labels may be repeated, omitted, or out of order.

public inductive Parenthesization (n : Nat) where
  /-- One matrix at its original bounded index. -/
  | matrix (index : Fin n)
  /-- Multiply two fully parenthesized subchains. -/
  | multiply (left right : Parenthesization n)
deriving DecidableEq, Repr

Used by 13

Used byColumn count of a parenthesization · Dimension-compatible parenthesization · Valid parenthesization · Matrix-chain ordering · Split candidates evaluated by matrix-chain ordering · Matrix-chain ordering reports the cost of its parenthesization · Reported matrix-chain cost is a lower bound · Matrix-chain ordering returns a valid parenthesization · Reconstruction size in matrix-chain ordering · Leaf indices of a parenthesization · Matrix-chain result · Row count of a parenthesization · Scalar multiplication count of a parenthesization

DefinitionLeaf indices of a parenthesization#✓fully proved

The leaf indices of a parenthesization of \(n\) matrices form the list of indices in \(\{0, \dots, n - 1\}\) obtained by reading its leaves from left to right: \([i]\) for a single leaf naming matrix \(i\), and the concatenation of the lists of the left and right factors for a product node.

@[expose] public def matrixIndices {n : Nat} : Parenthesization n → List (Fin n)
  | .matrix index => [index]
  | .multiply left right => matrixIndices left ++ matrixIndices right

Uses 1 · Used by 3

Statement usesParenthesization

Used byValid parenthesization · Reported matrix-chain cost is a lower bound · Matrix-chain ordering returns a valid parenthesization

DefinitionRow count of a parenthesization#✓fully proved

Let \(p = (p_0, \dots, p_n)\) be a vector of natural numbers, regarding matrix \(i\) (for \(0 \le i < n\)) as having \(p_i\) rows and \(p_{i+1}\) columns. The row count of a parenthesization of \(n\) matrices with respect to \(p\) is \(p_i\) for a single leaf naming matrix \(i\), and the row count of the left factor for a product node.

@[expose] public def rows {n : Nat}
    (dimensions : Vector Nat (n + 1)) : Parenthesization n → Nat
  | .matrix index => dimensions.get index.castSucc
  | .multiply left _ => rows dimensions left

Uses 1 · Used by 8

Statement usesParenthesization

Used byDimension-compatible parenthesization · Matrix-chain ordering · Split candidates evaluated by matrix-chain ordering · Matrix-chain ordering reports the cost of its parenthesization · Reported matrix-chain cost is a lower bound · Matrix-chain ordering returns a valid parenthesization · Reconstruction size in matrix-chain ordering · Scalar multiplication count of a parenthesization

DefinitionColumn count of a parenthesization#✓fully proved

Let \(p = (p_0, \dots, p_n)\) be a vector of natural numbers, regarding matrix \(i\) (for \(0 \le i < n\)) as having \(p_i\) rows and \(p_{i+1}\) columns. The column count of a parenthesization of \(n\) matrices with respect to \(p\) is \(p_{i+1}\) for a single leaf naming matrix \(i\), and the column count of the right factor for a product node.

@[expose] public def cols {n : Nat}
    (dimensions : Vector Nat (n + 1)) : Parenthesization n → Nat
  | .matrix index => dimensions.get index.succ
  | .multiply _ right => cols dimensions right

Uses 1 · Used by 8

Statement usesParenthesization

Used byDimension-compatible parenthesization · Matrix-chain ordering · Split candidates evaluated by matrix-chain ordering · Matrix-chain ordering reports the cost of its parenthesization · Reported matrix-chain cost is a lower bound · Matrix-chain ordering returns a valid parenthesization · Reconstruction size in matrix-chain ordering · Scalar multiplication count of a parenthesization

DefinitionDimension-compatible parenthesization#✓fully proved

Let \(p = (p_0, \dots, p_n)\) be a vector of natural numbers, regarding matrix \(i\) (for \(0 \le i < n\)) as having \(p_i\) rows and \(p_{i+1}\) columns. A parenthesization of \(n\) matrices is dimension-compatible with \(p\) when, at every product node, the column count of the left factor equals the row count of the right factor, where row and column counts are taken with respect to \(p\). A single leaf is always dimension-compatible.

@[expose] public def DimensionCompatible {n : Nat} (dimensions : Vector Nat (n + 1)) :
    Parenthesization n → Prop
  | .matrix _ => True
  | .multiply left right =>
      DimensionCompatible dimensions left ∧ DimensionCompatible dimensions right ∧
        cols dimensions left = rows dimensions right

Uses 3 · Used by 3

Statement usesParenthesization · Column count of a parenthesization · Row count of a parenthesization

Used byValid parenthesization · Reported matrix-chain cost is a lower bound · Matrix-chain ordering returns a valid parenthesization

DefinitionValid parenthesization#✓fully proved

Let \(p = (p_0, \dots, p_n)\) be a vector of natural numbers, regarding matrix \(i\) (for \(0 \le i < n\)) as having \(p_i\) rows and \(p_{i+1}\) columns. A parenthesization of \(n\) matrices is valid for \(p\) when its leaf indices, read left to right, are exactly \(0, 1, \dots, n - 1\), and it is dimension-compatible with \(p\).

@[expose] public def IsValid {n : Nat} (dimensions : Vector Nat (n + 1))
    (tree : Parenthesization n) : Prop :=
  tree.matrixIndices = List.finRange n ∧ tree.DimensionCompatible dimensions

Uses 3 · Used by 2

Statement usesParenthesization · Dimension-compatible parenthesization · Leaf indices of a parenthesization

Used byReported matrix-chain cost is a lower bound · Matrix-chain ordering returns a valid parenthesization

DefinitionScalar multiplication count of a parenthesization#✓fully proved

Let \(p = (p_0, \dots, p_n)\) be a vector of natural numbers, regarding matrix \(i\) (for \(0 \le i < n\)) as having \(p_i\) rows and \(p_{i+1}\) columns, and let \(r(T)\) and \(c(T)\) be the row and column counts of a parenthesization \(T\) with respect to \(p\). The scalar multiplication count of a single leaf is \(0\), and that of a product node with factors \(L\) and \(R\) is the sum of the counts of \(L\) and \(R\) plus \(r(L)\,c(L)\,c(R)\).

@[expose] public def scalarMultiplicationCost {n : Nat}
    (dimensions : Vector Nat (n + 1)) :
    Parenthesization n → Nat
  | .matrix _ => 0
  | .multiply left right =>
      scalarMultiplicationCost dimensions left + scalarMultiplicationCost dimensions right +
        left.rows dimensions * left.cols dimensions * right.cols dimensions

Uses 3 · Used by 6

Statement usesParenthesization · Column count of a parenthesization · Row count of a parenthesization

Used byMatrix-chain ordering · Split candidates evaluated by matrix-chain ordering · Matrix-chain ordering reports the cost of its parenthesization · Reported matrix-chain cost is a lower bound · Matrix-chain ordering returns a valid parenthesization · Reconstruction size in matrix-chain ordering

StructureMatrix-chain cost#✓fully proved

A matrix-chain cost is a pair of natural numbers counting the abstract events charged by matrix-chain ordering and reconstruction: the number of split candidates evaluated by the dynamic program, and the number of tree nodes emitted during reconstruction.

public structure Cost where
  /-- Split candidates evaluated by the dynamic program. -/
  candidateEvaluations : Nat
  /-- Tree constructors emitted during reconstruction. -/
  reconstructionNodes : Nat
deriving DecidableEq, Repr

Used by 9

Used byMatrix-chain ordering · Split candidates evaluated by matrix-chain ordering · Matrix-chain ordering reports the cost of its parenthesization · Reported matrix-chain cost is a lower bound · Matrix-chain ordering returns a valid parenthesization · Reconstruction size in matrix-chain ordering · Exact event count of matrix-chain ordering · Cubic bound for matrix-chain ordering · Total matrix-chain cost

DefinitionTotal matrix-chain cost#✓fully proved

The total of a matrix-chain cost is its number of candidate evaluations plus its number of reconstruction nodes.

@[expose] public def Cost.total (cost : Cost) : Nat :=
  cost.candidateEvaluations + cost.reconstructionNodes

Uses 1 · Used by 2

Statement usesMatrix-chain cost

Used byExact event count of matrix-chain ordering · Cubic bound for matrix-chain ordering

StructureMatrix-chain result#✓fully proved

A matrix-chain result for \(n\) matrices pairs a natural number, the reported optimal scalar multiplication count, with a parenthesization of \(n\) matrices, the reported optimal parenthesization. The structure itself does not require the count to be minimal or to be attained by the parenthesization.

public structure Result (n : Nat) where
  /-- Minimum scalar-multiplication count. -/
  optimalCost : Nat
  /-- Reconstructed optimal parenthesization. -/
  parenthesization : Parenthesization n
deriving DecidableEq, Repr

Uses 1 · Used by 8

Statement usesParenthesization

Used byMatrix-chain ordering · Split candidates evaluated by matrix-chain ordering · Matrix-chain ordering reports the cost of its parenthesization · Reported matrix-chain cost is a lower bound · Matrix-chain ordering returns a valid parenthesization · Reconstruction size in matrix-chain ordering · Exact event count of matrix-chain ordering · Cubic bound for matrix-chain ordering

DefinitionMatrix-chain ordering#✓fully proved

Given \(n \ge 1\) and natural numbers \(p_0, \dots, p_n\), where matrix \(i\) of the chain (\(0 \le i < n\)) has \(p_i\) rows and \(p_{i+1}\) columns, the algorithm computes, bottom-up by interval length, values \(m_{i,j}\) for \(0 \le i \le j < n\): \(m_{i,i} = 0\) and, for \(i < j\), \(m_{i,j}\) is the least value of \(m_{i,k} + m_{k+1,j} + p_i p_{k+1} p_{j+1}\) over \(i \le k < j\), and the first split point \(k\) attaining it is recorded. It then rebuilds a parenthesization of the whole chain from the recorded split points and returns \(m_{0,n-1}\) together with this parenthesization. One event is charged per evaluated split candidate and one per reconstructed tree node.

public def matrixChainOrder {n : Nat}
    (dimensions : Vector Nat (n + 1)) (hn : 0 < n) : TimeM Cost (Result n) :=
  let computation := matrixChainOrderRaw dimensions hn
  have hSome : computation.ret.isSome := by
    obtain ⟨cell, tree, hResult, hOptimal, hInterval, hCost⟩ :=
      matrixChainOrderRaw_spec dimensions hn
    change (matrixChainOrderRaw dimensions hn).ret.isSome
    rw [hResult]
    rfl
  { ret := computation.ret.get hSome, time := computation.time }

Uses 6 · Used by 7

Statement usesMatrix-chain cost · Parenthesization · Column count of a parenthesization · Row count of a parenthesization · Matrix-chain result · Scalar multiplication count of a parenthesization

Used bySplit candidates evaluated by matrix-chain ordering · Matrix-chain ordering reports the cost of its parenthesization · Reported matrix-chain cost is a lower bound · Matrix-chain ordering returns a valid parenthesization · Reconstruction size in matrix-chain ordering · Exact event count of matrix-chain ordering · Cubic bound for matrix-chain ordering

TheoremMatrix-chain ordering returns a valid parenthesization#✓fully proved

For every \(n \ge 1\) and all natural numbers \(p_0, \dots, p_n\), the parenthesization returned by the matrix-chain ordering algorithm on the dimensions \(p_0, \dots, p_n\) is valid: its leaves are the matrices \(0, 1, \dots, n - 1\) in order, each exactly once, and at every multiplication node the column count of the left factor equals the row count of the right factor, where matrix \(i\) has \(p_i\) rows and \(p_{i+1}\) columns.

public theorem matrixChainOrder_parenthesization_valid {n : Nat}
    (dimensions : Vector Nat (n + 1)) (hn : 0 < n) :
    let result := (matrixChainOrder dimensions hn).ret
    result.parenthesization.IsValid dimensions

Uses 10

Statement usesMatrix-chain cost · Parenthesization · Valid parenthesization · Matrix-chain result · Matrix-chain ordering

Proof usesDimension-compatible parenthesization · Column count of a parenthesization · Leaf indices of a parenthesization · Row count of a parenthesization · Scalar multiplication count of a parenthesization

TheoremMatrix-chain ordering reports the cost of its parenthesization#✓fully proved

For every \(n \ge 1\) and all natural numbers \(p_0, \dots, p_n\), the scalar-multiplication cost of the parenthesization returned by the matrix-chain ordering algorithm on the dimensions \(p_0, \dots, p_n\) equals the optimal cost it reports.

public theorem matrixChainOrder_cost_eq {n : Nat} (dimensions : Vector Nat (n + 1))
    (hn : 0 < n) :
    let result := (matrixChainOrder dimensions hn).ret
    scalarMultiplicationCost dimensions result.parenthesization = result.optimalCost

Uses 7

Statement usesMatrix-chain cost · Parenthesization · Matrix-chain result · Matrix-chain ordering · Scalar multiplication count of a parenthesization

Proof usesColumn count of a parenthesization · Row count of a parenthesization

TheoremReported matrix-chain cost is a lower bound#✓fully proved

For every \(n \ge 1\), all natural numbers \(p_0, \dots, p_n\) and every parenthesization \(T\) of \(n\) matrices that is valid for these dimensions, the optimal cost reported by the matrix-chain ordering algorithm on the dimensions \(p_0, \dots, p_n\) is at most the scalar-multiplication cost of \(T\).

public theorem matrixChainOrder_minimal {n : Nat} (dimensions : Vector Nat (n + 1))
    (hn : 0 < n) (tree : Parenthesization n) (hTree : tree.IsValid dimensions) :
    (matrixChainOrder dimensions hn).ret.optimalCost ≤
      scalarMultiplicationCost dimensions tree

Uses 10

Statement usesMatrix-chain cost · Parenthesization · Valid parenthesization · Matrix-chain result · Matrix-chain ordering · Scalar multiplication count of a parenthesization

Proof usesDimension-compatible parenthesization · Column count of a parenthesization · Leaf indices of a parenthesization · Row count of a parenthesization

TheoremSplit candidates evaluated by matrix-chain ordering#✓fully proved

For every \(n \ge 1\) and all natural numbers \(p_0, \dots, p_n\), the matrix-chain ordering algorithm run on the dimensions \(p_0, \dots, p_n\) evaluates exactly \(\binom{n+1}{3}\) split candidates.

This is the number of triples \(i \le k < j < n\), so the dynamic program evaluates one candidate for every interval split.

public theorem matrixChainOrder_candidateEvaluations {n : Nat}
    (dimensions : Vector Nat (n + 1)) (hn : 0 < n) :
    (matrixChainOrder dimensions hn).time.candidateEvaluations = Nat.choose (n + 1) 3

Uses 7 · Used by 1

Statement usesMatrix-chain cost · Matrix-chain result · Matrix-chain ordering

Proof usesParenthesization · Column count of a parenthesization · Row count of a parenthesization · Scalar multiplication count of a parenthesization

Used byExact event count of matrix-chain ordering

TheoremReconstruction size in matrix-chain ordering#✓fully proved

For every \(n \ge 1\) and all natural numbers \(p_0, \dots, p_n\), the matrix-chain ordering algorithm run on the dimensions \(p_0, \dots, p_n\) charges exactly \(2n - 1\) reconstruction events.

This is the number of nodes of a full binary tree with \(n\) leaves.

public theorem matrixChainOrder_reconstructionNodes {n : Nat}
    (dimensions : Vector Nat (n + 1)) (hn : 0 < n) :
    (matrixChainOrder dimensions hn).time.reconstructionNodes = 2 * n - 1

Uses 7 · Used by 1

Statement usesMatrix-chain cost · Matrix-chain result · Matrix-chain ordering

Proof usesParenthesization · Column count of a parenthesization · Row count of a parenthesization · Scalar multiplication count of a parenthesization

Used byExact event count of matrix-chain ordering

TheoremExact event count of matrix-chain ordering#✓fully proved

For every \(n \ge 1\) and all natural numbers \(p_0, \dots, p_n\), the total number of events charged by the matrix-chain ordering algorithm run on the dimensions \(p_0, \dots, p_n\) is \(\binom{n+1}{3} + (2n - 1)\).

The first term counts evaluated split candidates and the second the nodes of the reconstructed tree.

public theorem matrixChainOrder_time {n : Nat} (dimensions : Vector Nat (n + 1))
    (hn : 0 < n) :
    (matrixChainOrder dimensions hn).time.total =
      Nat.choose (n + 1) 3 + (2 * n - 1)

Uses 6 · Used by 1

Statement usesMatrix-chain cost · Total matrix-chain cost · Matrix-chain result · Matrix-chain ordering

Proof usesSplit candidates evaluated by matrix-chain ordering · Reconstruction size in matrix-chain ordering

Used byCubic bound for matrix-chain ordering

TheoremCubic bound for matrix-chain ordering#✓fully proved

For every \(n \ge 1\) and all natural numbers \(p_0, \dots, p_n\), the total number of events charged by the matrix-chain ordering algorithm run on the dimensions \(p_0, \dots, p_n\) is at most \(3n^3\).

public theorem matrixChainOrder_time_le_three_mul_cube {n : Nat}
    (dimensions : Vector Nat (n + 1)) (hn : 0 < n) :
    (matrixChainOrder dimensions hn).time.total ≤ 3 * n ^ 3

Uses 5

Statement usesMatrix-chain cost · Total matrix-chain cost · Matrix-chain result · Matrix-chain ordering

Proof usesExact event count of matrix-chain ordering

18 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.