def LogSpace.log : ℕ → ℕ

Base-2 logarithm on ℕ, used as the canonical space bound for the class L = SPACE(log n).

structure LogSpace.LogSpaceConfig (Q Γ : Type) : Type

A log-space Turing machine configuration (q, p_1, p_2, t) consisting of the current state, the input-tape head position p_1, the work-tape head position p_2, and the contents t of the work tape.

• state : Q
• inputHeadPos : ℕ
• workHeadPos : ℕ
• workTape : ℕ → Γ

def LogSpace.BoundedLogSpaceConfig (Q Γ : Type) (n s : ℕ) : Type

The type of log-space configurations restricted so that the input head lies in Fin n, the work head lies in Fin s, and the work tape is encoded as a function Fin s → Γ. This is a finite type whenever Q and Γ are.

@[implicit_reducible]

noncomputable instance LogSpace.BoundedLogSpaceConfig.fintype (Q Γ : Type) [Fintype Q] [Fintype Γ] (n s : ℕ) : Fintype (BoundedLogSpaceConfig Q Γ n s)

BoundedLogSpaceConfig Q Γ n s is a finite type, inherited from the product structure of its components.

def LogSpace.LogSpaceConfig.ofConfig {Q Γ : Type} (c : TuringMachine.Config Q Γ) : LogSpaceConfig Q Γ

Convert an ordinary Turing-machine configuration into the log-space configuration view by taking the input head position to be |c.headPos|, initializing the work head to 0, and copying the tape as the work tape.

def LogSpace.InL {Γ : Type} (A : Set (List Γ)) : Prop

The complexity class L = SPACE(log n): A ∈ L iff A is decided by some deterministic TM in space O(log n).

def LogSpace.InNL {Γ : Type} (A : Set (List Γ)) : Prop

The complexity class NL = NSPACE(log n): A ∈ NL iff A is decided by some nondeterministic TM in space O(log n).

def LogSpace.InCoNSPACE {Γ : Type} (f : ℕ → ℕ) (A : Set (List Γ)) : Prop

coNSPACE(f): A ∈ coNSPACE(f) iff the complement of A lies in NSPACE(f).

def LogSpace.InCoNL {Γ : Type} (A : Set (List Γ)) : Prop

The class coNL = coNSPACE(log n): A ∈ coNL iff Aᶜ ∈ NL.

def LogSpace.IsAtLeastLog (f : ℕ → ℕ) : Prop

IsAtLeastLog f asserts that f grows at least as fast as log₂, i.e. log₂ n ≤ f n for every n. This is the standard hypothesis under which Immerman–Szelepcsényi gives NSPACE(f) = coNSPACE(f).

theorem LogSpace.immerman_szelepcsenyi {Γ : Type} (f : ℕ → ℕ) (hf : IsAtLeastLog f) (A : Set (List Γ)) (hA : SpaceComplexity.InNSPACE f A) : SpaceComplexity.InNSPACE f Aᶜ

Immerman–Szelepcsényi Theorem. For any space bound f with f(n) ≥ log₂ n, the class NSPACE(f) is closed under complementation: if A ∈ NSPACE(f) then Aᶜ ∈ NSPACE(f).

theorem LogSpace.nspace_eq_conspace {Γ : Type} (f : ℕ → ℕ) (hf : IsAtLeastLog f) (A : Set (List Γ)) : SpaceComplexity.InNSPACE f A ↔ InCoNSPACE f A

NSPACE(f) = coNSPACE(f) for any f ≥ log₂, an immediate consequence of Immerman–Szelepcsényi applied to both A and Aᶜ.

theorem LogSpace.nl_eq_conl {Γ : Type} (A : Set (List Γ)) : InNL A ↔ InCoNL A

NL = coNL (Immerman–Szelepcsényi specialized to f = log₂).

inductive LogSpace.BoundedReachable {V : Type u_1} (G : V → V → Prop) : ℕ → V → V → Prop

BoundedReachable G d s t holds when t is reachable from s in the graph G using at most d edge steps. The weaken constructor pads a d-step path into a (d+1)-step path, ensuring monotonicity in d.

• refl {V : Type u_1} {G : V → V → Prop} (s : V) : BoundedReachable G 0 s s
• step {V : Type u_1} {G : V → V → Prop} {d : ℕ} {s u t : V} : BoundedReachable G d s u → G u t → BoundedReachable G (d + 1) s t
• weaken {V : Type u_1} {G : V → V → Prop} {d : ℕ} {s t : V} : BoundedReachable G d s t → BoundedReachable G (d + 1) s t

def LogSpace.reachableSet {V : Type u_1} (G : V → V → Prop) (d : ℕ) (s : V) : Set V

The set of vertices reachable from s in G within at most d steps.

noncomputable def LogSpace.reachableCount {V : Type u_1} (G : V → V → Prop) (d : ℕ) (s : V) : ℕ

The count c_d = |reachableSet G d s| of vertices reachable from s within d steps. In the Immerman–Szelepcsényi proof this is the quantity computed inductively by an NL machine.

theorem LogSpace.nl_config_compute {NLComputes_cd NLDecides_pathd : ℕ → Prop} (thm_cd_to_pathd_succ : ∀ (d : ℕ), NLComputes_cd d → NLDecides_pathd (d + 1)) (counting_to_cd : ∀ (d : ℕ), NLDecides_pathd d → NLComputes_cd d) (d : ℕ) (h : NLComputes_cd d) : NLComputes_cd (d + 1)

Inductive step in the Immerman–Szelepcsényi argument: given an NL procedure for computing c_d, one can build an NL procedure for deciding the distance-(d+1) path predicate, from which an NL procedure for c_{d+1} is obtained. This packages those two abstract steps into the successor case.

theorem LogSpace.step_eq_of_isHaltConfig {Q Γ : Type} [DecidableEq Q] (M : TuringMachine.TM Q Γ) (c : TuringMachine.Config Q Γ) (h : M.isHaltConfig c) : M.step c = c

If c is a halting configuration of M, then M.step c = c: halting configurations are fixed points of the transition function.

theorem LogSpace.run_eq_of_isHaltConfig {Q Γ : Type} [DecidableEq Q] (M : TuringMachine.TM Q Γ) (c : TuringMachine.Config Q Γ) {n m : ℕ} (hn : n ≤ m) (h : M.isHaltConfig (M.run c n)) : M.run c m = M.run c n

Once M has halted by step n, running it further does nothing: M.run c m = M.run c n for every m ≥ n.

theorem LogSpace.isHaltConfig_mono {Q Γ : Type} [DecidableEq Q] (M : TuringMachine.TM Q Γ) (c : TuringMachine.Config Q Γ) {n m : ℕ} (hn : n ≤ m) (h : M.isHaltConfig (M.run c n)) : M.isHaltConfig (M.run c m)

Monotonicity of halting: if M is in a halting configuration after n steps and n ≤ m, then it is also in a halting configuration after m steps.

theorem LogSpace.space_bounded_decider_poly_time {Q Γ : Type} [DecidableEq Q] [Fintype Q] [Fintype Γ] (M : TuringMachine.TM Q Γ) (g : ℕ → ℕ) (hSpace : SpaceComplexity.TMRunsInSpace M g) : ∃ (t : ℕ → ℕ) (K : ℕ), M.runsInTime t ∧ 0 < K ∧ ∀ (n : ℕ), t n ≤ K * 2 ^ (K * g n)

A deterministic TM running in space g(n) must halt within O(2^{O(g(n))}) steps, since otherwise some configuration would repeat and the machine would loop. Concretely there exist a time bound t and a constant K > 0 with M.runsInTime t and t n ≤ K · 2^(K · g n).

theorem LogSpace.dtm_simulates_ntm {Q Γ : Type} [DecidableEq Q] (M : SpaceComplexity.NTM Q Γ) (g : ℕ → ℕ) (hM_space : M.RunsInSpace g) : ∃ (Q' : Type) (x : Fintype Q') (x : DecidableEq Q') (T : TuringMachine.TM Q' Γ), T.language = M.language ∧ T.isDecider ∧ ∃ (K : ℕ), 0 < K ∧ T.runsInTime fun (n : ℕ) => K * 2 ^ (K * g n)

Simulation of a space-g NTM by a deterministic TM with time O(2^{O(g)}): searching the configuration graph of an NTM whose space usage is g can be done deterministically in time exponential in g.

theorem LogSpace.nspace_bounded_decider_poly_time {Q Γ : Type} [DecidableEq Q] (M : SpaceComplexity.NTM Q Γ) (g : ℕ → ℕ) (hSpace : M.RunsInSpace g) : ∃ (Q' : Type) (x : Fintype Q') (x : DecidableEq Q') (T : TuringMachine.TM Q' Γ) (t : ℕ → ℕ) (K : ℕ), T.decides M.language ∧ T.runsInTime t ∧ 0 < K ∧ ∀ (n : ℕ), t n ≤ K * 2 ^ (K * g n)

Packaging of dtm_simulates_ntm: every space-g NTM is decided by a deterministic TM in time K · 2^(K · g n) for some constant K > 0. This is the key tool behind NL ⊆ P (and more generally NSPACE(g) ⊆ DTIME(2^{O(g)})).

theorem LogSpace.l_subset_p {Γ : Type} [Fintype Γ] (A : Set (List Γ)) (h : InL A) : TuringMachine.InP A

L ⊆ P. Every language decidable in deterministic log-space is also decidable in deterministic polynomial time. The proof combines space_bounded_decider_poly_time (giving a time bound of K · 2^(K · g n)) with the bound g n ≤ c · log₂ n from the log-space hypothesis, yielding a polynomial time bound K · n^(K · c + 1).