Step-counted reachability and the halving recursion

⚠️ Unreviewed by Bolton

Savitch's theorem rests on one combinatorial identity: a walk of at most m + n steps is a walk of at most m steps followed by a walk of at most n steps, and conversely. Taking m = n turns a bound of 2t into two independent subproblems with bound t, so a bound of 2 ^ i recurses to depth i — the recursion whose stack a space-bounded machine can afford because each level stores only one midpoint.

Nothing here is about space, and nothing is about a machine: this is the pure statement that the midpoint search is correct, which is the part of Savitch's argument that has to be true before any bookkeeping is attempted.

The same step counting supplies the numbers that the Immerman–Szelepcsényi counting argument compares, so NLSubsetCoNL draws on this file too.

Main results

• NTM.ReachesCfgIn.trans, NTM.ReachesCfgIn.split — walks concatenate and split
• NTM.reachesCfgLe_add_iff — the midpoint recursion
• NTM.reachesCfgLe_two_mul_iff, NTM.reachesCfgLe_two_pow_succ_iff — its halving forms
• NTM.mem_reachSet_iff_reachesCfgLe — the rounds of the search are exactly the step bounds
• NTM.reachesCfg_iff_reachesCfgLe — every reachable configuration is reachable within the number of configuration codes

Walks concatenate and split

theorem Complexity.NTM.ReachesCfgIn.trans {k : ℕ} {tm : NTM k} {s t : ℕ} {c c' c'' : Cfg k tm.Q} (h : tm.ReachesCfgIn s c c') (h' : tm.ReachesCfgIn t c' c'') : tm.ReachesCfgIn (s + t) c c''

Walks concatenate, and their lengths add.

theorem Complexity.NTM.ReachesCfgIn.split {k : ℕ} {tm : NTM k} {s t : ℕ} {c c'' : Cfg k tm.Q} (h : tm.ReachesCfgIn (s + t) c c'') : ∃ (m : Cfg k tm.Q), tm.ReachesCfgIn s c m ∧ tm.ReachesCfgIn t m c''

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

theorem Complexity.NTM.ReachesCfgLe.mono {k : ℕ} {tm : NTM k} {s t : ℕ} {c c' : Cfg k tm.Q} (h : tm.ReachesCfgLe s c c') (hst : s ≤ t) : tm.ReachesCfgLe t c c'

A step bound can always be relaxed.

theorem Complexity.NTM.reachesCfgLe_refl {k : ℕ} (tm : NTM k) (t : ℕ) (c : Cfg k tm.Q) : tm.ReachesCfgLe t c c

A configuration reaches itself in no steps.

The midpoint recursion

theorem Complexity.NTM.reachesCfgLe_add_iff {k : ℕ} (tm : NTM k) (m n : ℕ) (c c'' : Cfg k tm.Q) : tm.ReachesCfgLe (m + n) c c'' ↔ ∃ (mid : Cfg k tm.Q), tm.ReachesCfgLe m c mid ∧ tm.ReachesCfgLe n mid c''

Savitch's 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 the only thing a recursive procedure has to remember.

theorem Complexity.NTM.reachesCfgLe_two_mul_iff {k : ℕ} (tm : NTM k) (t : ℕ) (c c'' : Cfg k tm.Q) : tm.ReachesCfgLe (2 * t) c c'' ↔ ∃ (mid : Cfg k tm.Q), tm.ReachesCfgLe t c mid ∧ tm.ReachesCfgLe t mid c''

The halving form: a bound of 2 t splits into two independent bounds of t.

theorem Complexity.NTM.reachesCfgLe_two_pow_succ_iff {k : ℕ} (tm : NTM k) (i : ℕ) (c c'' : Cfg k tm.Q) : tm.ReachesCfgLe (2 ^ (i + 1)) c c'' ↔ ∃ (mid : Cfg k tm.Q), tm.ReachesCfgLe (2 ^ i) c mid ∧ tm.ReachesCfgLe (2 ^ i) mid c''

The recursion Savitch's machine runs. A bound of 2 ^ (i + 1) recurses to two subproblems with bound 2 ^ i, so the depth is i and each level stores one midpoint.

Agreement with the breadth-first rounds

theorem Complexity.NTM.mem_reachSet_iff_reachesCfgLe {k : ℕ} (tm : NTM k) (c₀ : Cfg k tm.Q) (t : ℕ) (c : Cfg k tm.Q) : c ∈ tm.reachSet c₀ t ↔ tm.ReachesCfgLe t c₀ c

The rounds of the breadth-first search are exactly the step bounds.

theorem Complexity.NTM.reachesCfg_iff_reachesCfgLe {k : ℕ} {α : Type} [Fintype α] (tm : NTM k) (c₀ : Cfg k tm.Q) (g : Cfg k tm.Q → α) (hinj : ∀ {c c' : Cfg k tm.Q}, tm.ReachesCfg c₀ c → tm.ReachesCfg c₀ c' → g c = g c' → c = c') {N : ℕ} (hN : Fintype.card α ≤ N) (c : Cfg k tm.Q) : tm.ReachesCfg c₀ c ↔ tm.ReachesCfgLe N c₀ c

Every reachable configuration is reachable within the number of codes. A walk longer than that repeats a configuration, and the repetition can be cut out.