Topological sorting

DefinitionIndegree within a vertex list#✓fully proved

For a finite directed graph \(G\), a list \(R\) of vertices and a vertex \(v\), the indegree of \(v\) within \(R\) is the number of entries \(u\) of \(R\), counted with multiplicity, such that \(G\) has an edge from \(u\) to \(v\).

public def indegreeWithin {α : Type u} [DecidableEq α]
    (g : DirectedAdjacency α) (remaining : List α) (v : α) : Nat :=
  remaining.countP (fun u => g.hasEdge u v)

Uses 2 · Used by 8

Statement usesDirected adjacency graph · Boolean edge test

Used byA failed Kahn run leaves a directed cycle · Unprocessed vertices of a failed Kahn run have positive indegree among the unprocessed · A failed Kahn run splits the vertices into processed and unprocessed ones · Indegree · Kahn's topological sort · A successful topological sort lists every vertex · A successful topological sort points every edge forward · A successful topological sort has no repeated vertex

DefinitionIndegree#✓fully proved

The indegree of a vertex \(v\) in a finite directed graph \(G\) is the number of vertices \(u\) such that \(G\) has an edge from \(u\) to \(v\); repeated entries in adjacency lists count once.

public def indegree {α : Type u} [DecidableEq α]
    (g : DirectedAdjacency α) (v : α) : Nat :=
  indegreeWithin g g.vertices v

Uses 2

Statement usesDirected adjacency graph · Indegree within a vertex list

InductiveOutcome of Kahn's topological sort#✓fully proved

The result of Kahn's topological sorting algorithm on a graph with vertices of type \(\alpha\) is either a success, carrying a list of vertices, or a failure, carrying the list of vertices processed before the queue emptied and the list of vertices that remain.

public inductive Result (α : Type u) where
  /-- Every vertex was processed in this order. -/
  | success (order : List α)
  /-- The queue emptied after `processed`, leaving exactly `remaining`. -/
  | failure (processed remaining : List α)
  deriving DecidableEq, Repr

Used by 20

Used byThe serializability theorem · Shortest 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 · Kahn's algorithm succeeds on acyclic graphs · A failed Kahn run leaves a directed cycle · Unprocessed vertices of a failed Kahn run have positive indegree among the unprocessed · A failed Kahn run splits the vertices into processed and unprocessed ones · Kahn's topological sort · Kahn's algorithm succeeds exactly on acyclic graphs · A successful topological sort lists every vertex · A successful topological sort points every edge forward · Success of Kahn's algorithm implies acyclicity · A successful topological sort is a topological order · A successful topological sort has no repeated vertex

DefinitionKahn's topological sort#✓fully proved

Run Kahn's algorithm with a first-in first-out queue on a finite directed graph \(G\) whose vertices are enumerated as \(v_1, \dots, v_n\). Initially every vertex is remaining, the counter of each vertex is its number of in-neighbours, and the queue holds the vertices with no in-neighbours in enumeration order. At each of \(n\) steps, if the queue is nonempty, its front vertex \(x\) is removed from the queue and from the remaining vertices and appended to the output; then each distinct out-neighbour \(y\) of \(x\) that is still remaining, taken in order of first occurrence in the adjacency list of \(x\), has its counter decreased by one and joins the back of the queue if that counter was \(1\). If no vertices remain after the \(n\) steps, the result is a success with the output list; otherwise it is a failure with the output list as the processed vertices and the remaining vertices in enumeration order.

Cslib.Algorithms.Lean.TopologicalSort.sort · 27 lines

public def sort {α : Type u} [DecidableEq α] [Hashable α]
    (g : DirectedAdjacency α) : Result α :=
  let advance := fun (s : List α × (α → Nat) × Std.Queue α × List α) =>
    match s.2.2.1.dequeue? with
    | none => s
    | some (vertex, queue) =>
        let remaining := s.1.erase vertex
        let rec dedup (seen : α → Bool) : List α → List α
          | [] => []
          | target :: neighbors =>
              if seen target then dedup seen neighbors
              else target :: dedup (Function.update seen target true) neighbors
        let scan := dedup (fun _ => false) (g.adjacency vertex)
        let (degrees, queue) := scan.foldl (fun result v =>
              if v ∈ remaining && g.hasEdge vertex v then
                let old := result.1 v
                (Function.update result.1 v (old - 1),
                  if old == 1 then result.2.enqueue v else result.2)
              else
                result) (s.2.1, queue)
        (remaining, degrees, queue, s.2.2.2 ++ [vertex])
  let final := advance^[g.vertices.length]
    (g.vertices,
      indegreeWithin g g.vertices,
      Std.Queue.mk [] (g.vertices.filter fun v => indegreeWithin g g.vertices v == 0),
      [])
  if final.1.isEmpty then .success final.2.2.2 else .failure final.2.2.2 final.1

Uses 4 · Used by 19

Statement usesDirected adjacency graph · Boolean edge test · Outcome of Kahn's topological sort · Indegree within a vertex list

Used byThe serializability theorem · Shortest 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 · Kahn's algorithm succeeds on acyclic graphs · A failed Kahn run leaves a directed cycle · Unprocessed vertices of a failed Kahn run have positive indegree among the unprocessed · A failed Kahn run splits the vertices into processed and unprocessed ones · Kahn's algorithm succeeds exactly on acyclic graphs · A successful topological sort lists every vertex · A successful topological sort points every edge forward · Success of Kahn's algorithm implies acyclicity · A successful topological sort is a topological order · A successful topological sort has no repeated vertex

DefinitionDirected cycle within a vertex list#✓fully proved

Let \(G\) be a finite directed graph and \(R\) a list of vertices. A list \(c = [c_1, \dots, c_k]\) of vertices is a directed cycle of \(G\) in \(R\) when \(k \ge 1\), the vertices \(c_1, \dots, c_k\) are pairwise distinct, \(G\) has an edge from \(c_i\) to \(c_{i+1}\) for each \(1 \le i < k\) and an edge from \(c_k\) to \(c_1\), and every \(c_i\) lies in \(R\).

public def DirectedCycleIn {α : Type u}
    (g : DirectedAdjacency α) (remaining cycle : List α) : Prop :=
  cycle ≠ [] ∧
  cycle.Nodup ∧
  cycle.IsChain g.Edge ∧
  (match cycle with
    | [] => false
    | first :: rest => g.Edge (List.getLast (first :: rest) (by simp)) first) ∧
  ∀ v ∈ cycle, v ∈ remaining

Uses 2 · Used by 9

Statement usesDirected adjacency graph · Edge of a directed adjacency graph

Used byA rank increasing along precedence edges gives conflict serializability · A conflict-serializable schedule has an acyclic precedence graph · A failed DAG shortest-path run exhibits a cycle · Kahn's algorithm succeeds on acyclic graphs · Characterization of directed cycles within a vertex list · A failed Kahn run leaves a directed cycle · Acyclic directed graph · Acyclicity means having no directed cycle · Success of Kahn's algorithm implies acyclicity

TheoremCharacterization of directed cycles within a vertex list#✓fully proved

Let \(G\) be a finite directed graph and let \(R\) and \(c = [c_1, \dots, c_k]\) be lists of vertices. Then \(c\) is a directed cycle of \(G\) in \(R\) if and only if \(k \ge 1\), the vertices \(c_1, \dots, c_k\) are pairwise distinct, \(G\) has an edge from \(c_i\) to \(c_{i+1}\) for every \(1 \le i < k\), \(G\) has an edge from \(c_k\) to \(c_1\), and every \(c_i\) lies in \(R\).

public theorem directedCycleIn_iff {α : Type u}
    (g : DirectedAdjacency α) (remaining cycle : List α) :
    DirectedCycleIn g remaining cycle ↔
      ∃ hne : cycle ≠ [],
        cycle.Nodup ∧
        cycle.IsChain g.Edge ∧
        g.Edge (cycle.getLast hne) (cycle.head hne) ∧
        ∀ v ∈ cycle, v ∈ remaining

Uses 3 · Used by 5

Statement usesDirected adjacency graph · Edge of a directed adjacency graph · Directed cycle within a vertex list

Used byA rank increasing along precedence edges gives conflict serializability · A conflict-serializable schedule has an acyclic precedence graph · Kahn's algorithm succeeds on acyclic graphs · A failed Kahn run leaves a directed cycle · Success of Kahn's algorithm implies acyclicity

DefinitionAcyclic directed graph#✓fully proved

A finite directed graph \(G\) is acyclic when it has no directed cycle, that is, no nonempty list \([c_1, \dots, c_k]\) of pairwise distinct vertices such that \(G\) has an edge from \(c_i\) to \(c_{i+1}\) for each \(1 \le i < k\) and an edge from \(c_k\) to \(c_1\).

public def IsAcyclic {α : Type u} (g : DirectedAdjacency α) : Prop :=
  ¬ ∃ cycle, DirectedCycleIn g g.vertices cycle

Uses 2 · Used by 8

Statement usesDirected adjacency graph · Directed cycle within a vertex list

Used byThe serializability theorem · A rank increasing along precedence edges gives conflict serializability · A conflict-serializable schedule has an acyclic precedence graph · The DAG shortest-path algorithm succeeds exactly on acyclic graphs · Kahn's algorithm succeeds on acyclic graphs · Acyclicity means having no directed cycle · Kahn's algorithm succeeds exactly on acyclic graphs · Success of Kahn's algorithm implies acyclicity

TheoremAcyclicity means having no directed cycle#✓fully proved

A finite directed graph \(G\) is acyclic if and only if there is no directed cycle of \(G\) in its vertex list, that is, no nonempty list of pairwise distinct vertices in which each vertex has an edge to the next and the last vertex has an edge to the first.

public theorem isAcyclic_iff_no_directedCycle {α : Type u}
    (g : DirectedAdjacency α) :
    IsAcyclic g ↔ ¬ ∃ cycle, DirectedCycleIn g g.vertices cycle

Uses 3

Statement usesDirected adjacency graph · Directed cycle within a vertex list · Acyclic directed graph

DefinitionTopological order#✓fully proved

A list \(L\) of vertices of a finite directed graph \(G\) is a topological order of \(G\) when \(L\) has no duplicates, a vertex lies in \(L\) exactly when it lies in the vertex enumeration of \(G\), and for every edge \(u \to v\) of \(G\) the first position of \(u\) in \(L\) is strictly smaller than the first position of \(v\) in \(L\).

public def IsTopologicalOrder {α : Type u} [DecidableEq α]
    (g : DirectedAdjacency α) (order : List α) : Prop :=
  order.Nodup ∧
  (∀ v, v ∈ order ↔ v ∈ g.vertices) ∧
  ∀ u v, g.Edge u v → order.idxOf u < order.idxOf v

Uses 2 · Used by 23

Statement usesDirected adjacency graph · Edge of a directed adjacency graph

Used bySerializing along a topological order preserves conflict equivalence · The serializability theorem · Unreachable 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 · 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 · A successful topological sort is a topological order

TheoremA successful topological sort has no repeated vertex#✓fully proved

If Kahn's topological sort on a finite directed graph \(G\) returns a success with list \(L\), then \(L\) has no duplicates.

public theorem success_nodup {α : Type u} [DecidableEq α] [Hashable α]
    (g : DirectedAdjacency α) (order : List α)
    (h : sort g = .success order) : order.Nodup

Uses 9 · Used by 1

Statement usesDirected adjacency graph · Outcome of Kahn's topological sort · Kahn's topological sort

Proof usesBoolean edge test · Contents of a two-list queue · Enqueueing appends to the contents · A successful dequeue splits off the first element · Dequeueing fails exactly on empty queues · Indegree within a vertex list

Used byA successful topological sort is a topological order

TheoremA successful topological sort lists every vertex#✓fully proved

If Kahn's topological sort on a finite directed graph \(G\) returns a success with list \(L\), then a vertex lies in \(L\) if and only if it lies in the vertex enumeration of \(G\).

public theorem success_coverage {α : Type u} [DecidableEq α] [Hashable α]
    (g : DirectedAdjacency α) (order : List α)
    (h : sort g = .success order) : ∀ v, v ∈ order ↔ v ∈ g.vertices

Uses 9 · Used by 1

Statement usesDirected adjacency graph · Outcome of Kahn's topological sort · Kahn's topological sort

Proof usesBoolean edge test · Contents of a two-list queue · Enqueueing appends to the contents · A successful dequeue splits off the first element · Dequeueing fails exactly on empty queues · Indegree within a vertex list

Used byA successful topological sort is a topological order

TheoremA successful topological sort points every edge forward#✓fully proved

If Kahn's topological sort on a finite directed graph \(G\) returns a success with list \(L\), then for every edge \(u \to v\) of \(G\) the first position of \(u\) in \(L\) is strictly smaller than the first position of \(v\) in \(L\).

public theorem success_edge_forward {α : Type u} [DecidableEq α] [Hashable α]
    (g : DirectedAdjacency α) (order : List α) (h : sort g = .success order) :
    ∀ u v, g.Edge u v → order.idxOf u < order.idxOf v

Uses 11 · Used by 2

Statement usesDirected adjacency graph · Edge of a directed adjacency graph · Outcome of Kahn's topological sort · Kahn's topological sort

Proof usesBoolean edge test · The Boolean edge test is correct · Contents of a two-list queue · Enqueueing appends to the contents · A successful dequeue splits off the first element · Dequeueing fails exactly on empty queues · Indegree within a vertex list

Used bySuccess of Kahn's algorithm implies acyclicity · A successful topological sort is a topological order

TheoremA successful topological sort is a topological order#✓fully proved

If Kahn's topological sort on a finite directed graph \(G\) returns a success with list \(L\), then \(L\) is a topological order of \(G\).

public theorem success_isTopologicalOrder {α : Type u} [DecidableEq α] [Hashable α]
    (g : DirectedAdjacency α) (order : List α) (h : sort g = .success order) :
    IsTopologicalOrder g order

Uses 8 · Used by 3

Statement usesDirected adjacency graph · Topological order · Outcome of Kahn's topological sort · Kahn's topological sort

Proof usesEdge of a directed adjacency graph · A successful topological sort lists every vertex · A successful topological sort points every edge forward · A successful topological sort has no repeated vertex

Used byThe serializability theorem · Successful output of DAG shortest paths · The DAG shortest-path algorithm succeeds exactly on acyclic graphs

TheoremA failed Kahn run splits the vertices into processed and unprocessed ones#✓fully proved

Let \(G\) be a finite directed graph. If deterministic FIFO Kahn topological sorting of \(G\) fails after processing the vertex list \(P\) and leaving the vertex list \(R\) unprocessed, then \(R\) is nonempty, neither \(P\) nor \(R\) has repeated entries, a vertex lies in the vertex list of \(G\) if and only if it lies in \(P\) or in \(R\), and no vertex lies in both \(P\) and \(R\).

public theorem failure_remainder {α : Type u} [DecidableEq α] [Hashable α]
    (g : DirectedAdjacency α) (processed remaining : List α)
    (h : sort g = .failure processed remaining) :
    remaining ≠ [] ∧ processed.Nodup ∧ remaining.Nodup ∧
      (∀ v, v ∈ g.vertices ↔ v ∈ processed ∨ v ∈ remaining) ∧
      (∀ v ∈ processed, v ∉ remaining)

Uses 9 · Used by 2

Statement usesDirected adjacency graph · Outcome of Kahn's topological sort · Kahn's topological sort

Proof usesBoolean edge test · Contents of a two-list queue · Enqueueing appends to the contents · A successful dequeue splits off the first element · Dequeueing fails exactly on empty queues · Indegree within a vertex list

Used byKahn's algorithm succeeds on acyclic graphs · A failed Kahn run leaves a directed cycle

TheoremUnprocessed vertices of a failed Kahn run have positive indegree among the unprocessed#✓fully proved

Let \(G\) be a finite directed graph. If deterministic FIFO Kahn topological sorting of \(G\) fails after processing the vertex list \(P\) and leaving the vertex list \(R\) unprocessed, then for every vertex \(v\) in \(R\) the indegree of \(v\) within \(R\), the number of entries \(u\) of \(R\) such that \(G\) has an edge from \(u\) to \(v\), is positive.

public theorem failure_positive_indegree {α : Type u} [DecidableEq α] [Hashable α]
    (g : DirectedAdjacency α) (processed remaining : List α)
    (h : sort g = .failure processed remaining) :
    ∀ v ∈ remaining, 0 < indegreeWithin g remaining v

Uses 9 · Used by 1

Statement usesDirected adjacency graph · Outcome of Kahn's topological sort · Indegree within a vertex list · Kahn's topological sort

Proof usesBoolean edge test · Contents of a two-list queue · Enqueueing appends to the contents · A successful dequeue splits off the first element · Dequeueing fails exactly on empty queues

Used byA failed Kahn run leaves a directed cycle

TheoremA failed Kahn run leaves a directed cycle#✓fully proved

Let \(G\) be a finite directed graph. If deterministic FIFO Kahn topological sorting of \(G\) fails after processing the vertex list \(P\) and leaving the vertex list \(R\) unprocessed, then \(G\) has a directed cycle in \(R\): a nonempty list of pairwise distinct vertices of \(R\) in which each vertex has an edge to the next and the last vertex has an edge to the first.

public theorem failure_cycle {α : Type u} [DecidableEq α] [Hashable α]
    (g : DirectedAdjacency α) (processed remaining : List α)
    (h : sort g = .failure processed remaining) :
    ∃ cycle, DirectedCycleIn g remaining cycle

Uses 11 · Used by 2

Statement usesDirected adjacency graph · Directed cycle within a vertex list · Outcome of Kahn's topological sort · Kahn's topological sort

Proof usesEdge of a directed adjacency graph · Boolean edge test · The Boolean edge test is correct · Characterization of directed cycles within a vertex list · Unprocessed vertices of a failed Kahn run have positive indegree among the unprocessed · A failed Kahn run splits the vertices into processed and unprocessed ones · Indegree within a vertex list

Used byA failed DAG shortest-path run exhibits a cycle · Kahn's algorithm succeeds on acyclic graphs

TheoremSuccess of Kahn's algorithm implies acyclicity#✓fully proved

If Kahn's topological sort on a finite directed graph \(G\) returns a success, then \(G\) is acyclic.

public theorem success_implies_acyclic {α : Type u} [DecidableEq α] [Hashable α]
    (g : DirectedAdjacency α) (order : List α) (h : sort g = .success order) : IsAcyclic g

Uses 8 · Used by 1

Statement usesDirected adjacency graph · Acyclic directed graph · Outcome of Kahn's topological sort · Kahn's topological sort

Proof usesEdge of a directed adjacency graph · Directed cycle within a vertex list · Characterization of directed cycles within a vertex list · A successful topological sort points every edge forward

Used byKahn's algorithm succeeds exactly on acyclic graphs

TheoremKahn's algorithm succeeds on acyclic graphs#✓fully proved

If a finite directed graph \(G\), given by a vertex enumeration and adjacency lists, is acyclic, then deterministic FIFO Kahn topological sorting of \(G\) returns success with some vertex order.

public theorem acyclic_implies_success {α : Type u} [DecidableEq α] [Hashable α]
    (g : DirectedAdjacency α) (hacyclic : IsAcyclic g) :
    ∃ order, sort g = .success order

Uses 9 · Used by 2

Statement usesDirected adjacency graph · Acyclic directed graph · Outcome of Kahn's topological sort · Kahn's topological sort

Proof usesEdge of a directed adjacency graph · Directed cycle within a vertex list · Characterization of directed cycles within a vertex list · A failed Kahn run leaves a directed cycle · A failed Kahn run splits the vertices into processed and unprocessed ones

Used byThe serializability theorem · Kahn's algorithm succeeds exactly on acyclic graphs

TheoremKahn's algorithm succeeds exactly on acyclic graphs#✓fully proved

For every finite directed graph \(G\), Kahn's topological sort on \(G\) returns a success if and only if \(G\) is acyclic.

public theorem succeeds_iff_acyclic {α : Type u} [DecidableEq α] [Hashable α]
    (g : DirectedAdjacency α) :
    (∃ order, sort g = .success order) ↔ IsAcyclic g

Uses 6 · Used by 1

Statement usesDirected adjacency graph · Acyclic directed graph · Outcome of Kahn's topological sort · Kahn's topological sort

Proof usesKahn's algorithm succeeds on acyclic graphs · Success of Kahn's algorithm implies acyclicity

Used byThe DAG shortest-path algorithm succeeds exactly on acyclic graphs

19 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.