The rounds of breadth-first search and inductive counting

Round n of the breadth-first search of a relation r from a is the set Relation.reachableWithin r a n of elements reached within n steps. The rounds grow, each is the previous one together with its successors, and once a round adds nothing it is the set of all reachable elements; on a finite type with N elements, round N - 1 already is.

The method of inductive counting of Immerman and Szelepcsényi certifies that an element is not reachable, using only the sizes of the rounds. Its principle is that a subset of a finite set with at least as many elements is the whole set (Set.eq_of_subset_of_ncard_le). So a list of distinct members of round n, with at least as many entries as the round has members, contains every member of the round (Relation.IsRoundList), and an element missing from such a list is outside the round. Membership of each entry is itself certified by a walk of exactly n steps that may stay put (Relation.relatesWithinSteps_iff_relatesInSteps_reflGen). A nondeterministic machine guesses such a list one entry at a time and only counts the entries, so it needs to store just the size of the round, never the round.

The statements about all reachable elements come in two forms: for a finite type, and for any type on which few elements are reachable from a (..._of_encard_le), as for the configurations of a space-bounded machine.

Nothing here mentions a machine; these are the facts about the configuration graph that the inductive counting algorithm relies on.

Main definitions

• Relation.reachableWithin: round n of the breadth-first search, as a set.
• Relation.IsRoundList: a list certifying the contents of round n by its length.

Main results

• Relation.reachableWithin_succ, Relation.reachableWithin_mono: the round recursion.
• Relation.reachableWithin_eq_of_succ_eq, Relation.reachableWithin_eq_of_card_le: a round that adds nothing, or the round with index one less than the number of elements, is the set of all reachable elements.
• Relation.IsRoundList.mem_iff, Relation.exists_isRoundList: soundness and completeness of round lists.
• Relation.not_relatesWithinSteps_succ_iff: the inductive counting step, which certifies that an element is outside round n + 1 by a list for round n.
• Relation.forall_reflTransGen_iff_exists_isRoundList, Relation.not_reflTransGen_iff_exists_isRoundList: on a finite type, unreachability as a certificate.

References

• M. Sipser, Introduction to the Theory of Computation, Section 8.6
• C. H. Papadimitriou, Computational Complexity, Section 7.3

The rounds of breadth-first search

def Relation.reachableWithin {α : Type u_1} (r : α → α → Prop) (a : α) (n : ℕ) : Set α

Round n of the breadth-first search of r from a: the elements that r relates to a within n steps.

@[simp]

theorem Relation.mem_reachableWithin {α : Type u_1} {r : α → α → Prop} {a b : α} {n : ℕ} : b ∈ reachableWithin r a n ↔ RelatesWithinSteps r a b n

An element is in round n exactly when r relates a to it within n steps.

@[simp]

theorem Relation.reachableWithin_zero {α : Type u_1} {r : α → α → Prop} {a : α} : reachableWithin r a 0 = {a}

Round 0 consists of the starting element.

theorem Relation.mem_reachableWithin_succ {α : Type u_1} {r : α → α → Prop} {a c : α} {n : ℕ} : c ∈ reachableWithin r a (n + 1) ↔ ∃ b ∈ reachableWithin r a n, ReflGen r b c

An element is in round n + 1 exactly when it is at most one step away from round n.

theorem Relation.reachableWithin_succ {α : Type u_1} {r : α → α → Prop} {a : α} {n : ℕ} : reachableWithin r a (n + 1) = reachableWithin r a n ∪ {c : α | ∃ b ∈ reachableWithin r a n, r b c}

The round recursion. Round n + 1 is round n together with the successors of its members.

theorem Relation.reachableWithin_mono {α : Type u_1} {r : α → α → Prop} {a : α} : Monotone (reachableWithin r a)

The rounds grow.

theorem Relation.reachableWithin_subset_setOf_reflTransGen {α : Type u_1} {r : α → α → Prop} {a : α} {n : ℕ} : reachableWithin r a n ⊆ {b : α | ReflTransGen r a b}

Every round consists of reachable elements.

theorem Relation.iUnion_reachableWithin {α : Type u_1} {r : α → α → Prop} {a : α} : ⋃ (n : ℕ), reachableWithin r a n = {b : α | ReflTransGen r a b}

Every reachable element is in some round.

theorem Relation.reachableWithin_eq_of_succ_eq {α : Type u_1} {r : α → α → Prop} {a : α} {n : ℕ} (h : reachableWithin r a (n + 1) = reachableWithin r a n) : reachableWithin r a n = {b : α | ReflTransGen r a b}

A round that adds nothing is final. Once round n + 1 equals round n, round n contains every reachable element, so breadth-first search may stop.

theorem Relation.reachableWithin_eq_of_encard_le {α : Type u_1} {r : α → α → Prop} {a : α} {N : ℕ} (hN : {x : α | ReflTransGen r a x}.encard ≤ ↑N + 1) : reachableWithin r a N = {b : α | ReflTransGen r a b}

Round N contains every reachable element once at most N + 1 elements are reachable.

theorem Relation.finite_reachableWithin_of_encard_le {α : Type u_1} {r : α → α → Prop} {a : α} {N : ℕ} (hN : {x : α | ReflTransGen r a x}.encard ≤ ↑N + 1) : (reachableWithin r a N).Finite

Round N is finite once at most N + 1 elements are reachable.

theorem Relation.reachableWithin_eq_of_card_le {α : Type u_1} {r : α → α → Prop} {a : α} {N : ℕ} [Finite α] (hN : Nat.card α ≤ N + 1) : reachableWithin r a N = {b : α | ReflTransGen r a b}

On a finite type, the round with index one less than the number of elements contains every reachable element.

theorem Relation.finite_reachableWithin {α : Type u_1} {r : α → α → Prop} {a : α} (hr : ∀ (b : α), {c : α | r b c}.Finite) (n : ℕ) : (reachableWithin r a n).Finite

If every element has finitely many successors, every round is finite.

Round lists

structure Relation.IsRoundList {α : Type u_1} (r : α → α → Prop) (a : α) (n : ℕ) (l : List α) : Prop

A list certifying the contents of round n of the search from a: distinct members of the round, at least as many as the round has. The counting principle makes the list exhaustive (Relation.IsRoundList.mem_iff), so that an element missing from it is outside the round; this is the certificate that the inductive counting algorithm guesses one entry at a time Sipser, Theorem 8.27.

• nodup : l.Nodup

  The entries are distinct.

• relatesWithinSteps (b : α) : b ∈ l → RelatesWithinSteps r a b n

  Every entry is in round n.

• encard_le : (reachableWithin r a n).encard ≤ ↑l.length

  There are at least as many entries as members of round n.

theorem Relation.IsRoundList.of_ncard_le {α : Type u_1} {r : α → α → Prop} {a : α} {n : ℕ} {l : List α} (hfin : (reachableWithin r a n).Finite) (hnodup : l.Nodup) (hl : ∀ b ∈ l, RelatesWithinSteps r a b n) (hcard : (reachableWithin r a n).ncard ≤ l.length) : IsRoundList r a n l

A list of distinct members of a finite round, as many as the round has, is a round list: the form in which the count is a natural number.

theorem Relation.IsRoundList.setOf_mem_eq {α : Type u_1} {r : α → α → Prop} {a : α} {n : ℕ} {l : List α} (hl : IsRoundList r a n l) : {b : α | b ∈ l} = reachableWithin r a n

Round lists are sound. By the counting principle, a round list contains every member of the round.

theorem Relation.IsRoundList.mem_iff {α : Type u_1} {r : α → α → Prop} {a b : α} {n : ℕ} {l : List α} (hl : IsRoundList r a n l) : b ∈ l ↔ RelatesWithinSteps r a b n

A round list contains exactly the members of the round.

theorem Relation.IsRoundList.length_eq {α : Type u_1} {r : α → α → Prop} {a : α} {n : ℕ} {l : List α} (hl : IsRoundList r a n l) : l.length = (reachableWithin r a n).ncard

The length of a round list is the size of the round: the count that the inductive counting algorithm carries from one round to the next.

theorem Relation.exists_isRoundList {α : Type u_1} {r : α → α → Prop} {a : α} {n : ℕ} (hfin : (reachableWithin r a n).Finite) : ∃ (l : List α), IsRoundList r a n l

Round lists are complete. A finite round can always be listed.

theorem Relation.forall_relatesWithinSteps_iff_exists_isRoundList {α : Type u_1} {r : α → α → Prop} {a : α} {n : ℕ} (hfin : (reachableWithin r a n).Finite) {p : α → Prop} : (∀ (b : α), RelatesWithinSteps r a b n → p b) ↔ ∃ (l : List α), IsRoundList r a n l ∧ ∀ b ∈ l, p b

Universal statements about a finite round are certified by a round list. A property holds throughout round n exactly when some round list consists of elements with the property.

theorem Relation.not_relatesWithinSteps_iff_exists_isRoundList {α : Type u_1} {r : α → α → Prop} {a b : α} {n : ℕ} (hfin : (reachableWithin r a n).Finite) : ¬RelatesWithinSteps r a b n ↔ ∃ (l : List α), IsRoundList r a n l ∧ b ∉ l

An element is outside a finite round exactly when some round list does not contain it.

theorem Relation.not_relatesWithinSteps_succ_iff {α : Type u_1} {r : α → α → Prop} {a c : α} {n : ℕ} (hfin : (reachableWithin r a n).Finite) : ¬RelatesWithinSteps r a c (n + 1) ↔ ∃ (l : List α), IsRoundList r a n l ∧ ∀ b ∈ l, ¬ReflGen r b c

The inductive counting step. An element c is outside round n + 1 exactly when some round list for round n contains neither c nor a predecessor of c. Checking such a list needs only the size of round n, which is how the size of round n + 1 is computed from it.

Unreachability as a certificate

theorem Relation.forall_reflTransGen_iff_exists_isRoundList_of_encard_le {α : Type u_1} {r : α → α → Prop} {a : α} {N : ℕ} (hN : {x : α | ReflTransGen r a x}.encard ≤ ↑N + 1) {p : α → Prop} : (∀ (b : α), ReflTransGen r a b → p b) ↔ ∃ (l : List α), IsRoundList r a N l ∧ ∀ b ∈ l, p b

A property of every reachable element is certified by a round list for round N, once at most N + 1 elements are reachable.

theorem Relation.not_reflTransGen_iff_exists_isRoundList_of_encard_le {α : Type u_1} {r : α → α → Prop} {a b : α} {N : ℕ} (hN : {x : α | ReflTransGen r a x}.encard ≤ ↑N + 1) : ¬ReflTransGen r a b ↔ ∃ (l : List α), IsRoundList r a N l ∧ b ∉ l

Unreachability is certified by a round list for round N, once at most N + 1 elements are reachable.

theorem Relation.forall_reflTransGen_iff_exists_isRoundList {α : Type u_1} {r : α → α → Prop} {a : α} {N : ℕ} [Finite α] (hN : Nat.card α ≤ N + 1) {p : α → Prop} : (∀ (b : α), ReflTransGen r a b → p b) ↔ ∃ (l : List α), IsRoundList r a N l ∧ ∀ b ∈ l, p b

A property of every reachable element is certified by a round list. On a finite type with at most N + 1 elements, every element reachable from a has property p exactly when some round list for round N consists of elements with property p. With p the property of not being accepting, this is what a nondeterministic machine certifies to accept the complement of a language decided by reachability Sipser, Theorem 8.27.

theorem Relation.not_reflTransGen_iff_exists_isRoundList {α : Type u_1} {r : α → α → Prop} {a b : α} {N : ℕ} [Finite α] (hN : Nat.card α ≤ N + 1) : ¬ReflTransGen r a b ↔ ∃ (l : List α), IsRoundList r a N l ∧ b ∉ l

Unreachability is certified by a round list. On a finite type with at most N + 1 elements, b is not reachable from a exactly when some round list for round N does not contain b.