I would like to know about writing the Dijkstra Algorithm properly and efficiently using mathematical notation, which may simplify the process to writing the proof. Assume that the graph is unweighted, and there is no loop. Thanks.
Here is my attempt :
Let $G$ be the whole unweighted multigraph with no loop, $E_{G}$ and $N_{G}$ be the set of all edges and the set of all nodes of $G$ respectively, and $|N_{G}|=m$. Let $n_{0} \in N_{G}$ be the start node, we will search for all shortest paths from $n_{0}$ to all other nodes in $N_{G} - \{n_{0}\}$. Let $j \le m-1$ be a natural number and all nodes in $N_{G} - \{n_{0}\}$ that are connected to $n_{0}$ are labeled as $n_{i}, \: i =1,2,...,j$. Let $N_{c} = \{n_{0}, n_{1}, ..., n_{j} \}$.
Let $p_{n_{i}}^{t}, \: i = 1, 2,..., j$ be the path from $n_{0}$ to node $n_{i}$ after the $t_{th}$ iterations in Dijkstra algorithm. The Dijkstra Algorithm works as follows:
- Initially, let the paths $p_{n_{i}}^{0}$s be the longest paths.
- 1st iteration: Now let $N_{n_{0}}$ be the set of all neighbors of $n_{0}$. Let the neighbor nodes be $\{f_{11}, ..., f_{1 \alpha_{1}}\} \subseteq \{ n_{1}, ..., n_{j} \}$, $1 \le \alpha_{1} \le | N_{c} - \{ n_{0} \} |$. Let $e_{n_{0}}^{f_{11}}$ be an edge that connects $n_{0}$ and $f_{11}$. Now because $(e_{n_{0}}^{f_{11}})$ is a shorter path than the longest path $p_{f_{11}}^{0}$, we will set $p_{f_{11}}^{1} = (e_{n_{0}}^{f_{11}})$. By the same reasoning, we also set
$$p_{f_{12}}^{1} = (e_{n_{0}}^{f_{12}})$$ $$...$$ $$p_{f_{1 \alpha_{1}}}^{1} = (e_{n_{0}}^{f_{1 \alpha_{1}}})$$ The remaining $p_{n_{i}}^{1}$s will be equal to the previous paths (not updated, $p_{n_{i}}^{1} = p_{n_{i}}^{0} $) which is longest path. Now let $X_{1} = \{n_{0}\}$ be the set of all \textit{visited} nodes after the 1st iteration. - 2nd iteration: Now note the unvisited neighbor nodes of each node in $N_{n_{0}}$ (each neighbor must be in $N_{c} - X_{1}$). The sets of neighbors are $N_{f_{11}}, N_{f_{12}}, ... , N_{f_{1 (\alpha_{1}-1)}}, N_{f_{1 \alpha_{1}}}$. Let the neighbor nodes be denoted as:
$$N_{f_{11}} = \{f_{21}, ..., f_{2 \alpha_{2}}\} \subseteq \{ n_{1}, ..., n_{j} \}$$
$$N_{f_{12}} = \{f_{31}, ..., f_{3 \alpha_{3}}\} \subseteq \{ n_{1}, ..., n_{j} \}$$
$$...$$
$$N_{f_{1 \alpha_{1}}} = \{f_{(\alpha_{1}+1)1}, ..., f_{(\alpha_{1}+1) \alpha_{\alpha_{1}+1}}\} \subseteq \{ n_{1}, ..., n_{j} \}$$ Now we can set/update the paths:
- For neighbors of $f_{11}$ ($N_{f_{11}}$): Let $e_{f_{11}}^{f_{21}}$ be an edge that connects $f_{11}$ and $f_{21}$. Now check whether or not the path $(e_{n_{0}}^{f_{11}}, e_{f_{11}}^{f_{21}})$ is shorter than the path $p_{f_{21}}^{1}$. If it is, then $p_{f_{21}}^{2} = (e_{n_{0}}^{f_{11}}, e_{f_{11}}^{f_{21}})$. But if not, then $p_{f_{21}}^{2} =p_{f_{21}}^{1}$. Do the same process for $p_{f_{22}}^{2}, ... , p_{f_{2 \alpha_{2}}}^{2}$.
- Do the same process for the neighbors of $f_{12}, ..., f_{1 \alpha_{1}}$.
- For $ \forall x \in N_{c} - (N_{f_{11}} \cup ... \cup N_{f_{1 \alpha_{1}}}) $, the remaining $p_{x}^{2}$s will be equal to the previous paths (not updated, $p_{x}^{2} = p_{x}^{1} $)
- Now let $X_{2} = X_{1} \cup \{ f_{11}, ..., f_{1 \alpha_{1}} \}$ be the set of all visited nodes after the 2nd iteration.
- Next iterations: Same process as the 2nd iteration, but we have to consider the neighbor nodes of each node in the set $N_{f_{11}} \cup ... \cup N_{f_{1 \alpha_{1}}})$ (each neighbor must be in $N_{c} - X_{2}$). Repeat this process until we arrive in the $i_{th}$ iteration in which the set of all visited nodes $X_{i}$ equals to $N_{c}$. The paths $p_{n_{1}}^{i}, ..., p_{n_{j}}^{i}$ are the shortest paths.
Doing a something search for "dijkstra algorithm proof" brings up a lot of result, in particular this Stack Exchange question and this webpage, which both have short, concise proofs. The former uses induction, and the latter contradiction. (I haven't read them carefully; they may be in essence the same.)