Prim's algorithm

DefinitionPrim's algorithm with an indexed binary heap#✓fully proved

Let \(W\) be a linearly ordered type with a zero element, let \(W \cup \{\top\}\) be \(W\) with a new greatest element \(\top\) adjoined, let \(D\) be a directed adjacency structure on the vertices \(0, \dots, n-1\), with vertex list \(L\) and adjacency lists \(A(u)\), let \(w\) assign a weight \(w(\{u, v\}) \in W\) to every unordered pair \(\{u, v\}\) of vertices, not necessarily distinct, and let \(r\) be a vertex. Prim's algorithm starts with no vertex having a parent and inserts the vertices, in the order of \(L\), into an empty indexed minimum queue over the identities \(0, \dots, n-1\), with key \(0\) for \(r\) and key \(\top\) for every other vertex. It then repeats the following at most \(n\) times, stopping early when the queue is empty: it extracts the entry of minimum key, ties broken by the smaller vertex, say with vertex \(u\), and for each entry \(v\) of \(A(u)\) in order, if \(v\) is still in the queue and \(w(\{u, v\})\) is strictly smaller than the current key of \(v\), it sets the parent of \(v\) to \(u\) and decreases the key of \(v\) to \(w(\{u, v\})\). It returns, for each vertex, its parent or nothing.

Costs are counted as seven numbers: the five event counts of the queue operations (comparisons, swaps, reads of the position vector, writes to the position vector, and entry appends, pops or replacements), the number of adjacency entries inspected, and the number of inspected entries found still in the queue, which is the number of key comparisons. On a disconnected graph every vertex is still extracted and the parents form a forest.

public def prim {W : Type u} [LinearOrder W] [Zero W] {n : Nat}
    (graph : DirectedAdjacency (Fin n)) (weight : Sym2 (Fin n) → W) (root : Fin n) :
    TimeM ((Fin 5 → Nat) × Nat × Nat) (Vector (Option (Fin n)) n) :=
  let actual := Cslib.Algorithms.Lean.Prim.worker graph weight root
  ⟨actual.ret.parent, actual.time⟩

Uses 9 · Used by 11

Statement usesDirected adjacency graph · Indexed minimum queue · Decrease-key in an indexed minimum queue · Empty indexed minimum queue · Extract-min in an indexed minimum queue · Insertion into an indexed minimum queue · Membership test in an indexed minimum queue · Recorded positions lie inside the heap · Binary min-heap

Used byPrim's parent array is a parent tree · Prim's parent array on the complete graph · Prim's tree is a minimum spanning tree · Adjacency inspections of Prim's algorithm on a simple graph · Logarithmic heap cost of Prim's algorithm · Number of adjacency inspections in Prim's algorithm · Prim's algorithm returns a tree · Bound on key comparisons in Prim's algorithm · Prim's algorithm returns a minimum spanning tree · Parents returned by Prim's algorithm are adjacency-list neighbors · The root has no parent in Prim's algorithm

TheoremNumber of adjacency inspections in Prim's algorithm#✓fully proved

Let \(W\) be a linearly ordered type with a zero element, let \(D\) be a directed adjacency structure on the vertices \(0, \dots, n-1\) with adjacency lists \(A(u)\), let \(w\) assign a weight in \(W\) to every unordered pair of vertices, not necessarily distinct, and let \(r\) be a vertex. The number of adjacency entries inspected by Prim's algorithm on \(D\), \(w\) and \(r\) equals the sum of the lengths \(|A(u)|\) over all vertices \(u\).

public theorem prim_inspections {W : Type u} [LinearOrder W] [Zero W] {n : Nat}
    (graph : DirectedAdjacency (Fin n)) (weight : Sym2 (Fin n) → W) (root : Fin n) :
    (prim graph weight root).time.2.1 =
      (graph.vertices.map (fun v => (graph.adjacency v).length)).sum

Uses 27

Statement usesDirected adjacency graph · Prim's algorithm with an indexed binary heap

Proof usesIndexed minimum queue · Decrease-key in an indexed minimum queue · Decrease-key fails exactly on absent identities and non-decreases · Successful decrease-key · Empty indexed minimum queue · The empty indexed min queue has no present identity · Extract-min in an indexed minimum queue · Extraction from an indexed min queue fails exactly when it is empty · Successful extraction from an indexed min queue · Insertion into an indexed minimum queue · Insertion fails exactly on present identities · Successful insertion into an indexed min queue · Membership test in an indexed minimum queue · Membership reads the position vector · Absent identities carry no heap entry · Recorded positions lie inside the heap · Binary min-heap · Elements of a binary min-heap · Elements after binary heap insertion · Extracting the minimum of a binary min-heap · Binary heap extraction splits off the minimum · The value extracted from a binary min-heap is one of its elements · Insertion into a binary min-heap · Sift-up · Sift-up permutes the array

TheoremBound on key comparisons in Prim's algorithm#✓fully proved

Let \(W\) be a linearly ordered type with a zero element, let \(D\) be a directed adjacency structure on the vertices \(0, \dots, n-1\) with adjacency lists \(A(u)\), let \(w\) assign a weight in \(W\) to every unordered pair of vertices, not necessarily distinct, and let \(r\) be a vertex. The number of inspected adjacency entries that Prim's algorithm on \(D\), \(w\) and \(r\) finds still in the queue, which is its number of key comparisons, is at most the sum of the lengths \(|A(u)|\) over all vertices \(u\).

public theorem prim_key_tests_le {W : Type u} [LinearOrder W] [Zero W] {n : Nat}
    (graph : DirectedAdjacency (Fin n)) (weight : Sym2 (Fin n) → W) (root : Fin n) :
    (prim graph weight root).time.2.2 ≤
      (graph.vertices.map (fun v => (graph.adjacency v).length)).sum

Uses 27

Statement usesDirected adjacency graph · Prim's algorithm with an indexed binary heap

Proof usesIndexed minimum queue · Decrease-key in an indexed minimum queue · Decrease-key fails exactly on absent identities and non-decreases · Successful decrease-key · Empty indexed minimum queue · The empty indexed min queue has no present identity · Extract-min in an indexed minimum queue · Extraction from an indexed min queue fails exactly when it is empty · Successful extraction from an indexed min queue · Insertion into an indexed minimum queue · Insertion fails exactly on present identities · Successful insertion into an indexed min queue · Membership test in an indexed minimum queue · Membership reads the position vector · Absent identities carry no heap entry · Recorded positions lie inside the heap · Binary min-heap · Elements of a binary min-heap · Elements after binary heap insertion · Extracting the minimum of a binary min-heap · Binary heap extraction splits off the minimum · The value extracted from a binary min-heap is one of its elements · Insertion into a binary min-heap · Sift-up · Sift-up permutes the array

TheoremLogarithmic heap cost of Prim's algorithm#✓fully proved

Let \(W\) be a linearly ordered type with a zero element, let \(D\) be a directed adjacency structure on the vertices \(0, \dots, n-1\) with adjacency lists \(A(u)\), let \(w\) assign a weight in \(W\) to every unordered pair of vertices, not necessarily distinct, let \(r\) be a vertex, and let \(a\) be the sum of the lengths \(|A(u)|\) over all vertices \(u\). Each of the five heap event counts of Prim's algorithm on \(D\), \(w\) and \(r\) (comparisons, swaps, reads of the position vector, writes to the position vector, and entry appends, pops or replacements) is at most \(20(2n + a)(\lfloor \log_2(n + 1) \rfloor + 1) + a\).

public theorem prim_heap_time {W : Type u} [LinearOrder W] [Zero W] {n : Nat}
    (graph : DirectedAdjacency (Fin n)) (weight : Sym2 (Fin n) → W) (root : Fin n) :
    let a := (graph.vertices.map (fun v => (graph.adjacency v).length)).sum
    ∀ c : Fin 5, (prim graph weight root).time.1 c ≤
      20 * (2 * n + a) * (Nat.log2 (n + 1) + 1) + a

Uses 31

Statement usesDirected adjacency graph · Prim's algorithm with an indexed binary heap

Proof usesIndexed minimum queue · Decrease-key in an indexed minimum queue · Decrease-key fails exactly on absent identities and non-decreases · Successful decrease-key · Logarithmic event bound for indexed-queue decrease-key · Empty indexed minimum queue · The empty indexed min queue has no present identity · Extract-min in an indexed minimum queue · Extraction from an indexed min queue fails exactly when it is empty · Successful extraction from an indexed min queue · Logarithmic event bound for indexed-queue extract-min · Insertion into an indexed minimum queue · Insertion fails exactly on present identities · Successful insertion into an indexed min queue · Logarithmic event bound for indexed-queue insertion · Membership test in an indexed minimum queue · Membership reads the position vector · Membership costs one position read · Absent identities carry no heap entry · Recorded positions lie inside the heap · Binary min-heap · Elements of a binary min-heap · Elements after binary heap insertion · Extracting the minimum of a binary min-heap · Binary heap extraction splits off the minimum · The value extracted from a binary min-heap is one of its elements · Insertion into a binary min-heap · Sift-up · Sift-up permutes the array

TheoremAdjacency inspections of Prim's algorithm on a simple graph#✓fully proved

Let \(W\) be a linearly ordered type with a zero element, let \(G\) be a simple graph on the vertices \(0, \dots, n-1\), let \(D\) be a directed adjacency structure on the same vertices with adjacency lists \(A(u)\), let \(w\) assign a weight in \(W\) to every unordered pair of vertices, not necessarily distinct, and let \(r\) be a vertex. Suppose that for all vertices \(u\) and \(v\), \(v\) occurs in \(A(u)\) exactly when \(u\) and \(v\) are adjacent in \(G\), and that no list \(A(u)\) has repeated entries. Then the number of adjacency entries inspected by Prim's algorithm on \(D\), \(w\) and \(r\) is twice the number of edges of \(G\).

public theorem prim_edge_inspections {W : Type u} [LinearOrder W] [Zero W] {n : Nat}
    (graph : DirectedAdjacency (Fin n)) (G : SimpleGraph (Fin n))
    (weight : Sym2 (Fin n) → W) (root : Fin n) : by
    classical
    exact (∀ u v : Fin n, v ∈ graph.adjacency u ↔ G.Adj u v) →
      (∀ u : Fin n, (graph.adjacency u).Nodup) →
      (prim graph weight root).time.2.1 = 2 * G.edgeFinset.card

Uses 27

Statement usesDirected adjacency graph · Prim's algorithm with an indexed binary heap

Proof usesIndexed minimum queue · Decrease-key in an indexed minimum queue · Decrease-key fails exactly on absent identities and non-decreases · Successful decrease-key · Empty indexed minimum queue · The empty indexed min queue has no present identity · Extract-min in an indexed minimum queue · Extraction from an indexed min queue fails exactly when it is empty · Successful extraction from an indexed min queue · Insertion into an indexed minimum queue · Insertion fails exactly on present identities · Successful insertion into an indexed min queue · Membership test in an indexed minimum queue · Membership reads the position vector · Absent identities carry no heap entry · Recorded positions lie inside the heap · Binary min-heap · Elements of a binary min-heap · Elements after binary heap insertion · Extracting the minimum of a binary min-heap · Binary heap extraction splits off the minimum · The value extracted from a binary min-heap is one of its elements · Insertion into a binary min-heap · Sift-up · Sift-up permutes the array

TheoremThe root has no parent in Prim's algorithm#✓fully proved

Let \(W\) be a linearly ordered type with a zero element, let \(D\) be a directed adjacency structure on the vertices \(0, \dots, n-1\), let \(w\) assign a weight in \(W\) to every unordered pair of vertices, not necessarily distinct, and let \(r\) be a vertex. In the output of Prim's algorithm on \(D\), \(w\) and \(r\), the vertex \(r\) has no parent.

public theorem prim_root {W : Type u} [LinearOrder W] [Zero W] {n : Nat}
    (graph : DirectedAdjacency (Fin n)) (weight : Sym2 (Fin n) → W) (root : Fin n) :
    (prim graph weight root).ret[root] = none

Uses 25 · Used by 1

Statement usesDirected adjacency graph · Prim's algorithm with an indexed binary heap

Proof usesIndexed minimum queue · Decrease-key in an indexed minimum queue · Decrease-key fails exactly on absent identities and non-decreases · Successful decrease-key · Empty indexed minimum queue · The empty indexed min queue has no present identity · Extract-min in an indexed minimum queue · Extraction from an indexed min queue fails exactly when it is empty · Successful extraction from an indexed min queue · Insertion into an indexed minimum queue · Insertion fails exactly on present identities · Successful insertion into an indexed min queue · Membership test in an indexed minimum queue · Membership reads the position vector · Recorded positions lie inside the heap · Binary min-heap · Elements of a binary min-heap · Elements after binary heap insertion · Extracting the minimum of a binary min-heap · The value extracted from a binary min-heap is minimal · The value extracted from a binary min-heap is one of its elements · Insertion into a binary min-heap · Sift-up

Used byPrim's parent array is a parent tree

TheoremParents returned by Prim's algorithm are adjacency-list neighbors#✓fully proved

Let \(W\) be a linearly ordered type with a zero element, let \(D\) be a directed adjacency structure on the vertices \(0, \dots, n-1\) with adjacency lists \(A(u)\), let \(w\) assign a weight in \(W\) to every unordered pair of vertices, not necessarily distinct, and let \(r\) be a vertex. For all vertices \(u\) and \(v\), if Prim's algorithm on \(D\), \(w\) and \(r\) returns \(u\) as the parent of \(v\), then \(v\) occurs in \(A(u)\).

public theorem prim_parent_edge {W : Type u} [LinearOrder W] [Zero W] {n : Nat}
    (graph : DirectedAdjacency (Fin n)) (weight : Sym2 (Fin n) → W) (root : Fin n) :
    ∀ u v : Fin n, (prim graph weight root).ret[v] = some u →
      v ∈ graph.adjacency u

Uses 12

Statement usesDirected adjacency graph · Prim's algorithm with an indexed binary heap

Proof usesIndexed minimum queue · Decrease-key in an indexed minimum queue · Decrease-key fails exactly on absent identities and non-decreases · Empty indexed minimum queue · Extract-min in an indexed minimum queue · Insertion into an indexed minimum queue · Membership test in an indexed minimum queue · Membership reads the position vector · Recorded positions lie inside the heap · Binary min-heap

TheoremPrim's algorithm returns a tree#✓fully proved

Let \(W\) be a linearly ordered type with a zero element, let \(G\) be a connected simple graph on the vertices \(0, \dots, n-1\), let \(D\) be a directed adjacency structure on the same vertices with adjacency lists \(A(u)\) such that for all vertices \(u\) and \(v\), \(v\) occurs in \(A(u)\) exactly when \(u\) and \(v\) are adjacent in \(G\), let \(w\) assign a weight in \(W\) to every unordered pair of vertices, not necessarily distinct, and let \(r\) be a vertex. Let \(T\) be the simple graph on the vertices \(0, \dots, n-1\) in which two distinct vertices are adjacent when one of them is the parent of the other in the output of Prim's algorithm on \(D\), \(w\) and \(r\). Then \(T\) is a tree.

public theorem prim_isTree {W : Type u} [LinearOrder W] [Zero W] {n : Nat}
    (graph : DirectedAdjacency (Fin n)) (G : SimpleGraph (Fin n)) (weight : Sym2 (Fin n) → W)
    (root : Fin n) (hadj : ∀ u v : Fin n, v ∈ graph.adjacency u ↔ G.Adj u v) (hG : G.Connected) :
    (SimpleGraph.fromRel fun u v : Fin n => (prim graph weight root).ret[v] = some u).IsTree

Uses 29 · Used by 1

Statement usesDirected adjacency graph · Prim's algorithm with an indexed binary heap

Proof usesIndexed minimum queue · Decrease-key in an indexed minimum queue · Decrease-key fails exactly on absent identities and non-decreases · Successful decrease-key · Empty indexed minimum queue · The empty indexed min queue has no present identity · Extract-min in an indexed minimum queue · Extraction from an indexed min queue fails exactly when it is empty · Successful extraction from an indexed min queue · Insertion into an indexed minimum queue · Insertion fails exactly on present identities · Successful insertion into an indexed min queue · Membership test in an indexed minimum queue · Membership reads the position vector · Absent identities carry no heap entry · Recorded positions lie inside the heap · Binary min-heap · Elements of a binary min-heap · Elements after binary heap insertion · Extracting the minimum of a binary min-heap · Binary heap extraction splits off the minimum · The value extracted from a binary min-heap is minimal · The value extracted from a binary min-heap is one of its elements · Membership after extraction from a binary min-heap · Insertion into a binary min-heap · Sift-up · Sift-up permutes the array

Used byPrim's tree is a spanning tree

TheoremPrim's algorithm returns a minimum spanning tree#✓fully proved

Let \(G\) be a connected simple graph on the vertices \(0, \dots, n-1\), let \(D\) be a directed adjacency structure on the same vertices with adjacency lists \(A(u)\) such that for all vertices \(u\) and \(v\), \(v\) occurs in \(A(u)\) exactly when \(u\) and \(v\) are adjacent in \(G\), let \(w\) assign a real weight \(w(e)\) to every unordered pair \(e\) of vertices, not necessarily distinct, and let \(r\) be a vertex. Let \(T\) be the simple graph on the vertices \(0, \dots, n-1\) in which two distinct vertices are adjacent when one of them is the parent of the other in the output of Prim's algorithm on \(D\), \(w\) and \(r\), and write \(E(H)\) for the edge set of a graph \(H\). Then every edge of \(T\) is an edge of \(G\), \(T\) is a tree, and every graph \(H\) on the vertices \(0, \dots, n-1\) that is a tree and whose edges are all edges of \(G\) satisfies \(\sum_{e \in E(T)} w(e) \le \sum_{e \in E(H)} w(e)\).

Weights are arbitrary signed real numbers, and ties are allowed.

public theorem prim_minimum_spanningTree {n : Nat} (graph : DirectedAdjacency (Fin n))
    (G : SimpleGraph (Fin n))
    (weight : Sym2 (Fin n) → ℝ) (root : Fin n) : by
    classical
    exact (∀ u v : Fin n, v ∈ graph.adjacency u ↔ G.Adj u v) → G.Connected →
      let parents := (prim graph weight root).ret
      let T := SimpleGraph.fromRel (fun u v : Fin n => parents[v] = some u)
      T ≤ G ∧ T.IsTree ∧ ∀ H : SimpleGraph (Fin n), H ≤ G → H.IsTree →
        (∑ e ∈ T.edgeFinset, weight e) ≤ ∑ e ∈ H.edgeFinset, weight e

Uses 29 · Used by 1

Statement usesDirected adjacency graph · Prim's algorithm with an indexed binary heap

Proof usesIndexed minimum queue · Decrease-key in an indexed minimum queue · Decrease-key fails exactly on absent identities and non-decreases · Successful decrease-key · Empty indexed minimum queue · The empty indexed min queue has no present identity · Extract-min in an indexed minimum queue · Extraction from an indexed min queue fails exactly when it is empty · Successful extraction from an indexed min queue · Insertion into an indexed minimum queue · Insertion fails exactly on present identities · Successful insertion into an indexed min queue · Membership test in an indexed minimum queue · Membership reads the position vector · Absent identities carry no heap entry · Recorded positions lie inside the heap · Binary min-heap · Elements of a binary min-heap · Elements after binary heap insertion · Extracting the minimum of a binary min-heap · Binary heap extraction splits off the minimum · The value extracted from a binary min-heap is minimal · The value extracted from a binary min-heap is one of its elements · Membership after extraction from a binary min-heap · Insertion into a binary min-heap · Sift-up · Sift-up permutes the array

Used byPrim's tree is a minimum spanning tree

9 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.