The Underlying Principle of Dijkstra's Shortest Path Algorithm

Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

The Underlying Principle of Dijkstra's Shortest Path Algorithm

Jing-Chao Chen: Donghua University, Shanghai
Yatsuka Nakamura: Shinshu University, Nagano

Summary.

A path from a source vertex $v$ to a target vertex $u$ is said to be a shortest path if its total cost is minimum among all $v$-to-$u$ paths. Dijkstra's algorithm is a classic shortest path algorithm, which is described in many textbooks. To justify its correctness (whose rigorous proof will be given in the next article), it is necessary to clarify its underlying principle. For this purpose, the article justifies the following basic facts, which are the core of Dijkstra's algorithm. \begin{itemize} \itemsep-3pt \item A graph is given, its vertex set is denoted by $V.$ Assume $U$ is the subset of $V,$ and if a path $p$ from $s$ to $t$ is the shortest among the set of paths, each of which passes through only the vertices in $U,$ except the source and sink, and its source and sink is $s$ and in $V,$ respectively, then $p$ is a shortest path from $s$ to $t$ in the graph, and for any subgraph which contains at least $U,$ it is also the shortest. \item Let $p(s,x,U)$ denote the shortest path from $s$ to $x$ in a subgraph whose the vertex set is the union of $\{s,x\}$ and $U,$ and cost $(p)$ denote the cost of path $p(s,x,U),$ cost$(x,y)$ the cost of the edge from $x$ to $y.$ Give $p(s,x,U),$ $q(s,y,U)$ and $r(s,y,U \cup \{x\})$. If ${\rm cost}(p) = {\rm min} \{{\rm cost}(w): w(s,t,U) \wedge t \in V\}$, then we have $${\rm cost}(r) = {\rm min} ({\rm cost}(p)+{\rm cost}(x,y),{\rm cost}(q)).$$ \end{itemize} \noindent This is the well-known triangle comparison of Dijkstra's algorithm.

MML Identifier: GRAPH_5

The terminology and notation used in this paper have been introduced in the following articles [13] [16] [14] [17] [4] [3] [6] [15] [1] [8] [9] [2] [10] [5] [12] [7] [11]