Breadth-first search

StructureResult of breadth-first search#✓fully proved

A breadth-first search result on a vertex type \(V\) consists of a distance function, assigning to each vertex either a natural number or none, and a list of vertices. They are meant to record the shortest distance from the source (none when the vertex is unreachable) and the vertices in first-discovery order.

structure BFSResult (V : Type u) where
  /-- The shortest distance from the source, or `none` when unreachable. -/
  distance : V → Option Nat
  /-- Vertices in first-discovery order. -/
  order : List (V)

Used by 37

Used byThe Edmonds–Karp flow is feasible · Maximality of the Edmonds–Karp flow · The Edmonds–Karp flow value equals its residual cut capacity · No augmenting path remains after Edmonds–Karp · The augmentation loop never decreases the flow value · One augmentation step keeps or strictly raises the flow value · The Edmonds-Karp residual cut separates source and sink · Residual cut · Shortest path via breadth-first search · The shortest-path search succeeds exactly when the sink is reachable · Soundness of the shortest-path search · Breadth-first search · The executable BFS agrees with the list model · Breadth-first search on the vertices \(0, \dots, n-1\) · List model of breadth-first search · Breadth-first search with parent pointers · Breadth-first search with parents returns the ordinary BFS result · Exact cost of BFS with parents · Linear bound on the cost of BFS with parents · Breadth-first search forest · BFS reports exactly the shortest walk length · BFS reports a distance exactly for the reachable vertices · BFS discovers vertices in nondecreasing distance · BFS lists exactly the reachable vertices · BFS discovers each vertex at most once · Path reconstruction from BFS parents · Path reconstruction fails exactly at unreachable vertices · Path reconstruction at the source · Reconstructed BFS paths are shortest paths · Cost of path reconstruction for a reachable vertex · Cost of path reconstruction for an unreachable vertex · Saved-parent chains are simple · Each reachable vertex has a unique saved-parent chain · A BFS parent is one step closer to the source · The BFS parent is the first discovered in-neighbour · Exactly the source and the unreachable vertices have no BFS parent · Breadth-first search places the source at distance zero

DefinitionList model of breadth-first search#✓fully proved

Given a finite directed graph \(G\) with ordered adjacency lists and a source vertex \(s\), the list model keeps a list of processed pairs and a queue of pairs \((v, d)\) of a vertex and a distance, starting with no processed pairs and the queue \([(s, 0)]\). It performs one round per vertex of \(G\): if the queue is empty, nothing changes; otherwise the front pair \((u, d)\) is removed from the queue and recorded as processed, and then each entry \(w\) of the adjacency list of \(u\), from left to right, is appended to the queue as \((w, d + 1)\) unless \(w\) already occurs in a processed or queued pair. The reported distance of a vertex \(v\) is the distance in the first pair for \(v\) in the list of processed pairs in processing order followed by the queue, or none if there is no such pair; the reported order lists the processed vertices in processing order.

The model can be evaluated by kernel reduction, which is used to check concrete results.

def bfsModel (g : DirectedAdjacency V) (s : V) : BFSResult V :=
  let initial : List (V × Nat) × List (V × Nat) := ([], [(s, 0)])
  let final := g.vertices.foldr (fun _ state =>
    match state.2 with
    | [] => state
    | entry :: queue =>
        (g.adjacency entry.1).foldl (fun state vertex =>
          if ((state.1.reverse ++ state.2).map Prod.fst).contains vertex then state
          else (state.1, state.2 ++ [(vertex, entry.2 + 1)]))
          (entry :: state.1, queue)) initial
  let entries := final.1.reverse ++ final.2
  { distance := fun v => (entries.find? fun entry => entry.1 == v).map Prod.snd
    order := final.1.reverse.map Prod.fst }

Uses 2 · Used by 1

Statement usesResult of breadth-first search · Directed adjacency graph

Used byThe executable BFS agrees with the list model

DefinitionBreadth-first search#✓fully proved

Given a finite directed graph \(G\) with ordered adjacency lists and a source vertex \(s\), breadth-first search keeps a FIFO queue of pairs \((v, d)\) of a vertex and a distance and a table of discovered vertices with their distances, starting with the queue \([(s, 0)]\) and \(s\) discovered at distance \(0\). It performs one round per vertex of \(G\): if the queue is empty, nothing changes; otherwise it dequeues the front pair \((u, d)\), records \(u\) as processed, and scans the adjacency list of \(u\) from left to right, enqueueing each entry \(w\) that is not yet discovered as \((w, d + 1)\) and discovering it at distance \(d + 1\). The result reports for each vertex its discovered distance, or none if it was never discovered, and lists the processed vertices in processing order.

The table is a hash map, so the search runs in expected time linear in the number of vertices plus the total length of the adjacency lists.

Cslib.Algorithms.Lean.BreadthFirstSearch.bfs · 16 lines

def bfs (g : DirectedAdjacency V) (s : V) : BFSResult V :=
  let initial : List (V × Nat) × (Std.Queue (V × Nat) × Std.HashMap V Nat) :=
    ([], ((Std.Queue.empty : Std.Queue (V × Nat)).enqueue (s, 0),
      (Std.HashMap.emptyWithCapacity 1).insert s 0))
  let final := Nat.fold g.vertices.length (fun _ _ state =>
    match state.2.1.dequeue? with
    | none => state
    | some (entry, queue) =>
        (g.adjacency entry.1).foldl (fun state vertex =>
          if state.2.2.contains vertex then state
          else (state.1,
            (state.2.1.enqueue (vertex, entry.2 + 1),
              state.2.2.insert vertex (entry.2 + 1))))
          (entry :: state.1, (queue, state.2.2))) initial
  { distance := fun v => final.2.2[v]?
    order := final.1.reverse.map Prod.fst }

Uses 2 · Used by 30

Statement usesResult of breadth-first search · Directed adjacency graph

Used byThe Edmonds–Karp flow is feasible · Maximality of the Edmonds–Karp flow · The Edmonds–Karp flow value equals its residual cut capacity · No augmenting path remains after Edmonds–Karp · The augmentation loop never decreases the flow value · One augmentation step keeps or strictly raises the flow value · The Edmonds-Karp residual cut separates source and sink · Residual cut · Shortest path via breadth-first search · The shortest-path search succeeds exactly when the sink is reachable · Soundness of the shortest-path search · The executable BFS agrees with the list model · Breadth-first search on the vertices \(0, \dots, n-1\) · Breadth-first search with parents returns the ordinary BFS result · Exact cost of BFS with parents · Linear bound on the cost of BFS with parents · BFS reports exactly the shortest walk length · BFS reports a distance exactly for the reachable vertices · BFS discovers vertices in nondecreasing distance · BFS lists exactly the reachable vertices · BFS discovers each vertex at most once · Path reconstruction fails exactly at unreachable vertices · Reconstructed BFS paths are shortest paths · Cost of path reconstruction for a reachable vertex · Cost of path reconstruction for an unreachable vertex · Saved-parent chains are simple · Each reachable vertex has a unique saved-parent chain · The BFS parent is the first discovered in-neighbour · Exactly the source and the unreachable vertices have no BFS parent · Breadth-first search places the source at distance zero

TheoremThe executable BFS agrees with the list model#✓fully proved

For every finite directed graph \(G\) with ordered adjacency lists and every source vertex \(s\), the result of the executable breadth-first search from \(s\) equals the result of the list model of breadth-first search from \(s\): both report the same distance (or none) for every vertex and the same first-discovery order.

theorem bfs_eq_bfsModel (g : DirectedAdjacency V) (s : V) :
    bfs g s = bfsModel g s

Uses 10

Statement usesResult of breadth-first search · Breadth-first search · List model of breadth-first search · Directed adjacency graph

Proof usesEdge of a directed adjacency graph · Walks of a given length · 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

DefinitionBreadth-first search on the vertices \(0, \dots, n-1\)#✓fully proved

Given a natural number \(n\), an adjacency function assigning to each vertex \(i < n\) an ordered list of vertices among \(0, \dots, n-1\), and a source vertex \(s < n\), this is the result of breadth-first search from \(s\) on the finite directed graph with vertex enumeration \(0, 1, \dots, n-1\) and these adjacency lists.

def bfsFin {n : Nat} (adjacency : Fin n → List (Fin n)) (source : Fin n) :
    BFSResult (Fin n) :=
  bfs
    { vertices := List.finRange n
      vertices_nodup := List.nodup_finRange n
      vertices_complete := List.mem_finRange
      adjacency }
    source

Uses 3

Statement usesResult of breadth-first search · Breadth-first search · Directed adjacency graph

TheoremBFS reports a distance exactly for the reachable vertices#✓fully proved

For every finite directed graph \(G\) with ordered adjacency lists and all vertices \(s\) and \(v\), breadth-first search from \(s\) reports some distance for \(v\) (rather than none) if and only if \(v\) is reachable from \(s\) in \(G\).

theorem distance_present_iff_reachable (g : DirectedAdjacency V) (s v : V) :
    (∃ d, (bfs g s).distance v = some d) ↔ g.Reachable s v

Uses 11 · Used by 6

Statement usesResult of breadth-first search · Breadth-first search · Directed adjacency graph · Reachability in a directed graph

Proof usesEdge of a directed adjacency graph · Walks of a given length · Reachability by walks · 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 byThe shortest-path search succeeds exactly when the sink is reachable · Path reconstruction fails exactly at unreachable vertices · Reconstructed BFS paths are shortest paths · Saved-parent chains are simple · Each reachable vertex has a unique saved-parent chain · Exactly the source and the unreachable vertices have no BFS parent

TheoremBFS lists exactly the reachable vertices#✓fully proved

For every finite directed graph \(G\) with ordered adjacency lists and all vertices \(s\) and \(v\), the vertex \(v\) occurs in the first-discovery order of breadth-first search from \(s\) if and only if \(v\) is reachable from \(s\) in \(G\).

theorem order_mem_iff_reachable (g : DirectedAdjacency V) (s v : V) :
    v ∈ (bfs g s).order ↔ g.Reachable s v

Uses 11 · Used by 7

Statement usesResult of breadth-first search · Breadth-first search · Directed adjacency graph · Reachability in a directed graph

Proof usesEdge of a directed adjacency graph · Walks of a given length · Reachability by walks · 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 byMaximality of the Edmonds–Karp flow · The Edmonds–Karp flow value equals its residual cut capacity · The Edmonds-Karp residual cut separates source and sink · Path reconstruction fails exactly at unreachable vertices · Reconstructed BFS paths are shortest paths · Cost of path reconstruction for a reachable vertex · Cost of path reconstruction for an unreachable vertex

TheoremBFS discovers each vertex at most once#✓fully proved

For every finite directed graph \(G\) with ordered adjacency lists and every vertex \(s\), no vertex occurs twice in the first-discovery order of breadth-first search from \(s\).

theorem order_nodup (g : DirectedAdjacency V) (s : V) :
    (bfs g s).order.Nodup

Uses 9 · Used by 1

Statement usesResult of breadth-first search · Breadth-first search · Directed adjacency graph

Proof usesEdge of a directed adjacency graph · Walks of a given length · 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 byLinear bound on the cost of BFS with parents

TheoremBFS reports exactly the shortest walk length#✓fully proved

For every finite directed graph \(G\) with ordered adjacency lists, all vertices \(s\) and \(v\), and every natural number \(d\), breadth-first search from \(s\) reports distance \(d\) for \(v\) if and only if there is a walk of exactly \(d\) edges from \(s\) to \(v\) in \(G\) and \(d \le k\) for every natural number \(k\) such that there is a walk of exactly \(k\) edges from \(s\) to \(v\).

theorem distance_eq_some_iff_shortest (g : DirectedAdjacency V) (s v : V) (d : Nat) :
    (bfs g s).distance v = some d ↔
      Walk g d s v ∧ ∀ k, Walk g k s v → d ≤ k

Uses 11 · Used by 3

Statement usesResult of breadth-first search · Breadth-first search · Directed adjacency graph · Walks of a given length

Proof usesEdge of a directed adjacency graph · Reachability in a directed graph · Reachability by walks · 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 byThe shortest-path search succeeds exactly when the sink is reachable · Soundness of the shortest-path search · Reconstructed BFS paths are shortest paths

TheoremBreadth-first search places the source at distance zero#✓fully proved

For every finite directed graph \(G\) given by ordered adjacency lists and every vertex \(s\) of \(G\), breadth-first search in \(G\) from \(s\) reports a distance for \(s\) itself, and that distance is \(0\) edges.

theorem source_distance (g : DirectedAdjacency V) (s : V) :
    (bfs g s).distance s = some 0

Uses 8

Statement usesResult of breadth-first search · Breadth-first search · Directed adjacency graph

Proof usesEdge of a directed adjacency graph · Walks of a given length · Contents of a two-list queue · Enqueueing appends to the contents · A successful dequeue splits off the first element

TheoremBFS discovers vertices in nondecreasing distance#✓fully proved

For every finite directed graph \(G\) with ordered adjacency lists and every vertex \(s\), the distances reported by breadth-first search from \(s\), listed along its first-discovery order, form a nondecreasing sequence, where a vertex without a reported distance counts as \(0\).

theorem order_distances_nondecreasing (g : DirectedAdjacency V) (s : V) :
    (((bfs g s).order.map fun v => (bfs g s).distance v |>.getD 0).Pairwise (· ≤ ·))

Uses 9

Statement usesResult of breadth-first search · Breadth-first search · Directed adjacency graph

Proof usesEdge of a directed adjacency graph · Walks of a given length · 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

StructureBreadth-first search forest#✓fully proved

A breadth-first search forest on a vertex type \(V\) consists of a breadth-first search result, namely a partial distance function from \(V\) to the natural numbers and a list of vertices, together with a partial predecessor function from \(V\) to \(V\). For a search from a source vertex \(s\), these are meant to give the distance from \(s\) of each reachable vertex, the reachable vertices in first-discovery order, and the vertex from which each reachable vertex other than \(s\) was first discovered, with \(s\) and the unreachable vertices having no predecessor; the structure itself imposes none of these properties.

public structure BFSForest (V : Type u) extends BFSResult V where
  /-- The source and unreachable vertices have no predecessor. -/
  predecessor : V → Option V

Uses 1 · Used by 17

Statement usesResult of breadth-first search

Used byBreadth-first search with parent pointers · Breadth-first search with parents returns the ordinary BFS result · Exact cost of BFS with parents · Linear bound on the cost of BFS with parents · Path reconstruction from BFS parents · Path reconstruction fails exactly at unreachable vertices · Path reconstruction at the source · Reconstructed BFS paths are shortest paths · Cost of path reconstruction for a reachable vertex · Cost of path reconstruction for an unreachable vertex · Saved-parent chains are simple · Each reachable vertex has a unique saved-parent chain · A BFS parent is one step closer to the source · BFS parents are joined by graph edges · The BFS parent is the first discovered in-neighbour · Exactly the source and the unreachable vertices have no BFS parent · The saved-parent relation is acyclic

DefinitionBreadth-first search with parent pointers#✓fully proved

Given a finite directed graph \(G\) on a vertex type \(V\), with ordered adjacency lists, and a source vertex \(s\), this runs first-in-first-out breadth-first search from \(s\) for \(|V|\) rounds. The queue starts with \(s\) at distance \(0\). Each round tries to dequeue a vertex \(u\); if it succeeds, it scans the neighbors of \(u\) in adjacency-list order, and each neighbor not yet discovered gets distance one more than \(u\), records \(u\) as its parent and is enqueued. An already discovered vertex keeps its distance and parent. The result is the search forest: the distance of each discovered vertex, the vertices in the order they were dequeued, and the parent of each discovered vertex other than \(s\). The cost counts one unit for each dequeue attempt, each check of an adjacency entry against the discovered set, each enqueue (including that of \(s\)) and each parent write.

public def bfsWithParents {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (graph : DirectedAdjacency V) (source : V) : TimeM Nat (BFSForest V) := do
  let initial ← parentInitial source
  let final ← parentRun graph graph.vertices.length initial
  return {
    toBFSResult := {
      distance := fun vertex => final.core.2.2[vertex]?
      order := final.core.1.reverse.map Prod.fst }
    predecessor := fun vertex => final.parents[vertex]? }

Uses 3 · Used by 14

Statement usesBreadth-first search forest · Result of breadth-first search · Directed adjacency graph

Used byBreadth-first search with parents returns the ordinary BFS result · Exact cost of BFS with parents · Linear bound on the cost of BFS with parents · Path reconstruction fails exactly at unreachable vertices · Reconstructed BFS paths are shortest paths · Cost of path reconstruction for a reachable vertex · Cost of path reconstruction for an unreachable vertex · Saved-parent chains are simple · Each reachable vertex has a unique saved-parent chain · A BFS parent is one step closer to the source · BFS parents are joined by graph edges · The BFS parent is the first discovered in-neighbour · Exactly the source and the unreachable vertices have no BFS parent · The saved-parent relation is acyclic

DefinitionPath reconstruction from BFS parents#✓fully proved

Let \(p\) be the predecessor function of a breadth-first search forest, let \(n\) be the length of its discovery order, and let \(s\) and \(t\) be vertices. Starting from \(v_k = t\), this walks back along \(p\), setting \(v_{i-1} = p(v_i)\), until it reaches a vertex \(v_0\) that tests equal to \(s\), and returns the list \(v_0, v_1, \dots, v_k\). It returns no list if the walk meets a vertex that does not test equal to \(s\) and has no predecessor, or if none of the first \(n + 1\) vertices \(t, p(t), \dots\) of the walk tests equal to \(s\). The cost counts one unit for each test against \(s\), each predecessor lookup and each vertex prepended to the list.

The bound \(n\) makes the walk terminate even when the predecessor table contains a cycle.

public def BFSForest.pathTo? {V : Type u} [BEq V]
    (forest : BFSForest V) (source target : V) : TimeM Nat (Option (List V)) :=
  followParents forest.predecessor source forest.order.length target []

Uses 2 · Used by 5

Statement usesBreadth-first search forest · Result of breadth-first search

Used byPath reconstruction fails exactly at unreachable vertices · Path reconstruction at the source · Reconstructed BFS paths are shortest paths · Cost of path reconstruction for a reachable vertex · Cost of path reconstruction for an unreachable vertex

TheoremBreadth-first search with parents returns the ordinary BFS result#✓fully proved

For every finite directed graph \(G\) with ordered adjacency lists and every source vertex \(s\), the output of breadth-first search with parents from \(s\) in \(G\), with its cost and its predecessor table forgotten, equals the result of ordinary FIFO breadth-first search from \(s\) in \(G\): the same distance table and the same first-discovery order.

public theorem bfsWithParents_ret {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (graph : DirectedAdjacency V) (source : V) :
    (bfsWithParents graph source).ret.toBFSResult = bfs graph source

Uses 5 · Used by 9

Statement usesBreadth-first search forest · Result of breadth-first search · Breadth-first search · Breadth-first search with parent pointers · Directed adjacency graph

Used byExact cost of BFS with parents · Path reconstruction fails exactly at unreachable vertices · Reconstructed BFS paths are shortest paths · Cost of path reconstruction for a reachable vertex · Cost of path reconstruction for an unreachable vertex · Saved-parent chains are simple · Each reachable vertex has a unique saved-parent chain · The BFS parent is the first discovered in-neighbour · Exactly the source and the unreachable vertices have no BFS parent

TheoremExactly the source and the unreachable vertices have no BFS parent#✓fully proved

Let \(G\) be a finite directed graph with ordered adjacency lists, \(s\) a vertex, and \(F\) the predecessor forest computed by breadth-first search with parents from \(s\) in \(G\). A vertex \(v\) has no recorded predecessor in \(F\) if and only if \(v = s\) or \(v\) is not reachable from \(s\) along directed edges of \(G\).

public theorem predecessor_eq_none_iff {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (graph : DirectedAdjacency V) (source vertex : V) :
    (bfsWithParents graph source).ret.predecessor vertex = none ↔
      vertex = source ∨ ¬ graph.Reachable source vertex

Uses 12 · Used by 2

Statement usesBreadth-first search forest · Breadth-first search with parent pointers · Directed adjacency graph · Reachability in a directed graph

Proof usesResult of breadth-first search · Breadth-first search · Breadth-first search with parents returns the ordinary BFS result · BFS reports a distance exactly for the reachable vertices · Edge of a directed adjacency graph · Contents of a two-list queue · Enqueueing appends to the contents · A successful dequeue splits off the first element

Used byPath reconstruction fails exactly at unreachable vertices · Cost of path reconstruction for an unreachable vertex

TheoremBFS parents are joined by graph edges#✓fully proved

Let \(G\) be a finite directed graph with ordered adjacency lists, \(s\) a vertex, and \(F\) the predecessor forest computed by breadth-first search with parents from \(s\) in \(G\). If \(F\) records \(p\) as the predecessor of a vertex \(v\), then \(G\) has a directed edge from \(p\) to \(v\), that is, \(v\) occurs in the adjacency list of \(p\).

public theorem predecessor_edge {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (graph : DirectedAdjacency V) (source vertex parent : V)
    (found : (bfsWithParents graph source).ret.predecessor vertex = some parent) :
    graph.Edge parent vertex

Uses 7 · Used by 4

Statement usesBreadth-first search forest · Breadth-first search with parent pointers · Directed adjacency graph · Edge of a directed adjacency graph

Proof usesContents of a two-list queue · Enqueueing appends to the contents · A successful dequeue splits off the first element

Used byPath reconstruction fails exactly at unreachable vertices · Reconstructed BFS paths are shortest paths · Cost of path reconstruction for a reachable vertex · Saved-parent chains are simple

TheoremA BFS parent is one step closer to the source#✓fully proved

Let \(G\) be a finite directed graph with ordered adjacency lists, \(s\) a vertex, and \(F\) the predecessor forest computed by breadth-first search with parents from \(s\) in \(G\). If \(F\) records \(p\) as the predecessor of a vertex \(v\), then there is a natural number \(d\) such that \(F\) records distance \(d\) for \(p\) and distance \(d + 1\) for \(v\).

public theorem predecessor_distance {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (graph : DirectedAdjacency V) (source vertex parent : V)
    (found : (bfsWithParents graph source).ret.predecessor vertex = some parent) :
    ∃ distance : Nat,
      (bfsWithParents graph source).ret.distance parent = some distance ∧
      (bfsWithParents graph source).ret.distance vertex = some (distance + 1)

Uses 8

Statement usesBreadth-first search forest · Result of breadth-first search · Breadth-first search with parent pointers · Directed adjacency graph

Proof usesEdge of a directed adjacency graph · Contents of a two-list queue · Enqueueing appends to the contents · A successful dequeue splits off the first element

TheoremThe BFS parent is the first discovered in-neighbour#✓fully proved

Let \(G\) be a finite directed graph with ordered adjacency lists, \(s\) a vertex, and \(F\) the predecessor forest computed by breadth-first search with parents from \(s\) in \(G\). For every vertex \(v \ne s\), the predecessor that \(F\) records for \(v\) is the first vertex \(u\), in the first-discovery order of ordinary FIFO breadth-first search from \(s\) in \(G\), whose adjacency list contains \(v\); if no vertex in that order has \(v\) in its adjacency list, \(F\) records no predecessor for \(v\).

public theorem predecessor_eq_find? {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (graph : DirectedAdjacency V) (source vertex : V) (nonsource : vertex ≠ source) :
    (bfsWithParents graph source).ret.predecessor vertex =
      (bfs graph source).order.find?
        (fun parent => (graph.adjacency parent).contains vertex)

Uses 10

Statement usesBreadth-first search forest · Result of breadth-first search · Breadth-first search · Breadth-first search with parent pointers · Directed adjacency graph

Proof usesBreadth-first search with parents returns the ordinary BFS result · Edge of a directed adjacency graph · Contents of a two-list queue · Enqueueing appends to the contents · A successful dequeue splits off the first element

TheoremEach reachable vertex has a unique saved-parent chain#✓fully proved

Let \(G\) be a finite directed graph given by adjacency lists, and let \(s\) and \(v\) be vertices with \(v\) reachable from \(s\) in \(G\). There is exactly one list of vertices that starts at \(s\), ends at \(v\), and in which each vertex after the first has the preceding vertex as its saved parent in the breadth-first search forest of \(G\) from \(s\).

public theorem predecessor_chain_unique {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (graph : DirectedAdjacency V) (source vertex : V)
    (reachable : graph.Reachable source vertex) :
    ∃! chain : List V, chain.IsChainFromTo
      (fun parent child => (bfsWithParents graph source).ret.predecessor child = some parent)
      source vertex

Uses 12

Statement usesBreadth-first search forest · Breadth-first search with parent pointers · Directed adjacency graph · Reachability in a directed graph

Proof usesResult of breadth-first search · Breadth-first search · Breadth-first search with parents returns the ordinary BFS result · BFS reports a distance exactly for the reachable vertices · Edge of a directed adjacency graph · Contents of a two-list queue · Enqueueing appends to the contents · A successful dequeue splits off the first element

TheoremSaved-parent chains are simple#✓fully proved

Let \(G\) be a finite directed graph given by adjacency lists and let \(s\) and \(v\) be vertices. If a list of vertices starts at \(s\), ends at \(v\), and each of its vertices after the first has the preceding vertex as its saved parent in the breadth-first search forest of \(G\) from \(s\), then no vertex occurs twice in the list.

public theorem predecessor_chain_nodup {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (graph : DirectedAdjacency V) (source vertex : V) (chain : List V)
    (linked : chain.IsChainFromTo
      (fun parent child => (bfsWithParents graph source).ret.predecessor child = some parent)
      source vertex) :
    chain.Nodup

Uses 13 · Used by 3

Statement usesBreadth-first search forest · Breadth-first search with parent pointers · Directed adjacency graph

Proof usesResult of breadth-first search · Breadth-first search · Breadth-first search with parents returns the ordinary BFS result · BFS reports a distance exactly for the reachable vertices · BFS parents are joined by graph edges · Edge of a directed adjacency graph · Reachability in a directed graph · Contents of a two-list queue · Enqueueing appends to the contents · A successful dequeue splits off the first element

Used byPath reconstruction fails exactly at unreachable vertices · Reconstructed BFS paths are shortest paths · Cost of path reconstruction for a reachable vertex

TheoremThe saved-parent relation is acyclic#✓fully proved

Let \(G\) be a finite directed graph given by adjacency lists and let \(s\) and \(v\) be vertices. In the breadth-first search forest of \(G\) from \(s\), there is no sequence \(v = x_0, x_1, \dots, x_k = v\) with \(k \ge 1\) in which each \(x_i\) is the saved parent of \(x_{i+1}\).

public theorem predecessor_relation_acyclic {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (graph : DirectedAdjacency V) (source vertex : V) :
    ¬ Relation.TransGen
      (fun parent child => (bfsWithParents graph source).ret.predecessor child = some parent)
      vertex vertex

Uses 7

Statement usesBreadth-first search forest · Breadth-first search with parent pointers · Directed adjacency graph

Proof usesEdge of a directed adjacency graph · Contents of a two-list queue · Enqueueing appends to the contents · A successful dequeue splits off the first element

TheoremPath reconstruction at the source#✓fully proved

For every breadth-first search forest \(F\) and every vertex \(s\), following the saved parents of \(F\) from \(s\) back to \(s\) returns the one-vertex path \([s]\). This holds for every forest, including one whose discovery order is empty.

public theorem BFSForest.pathTo?_source {V : Type u} [BEq V] [ReflBEq V]
    (forest : BFSForest V) (source : V) :
    (forest.pathTo? source source).ret = some [source]

Uses 3

Statement usesBreadth-first search forest · Path reconstruction from BFS parents

Proof usesResult of breadth-first search

TheoremPath reconstruction fails exactly at unreachable vertices#✓fully proved

Let \(G\) be a finite directed graph given by adjacency lists, and let \(s\) and \(v\) be vertices. Following the saved parents of the breadth-first search forest of \(G\) from \(s\) back from \(v\) towards \(s\) returns no path if and only if \(v\) is not reachable from \(s\) in \(G\).

public theorem BFSForest.pathTo?_eq_none_iff {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (graph : DirectedAdjacency V) (source vertex : V) :
    ((bfsWithParents graph source).ret.pathTo? source vertex).ret = none ↔
      ¬ graph.Reachable source vertex

Uses 17 · Used by 1

Statement usesBreadth-first search forest · Path reconstruction from BFS parents · Breadth-first search with parent pointers · Directed adjacency graph · Reachability in a directed graph

Proof usesResult of breadth-first search · Breadth-first search · Breadth-first search with parents returns the ordinary BFS result · BFS reports a distance exactly for the reachable vertices · BFS lists exactly the reachable vertices · Saved-parent chains are simple · BFS parents are joined by graph edges · Exactly the source and the unreachable vertices have no BFS parent · Edge of a directed adjacency graph · Contents of a two-list queue · Enqueueing appends to the contents · A successful dequeue splits off the first element

Used byReconstructed BFS paths are shortest paths

TheoremReconstructed BFS paths are shortest paths#✓fully proved

Let \(G\) be a finite directed graph given by adjacency lists, let \(s\) and \(v\) be vertices, and suppose that following the saved parents of the breadth-first search forest of \(G\) from \(s\) back from \(v\) returns a list \(P\) of vertices. Then \(P\) starts at \(s\) and ends at \(v\), each vertex of \(P\) after the first has the preceding vertex as its saved parent, \(G\) has an edge from each vertex of \(P\) to the next, no vertex occurs twice in \(P\), breadth-first search from \(s\) reports a distance \(d\) for \(v\) and \(P\) has \(d + 1\) vertices, and every list of vertices from \(s\) to \(v\) such that \(G\) has an edge from each of its vertices to the next has at least as many vertices as \(P\).

public theorem BFSForest.pathTo?_spec {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (graph : DirectedAdjacency V) (source vertex : V) (chain : List V)
    (returned : ((bfsWithParents graph source).ret.pathTo? source vertex).ret = some chain) :
    chain.IsChainFromTo
        (fun parent child => (bfsWithParents graph source).ret.predecessor child = some parent)
        source vertex ∧
      chain.IsChainFromTo graph.Edge source vertex ∧ chain.Nodup ∧
      (∃ distance : Nat, (bfs graph source).distance vertex = some distance ∧
        chain.length = distance + 1) ∧
      ∀ other : List V, other.IsChainFromTo graph.Edge source vertex →
        chain.length ≤ other.length

Uses 19

Statement usesBreadth-first search forest · Path reconstruction from BFS parents · Result of breadth-first search · Breadth-first search · Breadth-first search with parent pointers · Directed adjacency graph · Edge of a directed adjacency graph

Proof usesPath reconstruction fails exactly at unreachable vertices · Breadth-first search with parents returns the ordinary BFS result · BFS reports exactly the shortest walk length · BFS reports a distance exactly for the reachable vertices · BFS lists exactly the reachable vertices · Saved-parent chains are simple · BFS parents are joined by graph edges · Reachability in a directed graph · Walks of a given length · Contents of a two-list queue · Enqueueing appends to the contents · A successful dequeue splits off the first element

TheoremCost of path reconstruction for a reachable vertex#✓fully proved

Let \(G\) be a finite directed graph given by adjacency lists, let \(s\) and \(v\) be vertices, and suppose breadth-first search from \(s\) reports distance \(d\) for \(v\). Following the saved parents of the breadth-first search forest of \(G\) from \(s\) back from \(v\) costs exactly \(3d + 2\), counting one unit for each comparison with \(s\), each parent lookup and each vertex prepended to the path.

public theorem BFSForest.pathTo?_time {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (graph : DirectedAdjacency V) (source vertex : V) (distance : Nat)
    (found : (bfs graph source).distance vertex = some distance) :
    ((bfsWithParents graph source).ret.pathTo? source vertex).time =
      3 * distance + 2

Uses 15

Statement usesBreadth-first search forest · Path reconstruction from BFS parents · Result of breadth-first search · Breadth-first search · Breadth-first search with parent pointers · Directed adjacency graph

Proof usesBreadth-first search with parents returns the ordinary BFS result · BFS lists exactly the reachable vertices · Saved-parent chains are simple · BFS parents are joined by graph edges · Edge of a directed adjacency graph · Reachability in a directed graph · Contents of a two-list queue · Enqueueing appends to the contents · A successful dequeue splits off the first element

TheoremCost of path reconstruction for an unreachable vertex#✓fully proved

Let \(G\) be a finite directed graph given by adjacency lists, and let \(s\) and \(v\) be vertices with \(v\) not reachable from \(s\) in \(G\). Following the saved parents of the breadth-first search forest of \(G\) from \(s\) back from \(v\) costs exactly \(2\), counting one unit for each comparison with \(s\), each parent lookup and each vertex prepended to the path: one comparison of \(v\) with \(s\) and one lookup of the missing parent of \(v\).

public theorem BFSForest.pathTo?_time_of_not_reachable
    {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (graph : DirectedAdjacency V) (source vertex : V)
    (unreachable : ¬ graph.Reachable source vertex) :
    ((bfsWithParents graph source).ret.pathTo? source vertex).time = 2

Uses 11

Statement usesBreadth-first search forest · Path reconstruction from BFS parents · Breadth-first search with parent pointers · Directed adjacency graph · Reachability in a directed graph

Proof usesResult of breadth-first search · Breadth-first search · Breadth-first search with parents returns the ordinary BFS result · BFS lists exactly the reachable vertices · Exactly the source and the unreachable vertices have no BFS parent · Edge of a directed adjacency graph

TheoremExact cost of BFS with parents#✓fully proved

Let \(G\) be a finite directed graph with vertex list \(V\) and adjacency lists \(\mathrm{adj}(u)\), let \(s\) be a vertex, and let \(L\) be the list of vertices in the order in which breadth-first search from \(s\) discovers them. The cost of breadth-first search with parents from \(s\), counting dequeue attempts, adjacency checks, enqueues and parent writes, equals \(|V| + \sum_{u \in L} |\mathrm{adj}(u)| + |L| + (|L| - 1)\), where adjacency lists are counted with repetitions and \(|L| - 1\) is truncated at \(0\).

public theorem bfsWithParents_time {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (graph : DirectedAdjacency V) (source : V) :
    (bfsWithParents graph source).time =
      graph.vertices.length +
        ((bfs graph source).order.map fun vertex => (graph.adjacency vertex).length).sum +
        (bfs graph source).order.length + ((bfs graph source).order.length - 1)

Uses 11 · Used by 1

Statement usesBreadth-first search forest · Result of breadth-first search · Breadth-first search · Breadth-first search with parent pointers · Directed adjacency graph

Proof usesBreadth-first search with parents returns the ordinary BFS result · Edge of a directed adjacency graph · 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 byLinear bound on the cost of BFS with parents

TheoremLinear bound on the cost of BFS with parents#✓fully proved

Let \(G\) be a finite directed graph with vertex list \(V\) and adjacency lists \(\mathrm{adj}(u)\), and let \(s\) be a vertex. The cost of breadth-first search with parents from \(s\), counting dequeue attempts, adjacency checks, enqueues and parent writes, is at most \(3|V| + \sum_{u \in V} |\mathrm{adj}(u)|\), where adjacency lists are counted with repetitions.

public theorem bfsWithParents_time_le {V : Type u} [BEq V] [Hashable V] [LawfulBEq V]
    (graph : DirectedAdjacency V) (source : V) :
    (bfsWithParents graph source).time ≤
      3 * graph.vertices.length +
        (graph.vertices.map fun vertex => (graph.adjacency vertex).length).sum

Uses 7

Statement usesBreadth-first search forest · Breadth-first search with parent pointers · Directed adjacency graph

Proof usesResult of breadth-first search · Breadth-first search · Exact cost of BFS with parents · BFS discovers each vertex at most once

29 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.