Dijkstra's algorithm on the word RAM: statements

This file defines the single-source shortest-path problem solved by Dijkstra's algorithm Dijkstra Cormen et al., Section 24.3.

An instance (Cslib.Algorithms.WordRAM.Dijkstra.Instance) is a directed graph on Fin n with natural-number edge weights, given by its weight matrix, and a source vertex. The distance Cslib.Algorithms.WordRAM.Dijkstra.Instance.dist is the infimum, in ℕ∞, of the weights of the paths (Quiver.Path, Quiver.Path.addWeight) between two vertices; it is ⊤ when there is no path. A program writes a distance as a word with 0 for an unreachable vertex and d + 1 for distance d (Cslib.Algorithms.WordRAM.Dijkstra.encodeDist).

Main definitions

• Cslib.Algorithms.WordRAM.Dijkstra.Instance: a weighted directed graph with a source.
• Cslib.Algorithms.WordRAM.Dijkstra.Instance.dist: the shortest-path distance.
• Cslib.Algorithms.WordRAM.Dijkstra.encodeDist: a distance as a word.

Main results

• Cslib.Algorithms.WordRAM.Dijkstra.Instance.dist_self: every vertex is at distance 0 from itself.

References

• E. W. Dijkstra, A note on two problems in connexion with graphs
• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms

structure Cslib.Algorithms.WordRAM.Dijkstra.Instance : Type

An instance of the single-source shortest-path problem: a directed graph on Fin n with natural-number edge weights, given by its weight matrix, and a source vertex. The entry weight u v is some c for an edge from u to v of weight c, and none for no edge.

• n : ℕ

  The number of vertices.

• weight : Fin self.n → Fin self.n → Option ℕ

  The weight matrix.

• source : Fin self.n

  The source.

def Cslib.Algorithms.WordRAM.Dijkstra.Instance.Vertex (I : Instance) : Type

The vertices of an instance, as a quiver: an arrow from u to v is a weight c with I.weight u v = some c, so there is at most one.

@[instance_reducible]

instance Cslib.Algorithms.WordRAM.Dijkstra.Instance.instQuiverVertex (I : Instance) : Quiver I.Vertex

def Cslib.Algorithms.WordRAM.Dijkstra.Instance.arrowWeight (I : Instance) {u v : I.Vertex} (e : u ⟶ v) : ℕ∞

The weight of an arrow.

noncomputable def Cslib.Algorithms.WordRAM.Dijkstra.Instance.dist (I : Instance) (u v : Fin I.n) : ℕ∞

The shortest-path distance from u to v: the infimum of the weights of the paths from u to v, and ⊤ when there is none.

theorem Cslib.Algorithms.WordRAM.Dijkstra.Instance.dist_self (I : Instance) (u : Fin I.n) : I.dist u u = 0

Every vertex is at distance 0 from itself, by the empty path.

def Cslib.Algorithms.WordRAM.Dijkstra.Instance.maxWeight (I : Instance) : ℕ

The largest edge weight, and 0 when there is no edge.

def Cslib.Algorithms.WordRAM.Dijkstra.encodeDist (d : ℕ∞) : ℕ

A distance as a word: 0 for an unreachable vertex and d + 1 for distance d.