Documentation

Complexity.Foundations.Relation.RelatesWithinSteps

Walks of bounded length and the midpoint recursion #

This file extends upstream Relation.RelatesInSteps and Relation.RelatesWithinSteps (a walk of exactly, or at most, n steps of a relation r) with the facts behind Savitch's theorem.

A walk of at most n steps of r is a walk of exactly n steps of the reflexive closure Relation.ReflGen r, which may stay put. In that form a walk of at most m + n steps is exactly a walk of at most m steps to a midpoint followed by a walk of at most n steps from it, so a bound of 2 ^ (i + 1) reduces to two independent bounds of 2 ^ i: the recursion that Savitch's algorithm runs, storing one midpoint per level. On a finite type with N elements, everything reachable is reachable within N - 1 steps, hence within 2 ^ ⌈log₂ N⌉ steps, which fixes the recursion depth at ⌈log₂ N⌉.

Nothing here mentions a machine: these are the facts about the configuration graph that Savitch's algorithm relies on.

Main results #

References #

Walks that may stay put #

source
theorem Relation.relatesInSteps_self {α : Type u_1} {r : α → α → Prop} [Std.Refl r] (a : α) (n : ℕ) :
RelatesInSteps r a a n

A reflexive relation relates every element to itself in any number of steps.

source
theorem Relation.RelatesWithinSteps.reflTransGen {α : Type u_1} {r : α → α → Prop} {a b : α} {n : ℕ} (h : RelatesWithinSteps r a b n) :
ReflTransGen r a b

A walk of at most n steps is a walk.

source
theorem Relation.relatesWithinSteps_iff_relatesInSteps_reflGen {α : Type u_1} {r : α → α → Prop} {a b : α} {n : ℕ} :
RelatesWithinSteps r a b n ↔ RelatesInSteps (ReflGen r) a b n

A walk of at most n steps is a walk of exactly n steps that may stay put. This is how a walk of bounded length is guessed and checked one step at a time.

source
theorem Relation.RelatesWithinSteps.succ_iff {α : Type u_1} {r : α → α → Prop} {a c : α} {n : ℕ} :
RelatesWithinSteps r a c (n + 1) ↔ ∃ (b : α), RelatesWithinSteps r a b n ∧ ReflGen r b c

One more step of breadth-first search. An element is reached within n + 1 steps exactly when it is reached in at most one step from an element reached within n steps.

source
@[simp]
theorem Relation.RelatesWithinSteps.one_iff {α : Type u_1} {r : α → α → Prop} {a b : α} :
RelatesWithinSteps r a b 1 ↔ ReflGen r a b

A walk of at most one step is a step of the reflexive closure.

Splitting walks #

source
theorem Function.iterate_trans {α : Type u_1} {f : α → α} {a b c : α} {m n : ℕ} (h₁ : f^[m] a = b) (h₂ : f^[n] b = c) :
f^[n + m] a = c

Iterated function applications compose across step counts.

source
theorem Relation.RelatesInSteps.add_iff {α : Type u_1} {r : α → α → Prop} {a c : α} {m n : ℕ} :
RelatesInSteps r a c (m + n) ↔ ∃ (b : α), RelatesInSteps r a b m ∧ RelatesInSteps r b c n

Walks split at any point. A walk of m + n steps passes through a midpoint after exactly m of them.

source
theorem Relation.RelatesWithinSteps.add_iff {α : Type u_1} {r : α → α → Prop} {a c : α} {m n : ℕ} :
RelatesWithinSteps r a c (m + n) ↔ ∃ (b : α), RelatesWithinSteps r a b m ∧ RelatesWithinSteps r b c n

The midpoint recursion. A walk of at most m + n steps is exactly a walk of at most m steps to some midpoint followed by a walk of at most n steps from it. The midpoint is all a recursive search has to remember.

source
theorem Relation.RelatesWithinSteps.two_mul_iff {α : Type u_1} {r : α → α → Prop} {a c : α} {n : ℕ} :
RelatesWithinSteps r a c (2 * n) ↔ ∃ (b : α), RelatesWithinSteps r a b n ∧ RelatesWithinSteps r b c n

The halving form of the midpoint recursion: a bound of 2 n splits into two independent bounds of n.

source
theorem Relation.RelatesWithinSteps.two_pow_succ_iff {α : Type u_1} {r : α → α → Prop} {a c : α} {i : ℕ} :
RelatesWithinSteps r a c (2 ^ (i + 1)) ↔ ∃ (b : α), RelatesWithinSteps r a b (2 ^ i) ∧ RelatesWithinSteps r b c (2 ^ i)

The recursion of Savitch's algorithm. A bound of 2 ^ (i + 1) splits into two subproblems with bound 2 ^ i, so the recursion from a bound of 2 ^ i has depth i and each level stores one midpoint; its base case is Relation.RelatesWithinSteps.one_iff Sipser, Theorem 8.5.

Walks on few elements are short #

source
theorem Relation.ReflTransGen.relatesWithinSteps_of_encard_le {α : Type u_1} {r : α → α → Prop} {a b : α} {N : ℕ} (h : ReflTransGen r a b) (hN : {x : α | ReflTransGen r a x}.encard ≤ ↑N + 1) :
RelatesWithinSteps r a b N

Everything reachable is reachable within one step fewer than the number of reachable elements. A longer walk repeats an element, and the loop between the repetitions can be cut out (upstream Relation.ReflTransGen.relatesInSteps_lt_encard).

source
theorem Relation.reflTransGen_iff_relatesWithinSteps_of_encard_le {α : Type u_1} {r : α → α → Prop} {a b : α} {N : ℕ} (hN : {x : α | ReflTransGen r a x}.encard ≤ ↑N + 1) :
ReflTransGen r a b ↔ RelatesWithinSteps r a b N

Reachability is reachability within N steps once at most N + 1 elements are reachable.

source
theorem Relation.reflTransGen_iff_relatesWithinSteps {α : Type u_1} {r : α → α → Prop} {a b : α} {N : ℕ} [Finite α] (hN : Nat.card α ≤ N + 1) :
ReflTransGen r a b ↔ RelatesWithinSteps r a b N

On a finite type, reachability is reachability within one step fewer than the number of elements.

source
theorem Relation.reflTransGen_iff_relatesWithinSteps_two_pow_clog {α : Type u_1} {r : α → α → Prop} {a b : α} [Finite α] :
ReflTransGen r a b ↔ RelatesWithinSteps r a b (2 ^ Nat.clog 2 (Nat.card α))

The bound Savitch's recursion starts from. On a finite type with N elements, reachability is reachability within 2 ^ ⌈log₂ N⌉ steps, so the recursion of Relation.RelatesWithinSteps.two_pow_succ_iff decides it at depth ⌈log₂ N⌉ Sipser, Theorem 8.5.