Breadth-first search by rounds

A round of breadth-first search (Cslib.Reachability.expand) appends to the list of the elements found so far every successor of one of them that has not been found yet. The found elements stay distinct, a round only appends, and a round adds nothing exactly when the found elements are closed under successors. So if at most N distinct elements are reachable from start, after N rounds from [start] (Cslib.Reachability.search) the found elements are exactly the reachable ones (Cslib.Reachability.mem_search_iff): each round before closure finds a new element. The number of rounds, not a search for a fixed point, keeps the algorithm a plain iteration, as polynomial-time certificates need. When no bound on the number of reachable elements is known in advance, the search runs until a round adds nothing: the closing round (Cslib.Reachability.closingRound) is the least number of rounds after which the found elements are closed, and they are then exactly the reachable ones (Cslib.Reachability.mem_search_iff_of_closed).

Main definitions

• Cslib.Reachability.insertNew: append an element to a list if not already present.
• Cslib.Reachability.expand: one round of breadth-first search.
• Cslib.Reachability.search: a number of rounds from a start element.
• Cslib.Reachability.closingRound: the least number of rounds after which the search is closed.

Main results

• Cslib.Reachability.nodup_search: the found elements are distinct.
• Cslib.Reachability.reflTransGen_of_mem_search: the found elements are reachable.
• Cslib.Reachability.mem_search_iff_of_closed: once a round adds nothing, the found elements are the reachable ones.
• Cslib.Reachability.expand_search_eq_of_bound, Cslib.Reachability.mem_search_iff: after as many rounds as there are reachable elements, the search is closed and the found elements are the reachable ones.
• Cslib.Reachability.closingRound_le, Cslib.Reachability.expand_search_ne_of_lt_closingRound: the closing round is the least round after which the search is closed.

References

• M. Sipser, Introduction to the Theory of Computation, Theorem 7.14

def Cslib.Reachability.insertNew {α : Type u_1} [DecidableEq α] (found : List α) (a : α) : List α

Append an element unless it is already in the list.

def Cslib.Reachability.expand {α : Type u_1} [DecidableEq α] (succ : α → List α) (found : List α) : List α

One round of breadth-first search: append, in order, every successor of a found element that has not been found yet.

def Cslib.Reachability.search {α : Type u_1} [DecidableEq α] (succ : α → List α) (rounds : ℕ) (start : α) : List α

rounds rounds of breadth-first search from start.

@[simp]

theorem Cslib.Reachability.search_zero {α : Type u_1} [DecidableEq α] {succ : α → List α} (start : α) : search succ 0 start = [start]

Zero rounds of breadth-first search return the singleton list [start].

theorem Cslib.Reachability.search_succ {α : Type u_1} [DecidableEq α] {succ : α → List α} (rounds : ℕ) (start : α) : search succ (rounds + 1) start = expand succ (search succ rounds start)

rounds + 1 rounds of breadth-first search apply expand to the result of rounds rounds.

theorem Cslib.Reachability.prefix_expand {α : Type u_1} [DecidableEq α] {succ : α → List α} (found : List α) : found <+: expand succ found

A round only appends.

theorem Cslib.Reachability.mem_expand {α : Type u_1} [DecidableEq α] {succ : α → List α} {found : List α} {a : α} : a ∈ expand succ found ↔ a ∈ found ∨ ∃ b ∈ found, a ∈ succ b

The elements found after a round are those found before and their successors.

theorem Cslib.Reachability.nodup_expand {α : Type u_1} [DecidableEq α] {succ : α → List α} {found : List α} (h : found.Nodup) : (expand succ found).Nodup

A round keeps the found elements distinct.

theorem Cslib.Reachability.expand_eq_self_iff {α : Type u_1} [DecidableEq α] {succ : α → List α} {found : List α} : expand succ found = found ↔ ∀ b ∈ found, ∀ a ∈ succ b, a ∈ found

A round adds nothing exactly when the found elements are closed under successors.

theorem Cslib.Reachability.prefix_search {α : Type u_1} [DecidableEq α] {succ : α → List α} {i j : ℕ} (hij : i ≤ j) (start : α) : search succ i start <+: search succ j start

The rounds only append.

theorem Cslib.Reachability.start_mem_search {α : Type u_1} [DecidableEq α] {succ : α → List α} (rounds : ℕ) (start : α) : start ∈ search succ rounds start

theorem Cslib.Reachability.nodup_search {α : Type u_1} [DecidableEq α] {succ : α → List α} (rounds : ℕ) (start : α) : (search succ rounds start).Nodup

The found elements are distinct.

theorem Cslib.Reachability.reflTransGen_of_mem_search {α : Type u_1} [DecidableEq α] {succ : α → List α} {rounds : ℕ} {start a : α} (h : a ∈ search succ rounds start) : Relation.ReflTransGen (fun (b c : α) => c ∈ succ b) start a

The found elements are reachable.

theorem Cslib.Reachability.mem_search_iff_of_closed {α : Type u_1} [DecidableEq α] {succ : α → List α} {rounds : ℕ} {start a : α} (hclosed : expand succ (search succ rounds start) = search succ rounds start) : a ∈ search succ rounds start ↔ Relation.ReflTransGen (fun (b c : α) => c ∈ succ b) start a

A closed round finds every reachable element: once a round adds nothing, the found elements are exactly those reachable from start.

theorem Cslib.Reachability.expand_search_eq_of_bound {α : Type u_1} [DecidableEq α] {succ : α → List α} {rounds bound : ℕ} {start : α} (hbound : ∀ (l : List α), l.Nodup → (∀ b ∈ l, Relation.ReflTransGen (fun (b c : α) => c ∈ succ b) start b) → l.length ≤ bound) (hrounds : bound ≤ rounds) : expand succ (search succ rounds start) = search succ rounds start

Breadth-first search closes within as many rounds as there are reachable elements: if every list of distinct elements reachable from start has at most bound entries, a round after at least bound rounds adds nothing.

theorem Cslib.Reachability.mem_search_iff {α : Type u_1} [DecidableEq α] {succ : α → List α} {rounds bound : ℕ} {start a : α} (hbound : ∀ (l : List α), l.Nodup → (∀ b ∈ l, Relation.ReflTransGen (fun (b c : α) => c ∈ succ b) start b) → l.length ≤ bound) (hrounds : bound ≤ rounds) : a ∈ search succ rounds start ↔ Relation.ReflTransGen (fun (b c : α) => c ∈ succ b) start a

After as many rounds as there are reachable elements, the found elements are the reachable ones. If every list of distinct elements reachable from start has at most bound entries, then after at least bound rounds the found elements are closed under successors, so they include every reachable element.

Searching until closed

noncomputable def Cslib.Reachability.closingRound {α : Type u_1} [DecidableEq α] (succ : α → List α) (start : α) : ℕ

The closing round: the least number of rounds after which a round from start adds nothing, or 0 if the search never closes. Searching until closed takes this many rounds, a number that need not be known in advance.

theorem Cslib.Reachability.expand_search_closingRound {α : Type u_1} [DecidableEq α] {succ : α → List α} {rounds : ℕ} {start : α} (h : expand succ (search succ rounds start) = search succ rounds start) : expand succ (search succ (closingRound succ start) start) = search succ (closingRound succ start) start

The search is closed after the closing round, if it ever closes.

theorem Cslib.Reachability.closingRound_le {α : Type u_1} [DecidableEq α] {succ : α → List α} {rounds : ℕ} {start : α} (h : expand succ (search succ rounds start) = search succ rounds start) : closingRound succ start ≤ rounds

The closing round is at most any round after which the search is closed.

theorem Cslib.Reachability.expand_search_ne_of_lt_closingRound {α : Type u_1} [DecidableEq α] {succ : α → List α} {rounds : ℕ} {start : α} (h : rounds < closingRound succ start) : expand succ (search succ rounds start) ≠ search succ rounds start

Before the closing round, every round finds a new element.