Dijkstra's algorithm on the word RAM with a Fibonacci heap: statements

This file states what a single-source shortest-path program on the word RAM must satisfy to achieve the Fredman–Tarjan running-time bound of Dijkstra's algorithm with a Fibonacci heap Dijkstra Fredman and Tarjan Cormen et al., Chapter 19 and Section 24.3.

Because memory past the input starts at 0, the priority-queue and distance arrays require only O(1) fresh initialization, and the algorithm extracts at most min n (m + 1) reachable vertices from the source. We therefore state both:

• Cslib.Algorithms.WordRAM.Dijkstra.FibonacciSpec: the sharper reachable-vertex bound steps + 1 ≤ K (m + min(n, m + 1) (⌊log₂ n⌋ + 1));
• Cslib.Algorithms.WordRAM.Dijkstra.FibonacciLinearSpec and Cslib.Algorithms.WordRAM.Dijkstra.FibonacciStatement: the textbook bound steps + 1 ≤ K (m + n (⌊log₂ n⌋ + 1)), derived immediately from FibonacciSpec.

Both bounds use the exact same word-size hypothesis Fits w (8 * (G.n + G.m + 2) * (G.maxWeight + 2)) as Cslib.Algorithms.WordRAM.Dijkstra.LogLinearSpec.

Main definitions

• Cslib.Algorithms.WordRAM.Dijkstra.FibonacciSpec: a flat program computes every distance from the source within K (m + min(n, m + 1) (⌊log₂ n⌋ + 1)) instructions.
• Cslib.Algorithms.WordRAM.Dijkstra.FibonacciLinearSpec: textbook K (m + n (⌊log₂ n⌋ + 1)) program specification.
• Cslib.Algorithms.WordRAM.Dijkstra.FibonacciSpecStatement: some program meets FibonacciSpec.
• Cslib.Algorithms.WordRAM.Dijkstra.FibonacciStatement: some program meets FibonacciLinearSpec.

Main results

• Cslib.Algorithms.WordRAM.Dijkstra.FibonacciSpec.toLinearSpec: FibonacciSpec implies FibonacciLinearSpec with the same constant K.

References

• E. W. Dijkstra, A note on two problems in connexion with graphs
• M. L. Fredman and R. E. Tarjan, Fibonacci heaps and their uses in improved network optimization algorithms, Section 4 (pp. 609–610).
• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms, Section 24.3 (p. 662).

def Cslib.Algorithms.WordRAM.Dijkstra.FibonacciSpec {r : ℕ} (p : WordRAM.Program WordRAM.Basis.exact r) (K : ℕ) : Prop

Shortest paths in O(m + min(n, m + 1) (⌊log₂ n⌋ + 1)) time. At every word size w that holds 8 (n + m + 2) (W + 2), where m is the number of edges and W the largest weight, the flat program p, started on the input words of an adjacency-list instance, halts within K (m + min(n, m + 1) (⌊log₂ n⌋ + 1)) instructions, the final halt included, and its memory then holds at G.outAddr v the encoded distance from the source to v, for every vertex v.

def Cslib.Algorithms.WordRAM.Dijkstra.FibonacciLinearSpec {r : ℕ} (p : WordRAM.Program WordRAM.Basis.exact r) (K : ℕ) : Prop

Shortest paths in O(m + n (⌊log₂ n⌋ + 1)) time. Textbook Fredman–Tarjan running-time specification for a flat word-RAM program p over the exact basis.

theorem Cslib.Algorithms.WordRAM.Dijkstra.FibonacciSpec.toLinearSpec {r K : ℕ} {p : WordRAM.Program WordRAM.Basis.exact r} (h : FibonacciSpec p K) : FibonacciLinearSpec p K

The sharper reachable-vertex specification FibonacciSpec implies the textbook specification FibonacciLinearSpec with the same constant K.

def Cslib.Algorithms.WordRAM.Dijkstra.FibonacciSpecStatement : Prop

Reachable-vertex Fibonacci-heap Dijkstra theorem (statement). Some word-RAM program over the exact basis meets FibonacciSpec.

def Cslib.Algorithms.WordRAM.Dijkstra.FibonacciStatement : Prop

Fibonacci-heap Dijkstra main theorem (statement). Some word-RAM program over the exact basis computes all shortest-path distances from the source of a weighted directed graph with n vertices and m edges, given by adjacency lists, within O(m + n (⌊log₂ n⌋ + 1)) instructions.