Transitive closure

DefinitionStaged transitive-closure computation#✓fully proved

Let \(A\) be a Boolean adjacency matrix on the vertices \(0, \dots, n-1\) and let \(k \le n\). The computation first builds the \(n \times n\) Boolean matrix \(T^{(0)}\) whose entry \((i, j)\) is true exactly when \(i = j\) or \(A_{ij}\) is true. Then, for \(p = 0, \dots, k - 1\), it builds a new matrix \(T^{(p+1)}\) from the saved matrix \(T^{(p)}\) by \(T^{(p+1)}_{ij} = T^{(p)}_{ij} \lor (T^{(p)}_{ip} \land T^{(p)}_{pj})\), and it returns \(T^{(k)}\). One time unit is charged for each cell assignment.

@[no_expose]
def transitiveClosureStages {n : Nat} (adjacency : Fin n → Fin n → Bool)
    (pivots : Nat) (hpivots : pivots ≤ n) : TimeM Nat (Vector (Vector Bool n) n) := do
  let initial ← buildInitial adjacency n (by omega)
  runStages initial pivots hpivots

Used by 9

Used bySaved-matrix transitive-closure algorithm · Correctness of the transitive-closure algorithm · Cost of initializing the transitive-closure matrix · Cost of one transition stage · Invariant of the transitive-closure stages · Transition recurrence of the transitive-closure stages · Initial matrix of the transitive-closure computation · Running time of the transitive-closure algorithm · Cost of the transition stages of transitive closure

DefinitionSaved-matrix transitive-closure algorithm#✓fully proved

Given a Boolean adjacency matrix \(A\) on the vertices \(0, 1, \dots, n-1\), the algorithm first builds the matrix \(t^{(0)}\) with \(t^{(0)}_{ij}\) true exactly when \(i = j\) or \(A_{ij}\) is true. Then, for \(k = 0, 1, \dots, n-1\) in turn, it builds a new matrix \(t^{(k+1)}\) with \(t^{(k+1)}_{ij} = t^{(k)}_{ij} \lor (t^{(k)}_{ik} \land t^{(k)}_{kj})\) for all \(i, j\), reading every operand from the saved matrix \(t^{(k)}\), and it returns \(t^{(n)}\). One time unit is charged for each cell assignment; reads, Boolean operations and matrix allocation are free.

This is the saved-matrix recurrence of CLRS for the reflexive transitive closure.

@[no_expose]
def transitiveClosure {n : Nat} (adjacency : Fin n → Fin n → Bool) :
    TimeM Nat (Fin n → Fin n → Bool) := do
  let final ← transitiveClosureStages adjacency n (by omega)
  pure fun i j => (final.get i).get j

Uses 1 · Used by 4

Statement usesStaged transitive-closure computation

Used byCorrectness of the transitive-closure algorithm · Running time of the transitive-closure algorithm · Cost of transitive closure on one vertex · Cost of transitive closure on the empty graph

TheoremInitial matrix of the transitive-closure computation#✓fully proved

Let \(A\) be a Boolean adjacency matrix on the vertices \(0, \dots, n-1\). For all vertices \(i\) and \(j\), the entry \((i, j)\) of the matrix produced by the staged transitive-closure computation with no pivot stages is true if and only if \(i = j\) or \(A_{ij}\) is true.

theorem transitiveClosureStages_zero_cell {n : Nat} (adjacency : Fin n → Fin n → Bool)
    (i j : Fin n) :
    ((transitiveClosureStages adjacency 0 (by omega)).ret.get i).get j =
      (decide (i = j) || adjacency i j)

Uses 1 · Used by 1

Statement usesStaged transitive-closure computation

Used byInvariant of the transitive-closure stages

TheoremTransition recurrence of the transitive-closure stages#✓fully proved

Let \(A\) be a Boolean adjacency matrix on the vertices \(0, \dots, n-1\), and for \(m \le n\) let \(T^{(m)}\) be the matrix produced by the staged transitive-closure computation on \(A\) after its first \(m\) pivot stages. For every \(k < n\) and all vertices \(i\) and \(j\),

\[T^{(k+1)}_{ij} = T^{(k)}_{ij} \lor \bigl(T^{(k)}_{ik} \land T^{(k)}_{kj}\bigr).\]

Every operand of stage \(k + 1\) is read from the complete matrix saved after stage \(k\).

theorem transitiveClosureStages_succ_cell {n : Nat} (adjacency : Fin n → Fin n → Bool)
    (k : Nat) (hk : k < n) (i j : Fin n) :
    let previous := (transitiveClosureStages adjacency k (by omega)).ret
    ((transitiveClosureStages adjacency (k + 1) (by omega)).ret.get i).get j =
      ((previous.get i).get j ||
        ((previous.get i).get ⟨k, hk⟩ && (previous.get ⟨k, hk⟩).get j))

Uses 1 · Used by 1

Statement usesStaged transitive-closure computation

Used byInvariant of the transitive-closure stages

TheoremCost of initializing the transitive-closure matrix#✓fully proved

For every Boolean adjacency matrix on \(n\) vertices, the staged transitive-closure computation with no pivot stages (only the initialization of the \(n \times n\) matrix) charges exactly \(n^2\) time units, one for each cell assignment.

theorem transitiveClosure_initializations {n : Nat} (adjacency : Fin n → Fin n → Bool) :
    (transitiveClosureStages adjacency 0 (by omega)).time = n ^ 2

Uses 1

Statement usesStaged transitive-closure computation

TheoremCost of one transition stage#✓fully proved

For every Boolean adjacency matrix on \(n\) vertices and every \(k < n\), the time charged by the staged transitive-closure computation with \(k + 1\) pivot stages minus the time charged with \(k\) pivot stages equals \(n^2\): one time unit for each cell assignment of the new stage.

theorem transitiveClosure_stage_assignments {n : Nat} (adjacency : Fin n → Fin n → Bool)
    (k : Nat) (hk : k < n) :
    (transitiveClosureStages adjacency (k + 1) (by omega)).time -
        (transitiveClosureStages adjacency k (by omega)).time = n ^ 2

Uses 1

Statement usesStaged transitive-closure computation

TheoremCost of the transition stages of transitive closure#✓fully proved

Charge one time unit for each cell assignment. For every Boolean adjacency matrix on \(n\) vertices, let \(a\) be the cost of running the initialization of the saved-matrix transitive-closure algorithm followed by all \(n\) of its stages, and let \(b\) be the cost of running the initialization alone. Then \(a - b = n^3\), where the subtraction is subtraction of natural numbers, truncated at \(0\). That is, the \(n\) transition stages together perform exactly \(n^3\) cell assignments.

theorem transitiveClosure_transition_assignments {n : Nat}
    (adjacency : Fin n → Fin n → Bool) :
    (transitiveClosureStages adjacency n (by omega)).time -
        (transitiveClosureStages adjacency 0 (by omega)).time = n ^ 3

Uses 1

Statement usesStaged transitive-closure computation

TheoremInvariant of the transitive-closure stages#✓fully proved

Let \(A\) be a Boolean adjacency matrix of a directed graph on the vertices \(0, \dots, n-1\) and let \(k \le n\). For all vertices \(i\) and \(j\), the entry \((i, j)\) of the matrix produced by the staged transitive-closure computation after its first \(k\) pivot stages is true if and only if there are vertices \(i = v_0, v_1, \dots, v_m = j\) with \(m \ge 0\) such that each \(A_{v_t v_{t+1}}\) is true and every intermediate vertex \(v_1, \dots, v_{m-1}\) is less than \(k\).

theorem transitiveClosureStages_cell_eq_true_iff {n : Nat}
    (adjacency : Fin n → Fin n → Bool) (pivots : Nat) (hpivots : pivots ≤ n)
    (i j : Fin n) :
    ((transitiveClosureStages adjacency pivots hpivots).ret.get i).get j = true ↔
      ∃ path, path.IsChainFromTo (fun a b => adjacency a b = true) i j ∧
        FloydWarshall.InternalVerticesBelow pivots path

Uses 4 · Used by 1

Statement usesIntermediate vertices below a bound · Staged transitive-closure computation

Proof usesTransition recurrence of the transitive-closure stages · Initial matrix of the transitive-closure computation

Used byCorrectness of the transitive-closure algorithm

TheoremCorrectness of the transitive-closure algorithm#✓fully proved

Let \(A\) be a Boolean adjacency matrix of a directed graph on the vertices \(0, \dots, n-1\). For all vertices \(i\) and \(j\), the entry \((i, j)\) of the matrix returned by the transitive-closure algorithm on \(A\) is true if and only if \(j\) is reachable from \(i\) by a sequence of zero or more edges of the graph.

theorem transitiveClosure_cell_eq_true_iff {n : Nat}
    (adjacency : Fin n → Fin n → Bool) (i j : Fin n) :
    (transitiveClosure adjacency).ret i j = true ↔
      Relation.ReflTransGen (fun a b => adjacency a b = true) i j

Uses 4

Statement usesSaved-matrix transitive-closure algorithm

Proof usesIntermediate vertices below a bound · Staged transitive-closure computation · Invariant of the transitive-closure stages

TheoremRunning time of the transitive-closure algorithm#✓fully proved

For every Boolean adjacency matrix on \(n\) vertices, the transitive-closure algorithm charges exactly \(n^2 + n^3\) time units: \(n^2\) cell assignments to initialize the matrix and \(n^2\) in each of the \(n\) transition stages.

theorem transitiveClosure_time {n : Nat} (adjacency : Fin n → Fin n → Bool) :
    (transitiveClosure adjacency).time = n ^ 2 + n ^ 3

Uses 2 · Used by 2

Statement usesSaved-matrix transitive-closure algorithm

Proof usesStaged transitive-closure computation

Used byCost of transitive closure on one vertex · Cost of transitive closure on the empty graph

TheoremCost of transitive closure on the empty graph#✓fully proved

For the graph with no vertices, the transitive-closure algorithm charges \(0\) time units: it performs no cell assignments.

theorem transitiveClosure_time_zero (adjacency : Fin 0 → Fin 0 → Bool) :
    (transitiveClosure adjacency).time = 0

Uses 2

Statement usesSaved-matrix transitive-closure algorithm

Proof usesRunning time of the transitive-closure algorithm

TheoremCost of transitive closure on one vertex#✓fully proved

For every Boolean adjacency matrix on a single vertex, the transitive-closure algorithm charges exactly \(2\) time units: one cell assignment for the initialization and one for the single transition stage.

theorem transitiveClosure_time_one (adjacency : Fin 1 → Fin 1 → Bool) :
    (transitiveClosure adjacency).time = 2

Uses 2

Statement usesSaved-matrix transitive-closure algorithm

Proof usesRunning time of the transitive-closure algorithm

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.