Shortest paths in directed acyclic graphs

StructureCost of the DAG shortest-path pass#✓fully proved

The cost of the one-pass relaxation in topological order consists of three natural-number counters: the number of vertices taken from the order, the number of edge occurrences checked for relaxation, and the number of distance installations (strict improvements or first finite distances).

Preparation and topological sorting are not counted.

public structure Cost where
  /-- Vertices taken from the certified order. -/
  vertexVisits : Nat
  /-- Original weighted edge occurrences checked for relaxation. -/
  edgeRelaxations : Nat
  /-- Strict improvements or first finite distances installed. -/
  distanceUpdates : Nat
  deriving DecidableEq, Repr

Used by 23

Used byShortest paths in a DAG with a topology check · Unreachable vertices are exactly those at infinite DAG distance · DAG shortest-path distances are shortest-path weights · Failure output of DAG shortest paths · Successful output of DAG shortest paths · A failed DAG shortest-path run exhibits a cycle · Extracted DAG shortest paths are shortest paths · The DAG shortest-path algorithm succeeds exactly on acyclic graphs · One-pass DAG shortest-path relaxation · Infinite DAG distances are exactly unreachable vertices · Finite DAG distances are at most every path weight · Finite DAG distances are path weights · Distance updates are bounded by edge relaxations · Edge relaxation count of the DAG pass · Finite non-source vertices have predecessors · Unreached vertices have no DAG shortest-path predecessor · Predecessor extraction fails exactly at infinite distances · Paths extracted after topological relaxation are shortest paths · Predecessor edges of the DAG shortest-path pass · The DAG shortest-path pass keeps its source · The DAG shortest-path pass gives the source distance zero · The source has no DAG shortest-path predecessor · The DAG shortest-path pass is charged one vertex visit per vertex

DefinitionOne-pass DAG shortest-path relaxation#✓fully proved

Let \(E\) be a list of integer-weighted directed edge occurrences on the vertices \(\{0, \dots, n-1\}\), let \(s\) be a source vertex, and let \(\sigma\) be a topological order of the directed graph obtained from \(E\) by forgetting weights. The relaxation starts from distance estimate \(0\) at \(s\), infinite estimates at every other vertex and no predecessor edges. It then takes the vertices \(u\) of \(\sigma\) in turn and relaxes each occurrence \(e\) in \(E\) from \(u\) to some \(v\) with weight \(c\), in the order of \(E\): if the estimate \(d\) at \(u\) is finite and the estimate at \(v\) is infinite or greater than \(d + c\), it sets the estimate at \(v\) to \(d + c\) and the predecessor of \(v\) to \(e\). The result records \(s\) as its source together with the final estimates and predecessors. Its cost counts one vertex visit per vertex of \(\sigma\), one edge relaxation per occurrence relaxed, and one distance update per estimate set.

The original edge occurrences are retained, so every parallel occurrence is checked. The proof that \(\sigma\) is a topological order is not used by the computation.

public def run {n : Nat} (edges : List (Edge n)) (source : Fin n) (order : List (Fin n))
    (_horder : TopologicalSort.IsTopologicalOrder (toDirectedAdjacency edges) order) :
    TimeM Cost (Distances n) :=
  let buckets := bucketize edges
  pass (fun vertex => buckets.get vertex) order (initialState source)

Uses 5 · Used by 19

Statement usesBellman-Ford distance table · Weighted directed edge · Weight-forgetting directed graph · Cost of the DAG shortest-path pass · Topological order

Used byUnreachable vertices are exactly those at infinite DAG distance · DAG shortest-path distances are shortest-path weights · Successful output of DAG shortest paths · Extracted DAG shortest paths are shortest paths · The DAG shortest-path algorithm succeeds exactly on acyclic graphs · Infinite DAG distances are exactly unreachable vertices · Finite DAG distances are at most every path weight · Finite DAG distances are path weights · Distance updates are bounded by edge relaxations · Edge relaxation count of the DAG pass · Finite non-source vertices have predecessors · Unreached vertices have no DAG shortest-path predecessor · Predecessor extraction fails exactly at infinite distances · Paths extracted after topological relaxation are shortest paths · Predecessor edges of the DAG shortest-path pass · The DAG shortest-path pass keeps its source · The DAG shortest-path pass gives the source distance zero · The source has no DAG shortest-path predecessor · The DAG shortest-path pass is charged one vertex visit per vertex

DefinitionShortest paths in a DAG with a topology check#✓fully proved

Given a list \(E\) of integer-weighted edges on the vertices \(0, \dots, n-1\) and a source \(s\), run Kahn's topological sort on the directed graph obtained from \(E\) by forgetting weights. If it succeeds with order \(\sigma\), start from distance \(0\) at \(s\) and \(\infty\) elsewhere, relax the outgoing edge occurrences of each vertex in the order \(\sigma\), and return the resulting distances and predecessor edges. If it fails after processing the list \(P\) of vertices and leaving the list \(R\), return the error \((P, R)\). Only the relaxation pass is charged in the recorded cost.

Failure preserves the sorter's processed and remaining lists; it does not return a cycle list.

public def dagShortestPaths {n : Nat} (edges : List (Edge n)) (source : Fin n) :
    TimeM Cost (Except (List (Fin n) × List (Fin n)) (Distances n)) :=
  let buckets := bucketize edges
  match TopologicalSort.sort (bucketGraph buckets) with
  | .success order => do
      let result ← pass (fun vertex => buckets.get vertex) order (initialState source)
      pure (.ok result)
  | .failure processed remaining => pure (.error (processed, remaining))

Uses 6 · Used by 7

Statement usesBellman-Ford distance table · Weighted directed edge · Cost of the DAG shortest-path pass · Directed adjacency graph · Outcome of Kahn's topological sort · Kahn's topological sort

Used byUnreachable vertices are exactly those at infinite DAG distance · DAG shortest-path distances are shortest-path weights · Failure output of DAG shortest paths · Successful output of DAG shortest paths · A failed DAG shortest-path run exhibits a cycle · Extracted DAG shortest paths are shortest paths · The DAG shortest-path algorithm succeeds exactly on acyclic graphs

TheoremThe DAG shortest-path pass is charged one vertex visit per vertex#✓fully proved

Let \(E\) be a list of integer-weighted directed edge occurrences on the vertices \(\{0, \dots, n-1\}\), let \(s\) be a source vertex, and let \(\sigma\) be a topological order of the directed graph obtained from \(E\) by forgetting weights. The one-pass DAG shortest-path relaxation of \(E\) from \(s\) in the order \(\sigma\) is charged exactly \(n\) vertex visits.

public theorem run_vertexVisits {n : Nat} (edges : List (Edge n)) (source : Fin n)
    (order : List (Fin n))
    (horder : TopologicalSort.IsTopologicalOrder (toDirectedAdjacency edges) order) :
    (run edges source order horder).time.vertexVisits = n

Uses 8

Statement usesBellman-Ford distance table · Weighted directed edge · Weight-forgetting directed graph · Cost of the DAG shortest-path pass · One-pass DAG shortest-path relaxation · Topological order

Proof usesDirected adjacency graph · Edge of a directed adjacency graph

TheoremEdge relaxation count of the DAG pass#✓fully proved

Let \(E\) be a list of integer-weighted edges on \(n\) vertices, \(s\) a source, and \(\sigma\) a topological order of the directed graph obtained from \(E\) by forgetting weights. In the cost of the one-pass relaxation from \(s\) in the order \(\sigma\), the number of edge relaxations equals the length of \(E\), with identical duplicate edges counted separately.

public theorem run_edgeRelaxations {n : Nat} (edges : List (Edge n)) (source : Fin n)
    (order : List (Fin n))
    (horder : TopologicalSort.IsTopologicalOrder (toDirectedAdjacency edges) order) :
    (run edges source order horder).time.edgeRelaxations = edges.length

Uses 8

Statement usesBellman-Ford distance table · Weighted directed edge · Weight-forgetting directed graph · Cost of the DAG shortest-path pass · One-pass DAG shortest-path relaxation · Topological order

Proof usesDirected adjacency graph · Edge of a directed adjacency graph

TheoremDistance updates are bounded by edge relaxations#✓fully proved

Let \(E\) be a list of integer-weighted edges on \(n\) vertices, \(s\) a source, and \(\sigma\) a topological order of the directed graph obtained from \(E\) by forgetting weights. In the cost of the one-pass relaxation from \(s\) in the order \(\sigma\), the number of distance installations is at most the number of edge relaxations.

Only actual strict improvements or first finite estimates install a predecessor.

public theorem run_distanceUpdates_le {n : Nat} (edges : List (Edge n)) (source : Fin n)
    (order : List (Fin n))
    (horder : TopologicalSort.IsTopologicalOrder (toDirectedAdjacency edges) order) :
    (run edges source order horder).time.distanceUpdates ≤
      (run edges source order horder).time.edgeRelaxations

Uses 6

Statement usesBellman-Ford distance table · Weighted directed edge · Weight-forgetting directed graph · Cost of the DAG shortest-path pass · One-pass DAG shortest-path relaxation · Topological order

TheoremFinite DAG distances are path weights#✓fully proved

Let \(E\) be a list of integer-weighted edges on \(n\) vertices, \(s\) a source, and \(\sigma\) a topological order of the directed graph obtained from \(E\) by forgetting weights. If the one-pass relaxation from \(s\) in the order \(\sigma\) gives a vertex \(t\) the finite distance \(d\), then there is a path from \(s\) to \(t\) made of edge occurrences of \(E\) whose edge weights sum to \(d\).

public theorem run_distance_realized {n : Nat} (edges : List (Edge n)) (source : Fin n)
    (order : List (Fin n))
    (horder : TopologicalSort.IsTopologicalOrder (toDirectedAdjacency edges) order)
    (target : Fin n) (value : Int)
    (hd : (run edges source order horder).ret.distance.get target = some value) :
    ∃ path, IsWeightedPath edges source target path ∧ pathWeight path = value

Uses 10 · Used by 2

Statement usesBellman-Ford distance table · Weighted directed edge · Weighted path in an edge list · Bellman–Ford path weight · Weight-forgetting directed graph · Cost of the DAG shortest-path pass · One-pass DAG shortest-path relaxation · Topological order

Proof usesAppending an edge to a weighted path · Weight of a path with an edge appended

Used byDAG shortest-path distances are shortest-path weights · Infinite DAG distances are exactly unreachable vertices

TheoremThe DAG shortest-path pass keeps its source#✓fully proved

Let \(E\) be a list of integer-weighted directed edge occurrences on the vertices \(\{0, \dots, n-1\}\), let \(s\) be a source vertex, and let \(\sigma\) be a topological order of the directed graph obtained from \(E\) by forgetting weights. The result of the one-pass DAG shortest-path relaxation of \(E\) from \(s\) in the order \(\sigma\) records \(s\) as its source.

public theorem run_source {n : Nat} (edges : List (Edge n)) (source : Fin n)
    (order : List (Fin n))
    (horder : TopologicalSort.IsTopologicalOrder (toDirectedAdjacency edges) order) :
    (run edges source order horder).ret.source = source

Uses 15 · Used by 2

Statement usesBellman-Ford distance table · Weighted directed edge · Weight-forgetting directed graph · Cost of the DAG shortest-path pass · One-pass DAG shortest-path relaxation · Topological order

Proof usesWeighted path in an edge list · Edges of the weight-forgetting graph · Appending an edge to a weighted path · Weighted paths give walks of the same length · Bellman–Ford path weight · Weight of a path with an edge appended · Directed adjacency graph · Edge of a directed adjacency graph · Walks of a given length

Used byPredecessor extraction fails exactly at infinite distances · Paths extracted after topological relaxation are shortest paths

TheoremThe DAG shortest-path pass gives the source distance zero#✓fully proved

Let \(E\) be a list of integer-weighted directed edge occurrences on the vertices \(\{0, \dots, n-1\}\), let \(s\) be a source vertex, and let \(\sigma\) be a topological order of the directed graph obtained from \(E\) by forgetting weights. The one-pass DAG shortest-path relaxation of \(E\) from \(s\) in the order \(\sigma\) ends with distance estimate \(0\) at \(s\).

This holds even when edges of negative weight enter \(s\).

public theorem run_source_distance {n : Nat} (edges : List (Edge n)) (source : Fin n)
    (order : List (Fin n))
    (horder : TopologicalSort.IsTopologicalOrder (toDirectedAdjacency edges) order) :
    (run edges source order horder).ret.distance.get source = some 0

Uses 15 · Used by 4

Statement usesBellman-Ford distance table · Weighted directed edge · Weight-forgetting directed graph · Cost of the DAG shortest-path pass · One-pass DAG shortest-path relaxation · Topological order

Proof usesWeighted path in an edge list · Edges of the weight-forgetting graph · Appending an edge to a weighted path · Weighted paths give walks of the same length · Bellman–Ford path weight · Weight of a path with an edge appended · Directed adjacency graph · Edge of a directed adjacency graph · Walks of a given length

Used byInfinite DAG distances are exactly unreachable vertices · Finite DAG distances are at most every path weight · Predecessor extraction fails exactly at infinite distances · Paths extracted after topological relaxation are shortest paths

TheoremThe source has no DAG shortest-path predecessor#✓fully proved

Let \(E\) be a list of integer-weighted directed edge occurrences on the vertices \(\{0, \dots, n-1\}\), let \(s\) be a source vertex, and let \(\sigma\) be a topological order of the directed graph obtained from \(E\) by forgetting weights. The one-pass DAG shortest-path relaxation of \(E\) from \(s\) in the order \(\sigma\) records no predecessor edge for \(s\).

public theorem run_source_predecessor {n : Nat} (edges : List (Edge n)) (source : Fin n)
    (order : List (Fin n))
    (horder : TopologicalSort.IsTopologicalOrder (toDirectedAdjacency edges) order) :
    (run edges source order horder).ret.predecessor.get source = none

Uses 15

Statement usesBellman-Ford distance table · Weighted directed edge · Weight-forgetting directed graph · Cost of the DAG shortest-path pass · One-pass DAG shortest-path relaxation · Topological order

Proof usesWeighted path in an edge list · Edges of the weight-forgetting graph · Appending an edge to a weighted path · Weighted paths give walks of the same length · Bellman–Ford path weight · Weight of a path with an edge appended · Directed adjacency graph · Edge of a directed adjacency graph · Walks of a given length

TheoremFinite DAG distances are at most every path weight#✓fully proved

Let \(E\) be a list of integer-weighted edges on \(n\) vertices, \(s\) a source, and \(\sigma\) a topological order of the directed graph obtained from \(E\) by forgetting weights. If the one-pass relaxation from \(s\) in the order \(\sigma\) gives a vertex \(t\) the finite distance \(d\), then \(d \le w(p)\) for every path \(p\) from \(s\) to \(t\) made of edge occurrences of \(E\), where \(w(p)\) is the sum of the weights of the edges of \(p\).

public theorem run_distance_minimal {n : Nat} (edges : List (Edge n)) (source : Fin n)
    (order : List (Fin n))
    (horder : TopologicalSort.IsTopologicalOrder (toDirectedAdjacency edges) order)
    (target : Fin n) (value : Int)
    (hd : (run edges source order horder).ret.distance.get target = some value)
    (path : List (Edge n)) (hp : IsWeightedPath edges source target path) :
    value ≤ pathWeight path

Uses 17 · Used by 2

Statement usesBellman-Ford distance table · Weighted directed edge · Weighted path in an edge list · Bellman–Ford path weight · Weight-forgetting directed graph · Cost of the DAG shortest-path pass · One-pass DAG shortest-path relaxation · Topological order

Proof usesEdges of the weight-forgetting graph · Appending an edge to a weighted path · Tail of a weighted path · Weighted paths give walks of the same length · Weight of a path with an edge appended · The DAG shortest-path pass gives the source distance zero · Directed adjacency graph · Edge of a directed adjacency graph · Walks of a given length

Used byDAG shortest-path distances are shortest-path weights · Paths extracted after topological relaxation are shortest paths

TheoremInfinite DAG distances are exactly unreachable vertices#✓fully proved

Let \(E\) be a list of integer-weighted edges on \(n\) vertices, \(s\) a source, and \(\sigma\) a topological order of the directed graph \(G\) obtained from \(E\) by forgetting weights. For every vertex \(t\), the one-pass relaxation from \(s\) in the order \(\sigma\) leaves the distance of \(t\) infinite if and only if \(t\) is not reachable from \(s\) in \(G\).

public theorem run_distance_eq_none_iff {n : Nat} (edges : List (Edge n)) (source : Fin n)
    (order : List (Fin n))
    (horder : TopologicalSort.IsTopologicalOrder (toDirectedAdjacency edges) order)
    (target : Fin n) :
    (run edges source order horder).ret.distance.get target = none ↔
      ¬(toDirectedAdjacency edges).Reachable source target

Uses 20 · Used by 1

Statement usesBellman-Ford distance table · Weighted directed edge · Weight-forgetting directed graph · Cost of the DAG shortest-path pass · One-pass DAG shortest-path relaxation · Reachability in a directed graph · Topological order

Proof usesWeighted path in an edge list · Edges of the weight-forgetting graph · Appending an edge to a weighted path · Tail of a weighted path · Weighted paths give walks of the same length · Bellman–Ford path weight · Weight of a path with an edge appended · Reachability by weighted paths · Finite DAG distances are path weights · The DAG shortest-path pass gives the source distance zero · Directed adjacency graph · Edge of a directed adjacency graph · Walks of a given length

Used byUnreachable vertices are exactly those at infinite DAG distance

TheoremPredecessor edges of the DAG shortest-path pass#✓fully proved

Let \(E\) be a list of integer-weighted directed edge occurrences on the vertices \(\{0, \dots, n-1\}\), let \(s\) be a source vertex, and let \(\sigma\) be a topological order of the directed graph obtained from \(E\) by forgetting weights. Suppose the one-pass DAG shortest-path relaxation of \(E\) from \(s\) in the order \(\sigma\) records an edge occurrence \(e\) from \(u\) to \(w\) with weight \(c\) as the predecessor of a vertex \(v\). Then \(e\) occurs in \(E\), \(w = v\), and there is an integer \(d\) such that the final distance estimate at \(u\) is \(d\), the final distance estimate at \(v\) is \(d + c\), and the position of \(u\) in \(\sigma\) is less than the position of \(v\) in \(\sigma\).

public theorem run_predecessor_spec {n : Nat} (edges : List (Edge n)) (source : Fin n)
    (order : List (Fin n))
    (horder : TopologicalSort.IsTopologicalOrder (toDirectedAdjacency edges) order)
    (target : Fin n) (edge : Edge n)
    (hp : (run edges source order horder).ret.predecessor.get target = some edge) :
    edge ∈ edges ∧ edge.target = target ∧
      ∃ value, (run edges source order horder).ret.distance.get edge.source = some value ∧
        (run edges source order horder).ret.distance.get target = some (value + edge.weight) ∧
        order.idxOf edge.source < order.idxOf target

Uses 15 · Used by 2

Statement usesBellman-Ford distance table · Weighted directed edge · Weight-forgetting directed graph · Cost of the DAG shortest-path pass · One-pass DAG shortest-path relaxation · Topological order

Proof usesWeighted path in an edge list · Edges of the weight-forgetting graph · Appending an edge to a weighted path · Weighted paths give walks of the same length · Bellman–Ford path weight · Weight of a path with an edge appended · Directed adjacency graph · Edge of a directed adjacency graph · Walks of a given length

Used byPredecessor extraction fails exactly at infinite distances · Paths extracted after topological relaxation are shortest paths

TheoremUnreached vertices have no DAG shortest-path predecessor#✓fully proved

Let \(E\) be a list of integer-weighted directed edge occurrences on the vertices \(\{0, \dots, n-1\}\), let \(s\) be a source vertex, and let \(\sigma\) be a topological order of the directed graph obtained from \(E\) by forgetting weights. If the one-pass DAG shortest-path relaxation of \(E\) from \(s\) in the order \(\sigma\) ends with an infinite distance estimate at a vertex \(v\), then it records no predecessor edge for \(v\).

public theorem run_infinite_predecessor {n : Nat} (edges : List (Edge n)) (source : Fin n)
    (order : List (Fin n))
    (horder : TopologicalSort.IsTopologicalOrder (toDirectedAdjacency edges) order)
    (target : Fin n) (hd : (run edges source order horder).ret.distance.get target = none) :
    (run edges source order horder).ret.predecessor.get target = none

Uses 15 · Used by 2

Statement usesBellman-Ford distance table · Weighted directed edge · Weight-forgetting directed graph · Cost of the DAG shortest-path pass · One-pass DAG shortest-path relaxation · Topological order

Proof usesWeighted path in an edge list · Edges of the weight-forgetting graph · Appending an edge to a weighted path · Weighted paths give walks of the same length · Bellman–Ford path weight · Weight of a path with an edge appended · Directed adjacency graph · Edge of a directed adjacency graph · Walks of a given length

Used byPredecessor extraction fails exactly at infinite distances · Paths extracted after topological relaxation are shortest paths

TheoremFinite non-source vertices have predecessors#✓fully proved

Let \(E\) be a list of integer-weighted edges on \(n\) vertices, \(s\) a source, and \(\sigma\) a topological order of the directed graph obtained from \(E\) by forgetting weights. If the one-pass relaxation from \(s\) in the order \(\sigma\) gives a vertex \(t \ne s\) a finite distance, then it records a predecessor edge for \(t\).

public theorem run_finite_predecessor {n : Nat} (edges : List (Edge n)) (source : Fin n)
    (order : List (Fin n))
    (horder : TopologicalSort.IsTopologicalOrder (toDirectedAdjacency edges) order)
    (target : Fin n) (value : Int)
    (hd : (run edges source order horder).ret.distance.get target = some value)
    (hne : target ≠ source) : ∃ edge, (run edges source order horder).ret.predecessor.get target =
      some edge

Uses 15 · Used by 2

Statement usesBellman-Ford distance table · Weighted directed edge · Weight-forgetting directed graph · Cost of the DAG shortest-path pass · One-pass DAG shortest-path relaxation · Topological order

Proof usesWeighted path in an edge list · Edges of the weight-forgetting graph · Appending an edge to a weighted path · Weighted paths give walks of the same length · Bellman–Ford path weight · Weight of a path with an edge appended · Directed adjacency graph · Edge of a directed adjacency graph · Walks of a given length

Used byPredecessor extraction fails exactly at infinite distances · Paths extracted after topological relaxation are shortest paths

TheoremSuccessful output of DAG shortest paths#✓fully proved

For a list \(E\) of integer-weighted edges on \(n\) vertices, a source \(s\), and a distance record \(D\), the DAG shortest-path algorithm on \(E\) from \(s\) returns \(D\) if and only if there is a topological order \(\sigma\) of the directed graph obtained from \(E\) by forgetting weights such that Kahn's topological sort of that graph succeeds with \(\sigma\) and \(D\) is the result of the one-pass relaxation from \(s\) in the order \(\sigma\).

public theorem dagShortestPaths_eq_ok_iff {n : Nat} (edges : List (Edge n)) (source : Fin n)
    (result : Distances n) :
    (dagShortestPaths edges source).ret = .ok result ↔
      ∃ order, ∃ horder : TopologicalSort.IsTopologicalOrder (toDirectedAdjacency edges) order,
        TopologicalSort.sort (toDirectedAdjacency edges) = .success order ∧
        result = (run edges source order horder).ret

Uses 11 · Used by 4

Statement usesBellman-Ford distance table · Weighted directed edge · Weight-forgetting directed graph · Cost of the DAG shortest-path pass · Shortest paths in a DAG with a topology check · One-pass DAG shortest-path relaxation · Topological order · Outcome of Kahn's topological sort · Kahn's topological sort

Proof usesDirected adjacency graph · A successful topological sort is a topological order

Used byUnreachable vertices are exactly those at infinite DAG distance · DAG shortest-path distances are shortest-path weights · Extracted DAG shortest paths are shortest paths · The DAG shortest-path algorithm succeeds exactly on acyclic graphs

TheoremFailure output of DAG shortest paths#✓fully proved

For a list \(E\) of integer-weighted edges on \(n\) vertices, a source \(s\), and lists \(P\) and \(R\) of vertices, the DAG shortest-path algorithm on \(E\) from \(s\) returns the error \((P, R)\) if and only if Kahn's topological sort of the directed graph obtained from \(E\) by forgetting weights fails after processing \(P\) and leaving \(R\).

public theorem dagShortestPaths_eq_error_iff {n : Nat} (edges : List (Edge n)) (source : Fin n)
    (processed remaining : List (Fin n)) :
    (dagShortestPaths edges source).ret = .error (processed, remaining) ↔
      TopologicalSort.sort (toDirectedAdjacency edges) = .failure processed remaining

Uses 8 · Used by 1

Statement usesBellman-Ford distance table · Weighted directed edge · Weight-forgetting directed graph · Cost of the DAG shortest-path pass · Shortest paths in a DAG with a topology check · Outcome of Kahn's topological sort · Kahn's topological sort

Proof usesDirected adjacency graph

Used byA failed DAG shortest-path run exhibits a cycle

TheoremPredecessor extraction fails exactly at infinite distances#✓fully proved

Let \(E\) be a list of integer-weighted directed edges on the vertices \(\{0, \dots, n-1\}\), \(s\) a source vertex, and \(\sigma\) a topological order of the directed graph with an edge \(u \to v\) for each edge of \(E\) from \(u\) to \(v\). After the one-pass relaxation of \(E\) from \(s\) in the order \(\sigma\), for every vertex \(t\), following the predecessor edges back from \(t\) fails to reach \(s\) within \(n\) steps if and only if the computed distance to \(t\) is infinite.

public theorem run_pathTo?_eq_none_iff {n : Nat} (edges : List (Edge n)) (source : Fin n)
    (order : List (Fin n))
    (horder : TopologicalSort.IsTopologicalOrder (toDirectedAdjacency edges) order)
    (target : Fin n) :
    (run edges source order horder).ret.pathTo? target = none ↔
      (run edges source order horder).ret.distance.get target = none

Uses 17 · Used by 1

Statement usesBellman-Ford distance table · Bellman-Ford path reconstruction · Weighted directed edge · Weight-forgetting directed graph · Cost of the DAG shortest-path pass · One-pass DAG shortest-path relaxation · Topological order

Proof usesPredecessor paths realize the distances under a decreasing rank · Weighted path in an edge list · Bellman–Ford path weight · Finite non-source vertices have predecessors · Unreached vertices have no DAG shortest-path predecessor · Predecessor edges of the DAG shortest-path pass · The DAG shortest-path pass keeps its source · The DAG shortest-path pass gives the source distance zero · Directed adjacency graph · Edge of a directed adjacency graph

Used byPaths extracted after topological relaxation are shortest paths

TheoremPaths extracted after topological relaxation are shortest paths#✓fully proved

Let \(E\) be a list of integer-weighted directed edges on the vertices \(\{0, \dots, n-1\}\), \(s\) a source vertex, and \(\sigma\) a topological order of the directed graph with an edge \(u \to v\) for each edge of \(E\) from \(u\) to \(v\). After the one-pass relaxation of \(E\) from \(s\) in the order \(\sigma\), suppose following the predecessor edges back from a vertex \(t\) reaches \(s\) within \(n\) steps, giving the path \(P\). Then \(P\) is a path from \(s\) to \(t\) in \(E\), the computed distance to \(t\) is finite and equals the weight of \(P\), \(P\) has fewer than \(n\) edges, and every path from \(s\) to \(t\) in \(E\) has weight at least the weight of \(P\). Here a path from \(s\) to \(t\) in \(E\) is a list of edges of \(E\), each starting where the previous one ends, the first starting at \(s\) and the last ending at \(t\) (the empty list when \(t = s\)), and its weight is the sum of its edge weights.

public theorem run_pathTo?_spec {n : Nat} (edges : List (Edge n)) (source : Fin n)
    (order : List (Fin n))
    (horder : TopologicalSort.IsTopologicalOrder (toDirectedAdjacency edges) order)
    (target : Fin n) (path : List (Edge n))
    (hpath : (run edges source order horder).ret.pathTo? target = some path) :
    IsWeightedPath edges source target path ∧
      (run edges source order horder).ret.distance.get target = some (pathWeight path) ∧
      path.length < n ∧
      ∀ other, IsWeightedPath edges source target other → pathWeight path ≤ pathWeight other

Uses 19 · Used by 1

Statement usesBellman-Ford distance table · Bellman-Ford path reconstruction · Weighted directed edge · Weighted path in an edge list · Bellman–Ford path weight · Weight-forgetting directed graph · Cost of the DAG shortest-path pass · One-pass DAG shortest-path relaxation · Topological order

Proof usesPredecessor paths realize the distances under a decreasing rank · Finite DAG distances are at most every path weight · Finite non-source vertices have predecessors · Unreached vertices have no DAG shortest-path predecessor · Predecessor extraction fails exactly at infinite distances · Predecessor edges of the DAG shortest-path pass · The DAG shortest-path pass keeps its source · The DAG shortest-path pass gives the source distance zero · Directed adjacency graph · Edge of a directed adjacency graph

Used byExtracted DAG shortest paths are shortest paths

TheoremA failed DAG shortest-path run exhibits a cycle#✓fully proved

Let \(E\) be a list of integer-weighted directed edges on the vertices \(\{0, \dots, n-1\}\) and \(s\) a source vertex. If the DAG shortest-path algorithm on \(E\) from \(s\) fails, reporting the processed vertices and the list \(R\) of remaining vertices of its topological sort, then the directed graph with an edge \(u \to v\) for each edge of \(E\) from \(u\) to \(v\) contains a nonempty directed cycle without repeated vertices whose vertices all lie in \(R\).

public theorem dagShortestPaths_failure_cycle {n : Nat} (edges : List (Edge n)) (source : Fin n)
    (processed remaining : List (Fin n))
    (hf : (dagShortestPaths edges source).ret = .error (processed, remaining)) :
    ∃ cycle, TopologicalSort.DirectedCycleIn (toDirectedAdjacency edges) remaining cycle

Uses 10

Statement usesBellman-Ford distance table · Weighted directed edge · Weight-forgetting directed graph · Cost of the DAG shortest-path pass · Shortest paths in a DAG with a topology check · Directed cycle within a vertex list

Proof usesFailure output of DAG shortest paths · Outcome of Kahn's topological sort · A failed Kahn run leaves a directed cycle · Kahn's topological sort

TheoremThe DAG shortest-path algorithm succeeds exactly on acyclic graphs#✓fully proved

Let \(E\) be a list of integer-weighted directed edges on the vertices \(\{0, \dots, n-1\}\) and \(s\) a source vertex. The DAG shortest-path algorithm on \(E\) from \(s\) succeeds if and only if the directed graph with an edge \(u \to v\) for each edge of \(E\) from \(u\) to \(v\) has no directed cycle.

This includes disconnected graphs: a cycle unreachable from \(s\) still causes failure.

public theorem dagShortestPaths_returns_iff_acyclic {n : Nat} (edges : List (Edge n))
    (source : Fin n) :
    (∃ result, (dagShortestPaths edges source).ret = .ok result) ↔
      TopologicalSort.IsAcyclic (toDirectedAdjacency edges)

Uses 13

Statement usesBellman-Ford distance table · Weighted directed edge · Weight-forgetting directed graph · Cost of the DAG shortest-path pass · Shortest paths in a DAG with a topology check · Acyclic directed graph

Proof usesSuccessful output of DAG shortest paths · One-pass DAG shortest-path relaxation · Topological order · Outcome of Kahn's topological sort · Kahn's topological sort · Kahn's algorithm succeeds exactly on acyclic graphs · A successful topological sort is a topological order

TheoremDAG shortest-path distances are shortest-path weights#✓fully proved

Let \(E\) be a list of integer-weighted directed edges on the vertices \(\{0, \dots, n-1\}\) and \(s\) a source vertex. Suppose the DAG shortest-path algorithm on \(E\) from \(s\) succeeds and returns a finite distance \(d \in \mathbb{Z}\) for a vertex \(t\). Then some path from \(s\) to \(t\) in \(E\) has weight \(d\), and every path from \(s\) to \(t\) in \(E\) has weight at least \(d\). Here a path from \(s\) to \(t\) in \(E\) is a list of edges of \(E\), each starting where the previous one ends, the first starting at \(s\) and the last ending at \(t\) (the empty list when \(t = s\)), and its weight is the sum of its edge weights.

public theorem dagShortestPaths_distance_spec {n : Nat} (edges : List (Edge n))
    (source : Fin n) (result : Distances n)
    (hr : (dagShortestPaths edges source).ret = .ok result) (target : Fin n) (value : Int)
    (hd : result.distance.get target = some value) :
    (∃ path, IsWeightedPath edges source target path ∧ pathWeight path = value) ∧
      ∀ path, IsWeightedPath edges source target path → value ≤ pathWeight path

Uses 14

Statement usesBellman-Ford distance table · Weighted directed edge · Weighted path in an edge list · Bellman–Ford path weight · Cost of the DAG shortest-path pass · Shortest paths in a DAG with a topology check

Proof usesWeight-forgetting directed graph · Successful output of DAG shortest paths · One-pass DAG shortest-path relaxation · Finite DAG distances are at most every path weight · Finite DAG distances are path weights · Topological order · Outcome of Kahn's topological sort · Kahn's topological sort

TheoremUnreachable vertices are exactly those at infinite DAG distance#✓fully proved

Let \(E\) be a list of integer-weighted directed edges on the vertices \(\{0, \dots, n-1\}\) and \(s\) a source vertex. If the DAG shortest-path algorithm on \(E\) from \(s\) succeeds, then for every vertex \(t\) the returned distance to \(t\) is infinite if and only if \(t\) is not reachable from \(s\) in the directed graph with an edge \(u \to v\) for each edge of \(E\) from \(u\) to \(v\).

public theorem dagShortestPaths_distance_eq_none_iff {n : Nat} (edges : List (Edge n))
    (source : Fin n) (result : Distances n)
    (hr : (dagShortestPaths edges source).ret = .ok result) (target : Fin n) :
    result.distance.get target = none ↔ ¬(toDirectedAdjacency edges).Reachable source target

Uses 12

Statement usesBellman-Ford distance table · Weighted directed edge · Weight-forgetting directed graph · Cost of the DAG shortest-path pass · Shortest paths in a DAG with a topology check · Reachability in a directed graph

Proof usesSuccessful output of DAG shortest paths · One-pass DAG shortest-path relaxation · Infinite DAG distances are exactly unreachable vertices · Topological order · Outcome of Kahn's topological sort · Kahn's topological sort

TheoremExtracted DAG shortest paths are shortest paths#✓fully proved

Let \(E\) be a list of integer-weighted directed edges on the vertices \(\{0, \dots, n-1\}\) and \(s\) a source vertex. Suppose the DAG shortest-path algorithm on \(E\) from \(s\) succeeds, and following its predecessor edges back from a vertex \(t\) reaches \(s\) within \(n\) steps, giving the path \(P\). Then \(P\) is a path from \(s\) to \(t\) in \(E\), the returned distance to \(t\) is finite and equals the weight of \(P\), \(P\) has fewer than \(n\) edges, and every path from \(s\) to \(t\) in \(E\) has weight at least the weight of \(P\). Here a path from \(s\) to \(t\) in \(E\) is a list of edges of \(E\), each starting where the previous one ends, the first starting at \(s\) and the last ending at \(t\) (the empty list when \(t = s\)), and its weight is the sum of its edge weights.

public theorem dagShortestPaths_pathTo?_spec {n : Nat} (edges : List (Edge n))
    (source : Fin n) (result : Distances n)
    (hr : (dagShortestPaths edges source).ret = .ok result) (target : Fin n)
    (path : List (Edge n)) (hp : result.pathTo? target = some path) :
    IsWeightedPath edges source target path ∧ result.distance.get target = some (pathWeight path) ∧
      path.length < n ∧
      ∀ other, IsWeightedPath edges source target other → pathWeight path ≤ pathWeight other

Uses 14

Statement usesBellman-Ford distance table · Bellman-Ford path reconstruction · Weighted directed edge · Weighted path in an edge list · Bellman–Ford path weight · Cost of the DAG shortest-path pass · Shortest paths in a DAG with a topology check

Proof usesWeight-forgetting directed graph · Successful output of DAG shortest paths · One-pass DAG shortest-path relaxation · Paths extracted after topological relaxation are shortest paths · Topological order · Outcome of Kahn's topological sort · Kahn's topological sort

24 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.