Documentation

MiscMath.Computability.RedBluePebbleGame.MatMulChain

The red-blue pebble game: the ordinary algorithm for matrix multiplication, as a graph #

Support module of MiscMath.Computability.RedBluePebbleGame, where the results are stated and where the reader should start. Nothing here is a result on its own.

The graph of the ordinary algorithm for the product of an m × k matrix A by a k × n matrix B, each entry of the product summed left to right (MatMulChain.edge). Its vertices are the entries of A and B, the products A i l * B l j, and for each entry (i, j) of the product the partial sums of its products at positions 0, …, r + 1, for r < k - 1. The inputs are the vertices with no predecessor and the outputs those with no successor.

For m, k, n ≥ 1 it is an IsMatMulEvaluation (MatMulChain.isMatMulEvaluation), and it has a complete calculation exactly when S ≥ 3 (MatMulChain.complete_iff): the witness of exists_isMatMulEvaluation. Three red pebbles suffice for any finite graph whose non-inputs each have exactly two predecessors and which some rank orders (hasCompleteCalculation_of_rank, which generalises the FFT graph's fft_run_union): load the two predecessors, compute, store, clear.

theorem MiscMath.Computability.RedBluePebbleGame.acyclic_of_rank {V : Type u_1} {E : V → V → Prop} (f : V → ℕ) (hf : ∀ (u v : V), E u v → f u < f v) (v : V) :

¬Relation.TransGen E v v

A rank that every edge raises rules out cycles.

theorem MiscMath.Computability.RedBluePebbleGame.run_union_of_rank {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} (f : V → ℕ) (hf : ∀ (u v : V), E u v → f u < f v) (hS : 3 ≤ S) (hpred : ∀ v ∉ I, ∃ (p₁ : V) (p₂ : V), p₁ ≠ p₂ ∧ E p₁ v ∧ E p₂ v ∧ ∀ (u : V), E u v → u = p₁ ∨ u = p₂) (X : Finset V) :

(∀ v ∈ X, v ∉ I) → (∀ v ∈ X, ∀ (u : V), E u v → u ∈ I ∨ u ∈ X) → ∃ (q : ℕ), Run E I S (∅, I) q (∅, I ∪ X)

In a graph ordered by a rank, in which every non-input has exactly two predecessors, every predecessor-closed set of non-inputs can be computed and stored with three red pebbles.

theorem MiscMath.Computability.RedBluePebbleGame.hasCompleteCalculation_of_rank {V : Type u_1} [DecidableEq V] {E : V → V → Prop} {I : Finset V} {S : ℕ} [Finite V] (f : V → ℕ) (hf : ∀ (u v : V), E u v → f u < f v) (hS : 3 ≤ S) (hpred : ∀ v ∉ I, ∃ (p₁ : V) (p₂ : V), p₁ ≠ p₂ ∧ E p₁ v ∧ E p₂ v ∧ ∀ (u : V), E u v → u = p₁ ∨ u = p₂) (O : Finset V) :

∃ (q : ℕ), HasCompleteCalculation E I O S q

Three red pebbles suffice for a finite graph ordered by a rank, in which every non-input has exactly two predecessors, whatever its outputs: compute and store every vertex, then delete the blue pebbles off the vertices that are not outputs.

inductive MiscMath.Computability.RedBluePebbleGame.MatMulChain.Vertex (m k n : ℕ) :

The vertices of the graph of the ordinary algorithm for the product of an m × k matrix A by a k × n matrix B, each entry of the product summed left to right.

a {m k n : ℕ} (i : Fin m) (l : Fin k) : Vertex m k n
The entry A i l.
b {m k n : ℕ} (l : Fin k) (j : Fin n) : Vertex m k n
The entry B l j.
prod {m k n : ℕ} (i : Fin m) (l : Fin k) (j : Fin n) : Vertex m k n
The product A i l * B l j.
sum {m k n : ℕ} (i : Fin m) (r : Fin (k - 1)) (j : Fin n) : Vertex m k n
The partial sum of the products A i l * B l j for l ≤ r + 1.

Instances For

@[instance_reducible]

instance MiscMath.Computability.RedBluePebbleGame.MatMulChain.instDecidableEqVertex {m✝ k✝ n✝ : ℕ} :

DecidableEq (Vertex m✝ k✝ n✝)

Equations

MiscMath.Computability.RedBluePebbleGame.MatMulChain.instDecidableEqVertex = MiscMath.Computability.RedBluePebbleGame.MatMulChain.instDecidableEqVertex.decEq

def MiscMath.Computability.RedBluePebbleGame.MatMulChain.instDecidableEqVertex.decEq {m✝ k✝ n✝ : ℕ} (x✝ x✝¹ : Vertex m✝ k✝ n✝) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[instance_reducible]

instance MiscMath.Computability.RedBluePebbleGame.MatMulChain.instFintypeVertex {m✝ k✝ n✝ : ℕ} :

Fintype (Vertex m✝ k✝ n✝)

Equations

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

def MiscMath.Computability.RedBluePebbleGame.MatMulChain.edge {m k n : ℕ} :

Vertex m k n → Vertex m k n → Prop

The edges: each product from its two factors, the first partial sum of an entry from its first two products, and each later partial sum from the one before it and the next product. Indices are compared as natural numbers.

Equations

One or more equations did not get rendered due to their size.
MiscMath.Computability.RedBluePebbleGame.MatMulChain.edge x✝¹ x✝ = False

Instances For

@[instance_reducible]

instance MiscMath.Computability.RedBluePebbleGame.MatMulChain.instDecidableRelVertexEdge {m k n : ℕ} :

DecidableRel edge

Equations

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

def MiscMath.Computability.RedBluePebbleGame.MatMulChain.rank {m k n : ℕ} :

Vertex m k n → ℕ

A rank raised by every edge.

Equations

Instances For

theorem MiscMath.Computability.RedBluePebbleGame.MatMulChain.rank_lt {m k n : ℕ} {u v : Vertex m k n} (h : edge u v) :

rank u < rank v

def MiscMath.Computability.RedBluePebbleGame.MatMulChain.entry {m k n : ℕ} :

Vertex m k n → Option (Fin m × Fin n)

The entry of the product that a product or a partial sum belongs to.

Equations

Instances For

theorem MiscMath.Computability.RedBluePebbleGame.MatMulChain.entry_eq {m k n : ℕ} {u v : Vertex m k n} {e : Fin m × Fin n} (h : edge u v) (hu : entry u = some e) :

entry v = some e

theorem MiscMath.Computability.RedBluePebbleGame.MatMulChain.entry_of_reach {m k n : ℕ} {i : Fin m} {l : Fin k} {j : Fin n} {w : Vertex m k n} (h : Relation.ReflTransGen edge (Vertex.prod i l j) w) :

entry w = some (i, j)

Everything reached from a product belongs to its entry.

def MiscMath.Computability.RedBluePebbleGame.MatMulChain.inputs (m k n : ℕ) :

Finset (Vertex m k n)

The inputs: the vertices with no predecessor.

Equations

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

Instances For

def MiscMath.Computability.RedBluePebbleGame.MatMulChain.outputs (m k n : ℕ) :

Finset (Vertex m k n)

The outputs: the vertices with no successor.

Equations

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

Instances For

theorem MiscMath.Computability.RedBluePebbleGame.MatMulChain.a_mem_inputs {m k n : ℕ} (i : Fin m) (l : Fin k) :

Vertex.a i l ∈ inputs m k n

theorem MiscMath.Computability.RedBluePebbleGame.MatMulChain.b_mem_inputs {m k n : ℕ} (l : Fin k) (j : Fin n) :

Vertex.b l j ∈ inputs m k n

theorem MiscMath.Computability.RedBluePebbleGame.MatMulChain.isComputationDAG {m k n : ℕ} (hm : 1 ≤ m) (hn : 1 ≤ n) :

IsComputationDAG edge (inputs m k n) (outputs m k n)

theorem MiscMath.Computability.RedBluePebbleGame.MatMulChain.isMatMulLabelling {m k n : ℕ} :

IsMatMulLabelling edge (inputs m k n) (fun (y : Fin m × Fin k) => Vertex.a y.1 y.2) (fun (z : Fin k × Fin n) => Vertex.b z.1 z.2) fun (x : Fin m × Fin k × Fin n) => Vertex.prod x.1 x.2.1 x.2.2

theorem MiscMath.Computability.RedBluePebbleGame.MatMulChain.isMatMulEvaluation {m k n : ℕ} (hm : 1 ≤ m) (hn : 1 ≤ n) :

IsMatMulEvaluation m k n edge (inputs m k n) (outputs m k n)

theorem MiscMath.Computability.RedBluePebbleGame.MatMulChain.preds {m k n : ℕ} (v : Vertex m k n) (hv : v ∉ inputs m k n) :

∃ (p₁ : Vertex m k n) (p₂ : Vertex m k n), p₁ ≠ p₂ ∧ edge p₁ v ∧ edge p₂ v ∧ ∀ (u : Vertex m k n), edge u v → u = p₁ ∨ u = p₂

Every vertex that is not an input has exactly two predecessors.

theorem MiscMath.Computability.RedBluePebbleGame.MatMulChain.complete_iff {m k n : ℕ} (hm : 1 ≤ m) (hk : 1 ≤ k) (hn : 1 ≤ n) (S : ℕ) :

(∃ (q : ℕ), HasCompleteCalculation edge (inputs m k n) (outputs m k n) S q) ↔ 3 ≤ S

Feasibility. For m, k, n ≥ 1 the graph has a complete calculation exactly when S ≥ 3.