A formalization of the Dijkstra's algorithm

dijkstra-formalism.md

Formalization of Dijkstra's Path finder

Natural English Definition:

Overview: The formal definition describes how to compute the shortest path between two vertices in a graph using a systematic approach. It formalizes the idea of Dijkstra's algorithm, where each vertex is processed step-by-step, and distances are updated to find the shortest path from a starting vertex to a terminal vertex.

Graph Representation: The graph consists of a set of vertices (𝑉) and edges (𝐸). Each edge has a weight that represents the distance between two connected vertices. These distances are stored in a matrix (𝑀), where the value at position $$𝑚_𝑖𝑗$$ represents the distance from vertex 𝑖 to vertex 𝑗.

The Shortest Path Problem: Given: A starting vertex (s). A terminal vertex (e). The task is to find the shortest path from (s) to (e), which is the sequence of vertices and edges with the smallest total weight. Components of the Approach: Position-Dependent Sequence ( Ψ Ψ): This structure stores information about each vertex, including its current shortest distance from the starting vertex and whether it has been fully processed. Each vertex has three associated values: 𝑣 v: the vertex itself. 𝑝 p: the shortest known distance to 𝑣 v. 𝜁 ζ: a marker indicating whether the vertex has been processed. Algorithm Steps: Initialization (Algorithm-I):

Start by initializing the distance of all vertices to infinity ( ∞ ∞) except the starting vertex ( 𝑠 s), which is set to 0. Mark all vertices as unprocessed ( 𝜁

0 ζ=0). This step prepares the structure ( Ψ Ψ) to hold the initial state of the graph. Selecting the Next Vertex (Algorithm-II):

Among all unprocessed vertices, find the one with the smallest distance from the starting vertex ( 𝑝 p). If this vertex is the terminal vertex ( 𝑒 e), the algorithm terminates because the shortest path has been determined. Otherwise, mark the selected vertex as processed ( 𝜁

1 ζ=1). Updating Distances (Algorithm-III):

For the selected vertex, examine all its neighboring vertices. Calculate the potential new distance to each neighbor as the sum of the selected vertex’s current distance ( 𝑝 p) and the weight of the edge connecting the two vertices ( 𝑚 𝑖 𝑗 m ij ​ ). If this new distance is smaller than the previously known distance to the neighbor, update the neighbor's distance in the structure ( Ψ Ψ). Key Details: The algorithm ensures that each vertex’s shortest path is finalized before moving to the next vertex. This is why the vertex with the smallest distance is always selected. Once a vertex is processed, its distance value ( 𝑝 p) is guaranteed to be the shortest possible distance from the starting vertex ( 𝑠 s). Termination: The process continues until either: The terminal vertex ( 𝑒 e) is reached, meaning the shortest path has been found. All vertices are processed, ensuring that every vertex’s shortest path from 𝑠 s is calculated. Why This Works: The algorithm's logic relies on iteratively exploring the shortest known paths to unprocessed vertices and updating neighbors' distances if a shorter path is discovered. This guarantees that the shortest path to any vertex is finalized before moving forward, which is the foundation of Dijkstra's algorithm.

In summary, this formal definition is a precise mathematical representation of Dijkstra’s algorithm, broken into three key steps: initializing distances, selecting the next vertex to process, and updating the distances of its neighbors. It carefully tracks the state of each vertex using a sequence ( Ψ Ψ), ensuring that the algorithm proceeds in an organized and efficient manner to find the shortest path.

Formal Definition:

Let $$G(V, E)$$ be a graph composed of a set of vertices $$V$$ of cardinality $$n_v$$ and a set of edges $$E$$ of cardinality $$n_e$$; $$M$$ be an adjacency-cellular matrix of cardinality $$n_v \times n_v$$; in which the entries of the matrix $$M_{n_v \times n_v}$$ are $$m_{ij}$$ holding the weight of the transition among vertices $$i$$ and $$j$$; where $$i,\ j \in V$$. The weight of the transition is the distance covered between the two vertices.

If vertex $$s \in V$$ is specified as the initial vertex, and vertex $$e \in V$$ is specified as the terminal vertex; a shortest path can exist in which $$P = \{s,..., e\}$$; where $$P \subseteq V$$; such that the following predicates are met:

• Let $$\Psi$$ be a position-dependent sequence structure that stores the vertices of $$V$$ in a lesser position order calculated from the initial vertex $$s$$; such that $$\psi = \{v, p, \zeta\}$$.
• Algorithm-I (Initialize the position-dependent sequence with the distances from the initial vertex $$s$$): If $$s$$ is selected from $$V$$ as the starting vertex, then $$\Psi = ( \psi: \psi = \{v, p, \zeta\} \land v \in V \land p = \infty \land (\zeta = 0) \land ((v = s) \implies p = 0))$$; where $$\zeta$$ is a predicate holding Zero if the structure is not selected before by algorithm-II, and One if the structure is selected before as a result of applying algorithm-II.
• Algorithm-II (Pull Lesser Distant Vertex): Let $$p_{lesser}$$ be the lesser distance from the initial vertex $$s$$; then the selected lesser distance structure would be $$\psi_{lesser} = \{v, \rho, \zeta | \rho = p_{lesser} \land (\zeta = 0)\}$$. If $$\psi_{lesser} = \{v, \rho, \zeta | \rho = p_{lesser} \land (\zeta = 0) \land (v = e) \land e\ is\ the\ end\ vertex \}$$; then terminate the algorithm; after the selection is made, $$\zeta$$ is switched to $$1$$.
• Algorithm-III (Update the position-dependent sequence with new positions):
  • Recall, $$\psi_{lesser}$$ is a structure in the sequence $$\Psi$$ holding the lesser positioned vertex from the source vertex $$s$$, the $$\rho$$ value;
  • Recall $$m_{ij}$$; where $$i$$ is the index of the vertex selected from $$\psi_{lesser}$$, and $$j$$ is the index of the vertex reachable from $$i$$, the entry of the adjacency matrix is the distance $$i \rightarrow j$$; therefore $$\rho + m_{ij}$$ represents the total distance from the source vertex $$s$$; as $$\rho$$ is an incremental value; hence if the predicate $$\rho + m_{ij} < \psi_{j}$$ is true; then update the $$\psi_{j}$$ as $$\psi_{j} = \rho + m_{ij}$$. Hence, $$(\ (\rho + m_{ij} < \psi_{j}) \implies (\psi_{j} = \rho + m_{ij})\ )$$.

Pseudo-code:

GNU/C99 Code: