Dijkstra's Algorithm with a Fibonacci Heap in O(m + n (⌊log₂ n⌋ + 1)) Time

This file instantiates the black-box outer Dijkstra algorithm (Cslib.Algorithms.WordRAM.Dijkstra.dijkstraCode_exec and Cslib.Algorithms.WordRAM.Dijkstra.dijkstra_of_pq_spec) with the standalone static-array Fibonacci heap package (Cslib.Algorithms.WordRAM.PriorityQueue.FibonacciHeap.pkg) to obtain both the sharper reachable-vertex bound Cslib.Algorithms.WordRAM.Dijkstra.FibonacciSpec (O(m + min(n, m + 1) (⌊log₂ n⌋ + 1))) and the textbook Fredman–Tarjan bound Cslib.Algorithms.WordRAM.Dijkstra.FibonacciStatement (O(m + n (⌊log₂ n⌋ + 1))).

Main definitions

• Cslib.Algorithms.WordRAM.Dijkstra.fibDijkstra: structured exact-basis Dijkstra program instantiated with PriorityQueue.FibonacciHeap.code.

Main results

• Cslib.Algorithms.WordRAM.Dijkstra.fibDijkstra_spec: structured execution bound 640 * (m + min(n, m + 1) * (⌊log₂ n⌋ + 1)).
• Cslib.Algorithms.WordRAM.Dijkstra.fibonacciSpec: compiled flat-program reachable-vertex specification FibonacciSpec (fibDijkstra.program OuterReg.zero) 640.
• Cslib.Algorithms.WordRAM.Dijkstra.fibonacciLinearSpec: compiled flat-program textbook specification FibonacciLinearSpec (fibDijkstra.program OuterReg.zero) 640.
• Cslib.Algorithms.WordRAM.Dijkstra.fibonacciSpecStatement: existential reachable-vertex theorem.
• Cslib.Algorithms.WordRAM.Dijkstra.fibonacciStatement: textbook O(m + n log n) main theorem.

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).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Dijkstra.fibDijkstra : WordRAM.Code WordRAM.Basis.exact (15 + PriorityQueue.FibonacciHeap.rFib)

Structured exact-basis Dijkstra program instantiated with the standalone Fibonacci heap.

theorem Cslib.Algorithms.WordRAM.Dijkstra.fibDijkstra_spec {G : ListInstance} {w : ℕ} (hw : WordRAM.Fits w (8 * (G.n + G.m + 2) * (G.maxWeight + 2))) : ∃ (y : WordRAM.Data (15 + PriorityQueue.FibonacciHeap.rFib)), WordRAM.ExecWithin w fibDijkstra (WordRAM.Data.init G.encode) y (640 * (G.m + min G.n (G.m + 1) * (Nat.log 2 G.n + 1))) ∧ ∀ (v : Fin G.n), y.mem (G.outAddr v) = encodeDist (G.dist G.source v)

Correctness and running time of structured Dijkstra with a Fibonacci heap.

theorem Cslib.Algorithms.WordRAM.Dijkstra.fibonacciSpec : FibonacciSpec (fibDijkstra.program OuterReg.zero) 640

Dijkstra's algorithm with a Fibonacci heap in O(m + min(n, m + 1) (⌊log₂ n⌋ + 1)) time. The compiled flat program meets Cslib.Algorithms.WordRAM.Dijkstra.FibonacciSpec with K = 640.

theorem Cslib.Algorithms.WordRAM.Dijkstra.fibonacciLinearSpec : FibonacciLinearSpec (fibDijkstra.program OuterReg.zero) 640

Dijkstra's algorithm with a Fibonacci heap in O(m + n (⌊log₂ n⌋ + 1)) time. The compiled flat program meets Cslib.Algorithms.WordRAM.Dijkstra.FibonacciLinearSpec with K = 640.

theorem Cslib.Algorithms.WordRAM.Dijkstra.fibonacciSpecStatement : FibonacciSpecStatement

Reachable-vertex Fibonacci-heap Dijkstra theorem.

theorem Cslib.Algorithms.WordRAM.Dijkstra.fibonacciStatement : FibonacciStatement

Fibonacci-heap Dijkstra main theorem. 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.