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.

Main definitions

• Cslib.Reachability.expand: one round of breadth-first search.
• Cslib.Reachability.search: a number of rounds from a start element.

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: after as many rounds as there are reachable elements, the found elements are the reachable ones.

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]

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

theorem Cslib.Reachability.prefix_foldl_insertNew {α : Type u_1} [DecidableEq α] (l found : List α) : found <+: List.foldl insertNew found l

theorem Cslib.Reachability.mem_foldl_insertNew {α : Type u_1} [DecidableEq α] {l found : List α} {a : α} : a ∈ List.foldl insertNew found l ↔ a ∈ found ∨ a ∈ l

theorem Cslib.Reachability.nodup_foldl_insertNew {α : Type u_1} [DecidableEq α] {l found : List α} (h : found.Nodup) : (List.foldl insertNew found l).Nodup

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 : α), 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 : α), b ∈ found → ∀ (a : α), a ∈ succ b → a ∈ found

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

theorem Cslib.Reachability.length_lt_expand {α : Type u_1} [DecidableEq α] {succ : α → List α} {found : List α} (h : expand succ found ≠ found) : found.length < (expand succ found).length

A round that adds something makes the list longer.

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.succ_le_length_search_or_closed {α : Type u_1} [DecidableEq α] {succ : α → List α} (rounds : ℕ) (start : α) : rounds + 1 ≤ (search succ rounds start).length ∨ expand succ (search succ rounds start) = search succ rounds start

Each round before the found elements are closed finds a new element.

theorem Cslib.Reachability.mem_search_iff {α : Type u_1} [DecidableEq α] {succ : α → List α} {rounds bound : ℕ} {start a : α} (hbound : ∀ (l : List α), l.Nodup → (∀ (b : α), 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.