Logarithmic space

Space is upstream's measure: the number of distinct work-tape cells visited by the heads, summed over the work tapes. The input is on a read-only tape and is not charged; nor is the write-only, append-only output. A space bound applies to every computation prefix (Turing.MultiTapeNTM.RunsInSpace). The logarithmic bounds are c * (Nat.log2 n + 1) on encoded instances of length n, for a constant c Sipser, Section 8.4.

Cslib.Complexity.L enc consists of the problems decided by a Boolean function computable in logarithmic space (Turing.MultiTapeTM.ComputableInLogSpace): one deterministic machine with a binary alphabet and finitely many states halts on every encoded instance with output [true] or [false] within logarithmic space. Any number of work tapes is allowed; definitions with one work tape give the same class, since work tapes can be interleaved on one at a constant factor in space (not formalized here). No time bound is imposed beyond halting; a polynomial one follows (Cslib.Complexity.L_subset_P). Equivalently (Cslib.Complexity.mem_L_iff), the problem is decidable within some time and space c₁ * Nat.log2 n + c₂ in the sense of upstream Turing.MultiTapeTM.DecidableInTimeAndSpace. The local characterization Cslib.Complexity.mem_L_iff_mem_DSPACE gives exactly DSPACE enc Nat.log2, the shape of the class L = DSPACE(log₂) of cslib pull request #767 (open), whose classes are indexed by languages rather than encoded instances.

Cslib.Complexity.NL enc consists of the problems decided by one nondeterministic machine with a binary alphabet and finitely many states within logarithmic space (Turing.MultiTapeNTM.DecidesInSpace): every computation prefix on enc a stays within the bound, every branch halts, and a ∈ A exactly when some computation path halts with output [true] Sipser, Definition 8.1. No time bound is imposed beyond halting; a polynomial one follows (Cslib.Complexity.NL_subset_P).

Halting convention. Every branch must halt: on each encoded instance some number of steps bounds every computation path, though a path may end stuck before it, and then does not accept. Every upper bound proved here for NL also holds for logspace recognizers, whose branches may run forever (Turing.MultiTapeNTM.RecognizesInSpace): such a problem is in P (Cslib.Complexity.mem_P_of_recognizesInSpace). The complement construction also puts it in NL itself (Cslib.Complexity.mem_NL_of_recognizesInSpace in CslibFrontier.Computability.Complexity.Classes.LogSpace.Complement), without requiring source termination.

Cslib.Complexity.LogSpaceReducible encA encB A B asks for a logspace function mapping instances of A to instances of B, preserving membership Sipser, Section 8.5. By definition it is the many-one reducibility Cslib.Complexity.ManyOneReducibleBy by logspace functions (Cslib.Complexity.logSpaceReducible_iff_manyOneReducibleBy); its body is kept as the ∃ statement, so that the admissibility goal of an anonymous constructor is ComputableInLogSpace f enc encB itself. Logspace reductions compose, and L is closed under them, because logspace functions compose without storing intermediate values (Turing.MultiTapeTM.ComputableInLogSpace.comp). Hardness and completeness under them, Cslib.Complexity.LogSpaceHard and Cslib.Complexity.LogSpaceComplete, are the instances of Cslib.Complexity.HardUnder and Cslib.Complexity.CompleteUnder for LogSpaceReducible; the second conjunct of LogSpaceComplete is stated as LogSpaceHard.

Main definitions

• Cslib.Complexity.L: deterministic logarithmic space.
• Cslib.Complexity.NL: nondeterministic logarithmic space.
• Cslib.Complexity.LogSpaceReducible: logspace many-one reductions.
• Cslib.Complexity.LogSpaceHard, Cslib.Complexity.LogSpaceComplete: hardness and completeness under logspace many-one reductions.

Main results

• Cslib.Complexity.mem_L_iff: L in terms of upstream DecidableInTimeAndSpace.
• Cslib.Complexity.mem_L_iff_mem_DSPACE: the specialization DSPACE Nat.log2.
• Cslib.Complexity.L_subset_NL: a deterministic machine is a nondeterministic machine.
• Cslib.Complexity.compl_mem_L, Cslib.Complexity.L_eq_preimage_compl_L: L is closed under complement.
• Cslib.Complexity.L_subset_P: logarithmic space is within polynomial time.
• Cslib.Complexity.L_subset_PSPACE, Cslib.Complexity.NL_subset_NPSPACE: logarithmic space is within polynomial space.
• Cslib.Complexity.LogSpaceReducible.refl, Cslib.Complexity.LogSpaceReducible.trans: logspace reducibility is a preorder.
• Cslib.Complexity.LogSpaceReducible.mem_L: L is closed under logspace reductions.
• Cslib.Complexity.LogSpaceReducible.compl: reductions between complements.
• Cslib.Complexity.LogSpaceReducible.polyTimeReducible: logspace reductions are polynomial-time reductions.
• Cslib.Complexity.LogSpaceHard.trans: hardness transfers along logspace reductions.
• Cslib.Complexity.LogSpaceHard.subset_L: a hard problem in L places its source class in L.
• Cslib.Complexity.LogSpaceComplete.mem_L_iff: a problem complete for a class containing L is in L exactly when the class equals L, for every encoding.
• Cslib.Complexity.LogSpaceHard.polyTimeHard: logspace hardness implies polynomial-time hardness.
• Cslib.Complexity.LogSpaceComplete.polyTimeComplete: completeness under logspace reductions implies completeness under polynomial-time reductions.

References

• M. Sipser, Introduction to the Theory of Computation, Sections 8.4 and 8.5
• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 4.3

def Cslib.Complexity.L {α : Type} (enc : α ↪ List Bool) : Set (Set α)

The problems decided in logarithmic space with respect to the encoding enc: a Boolean function deciding membership is computable in logarithmic space Sipser, Section 8.4.

def Cslib.Complexity.NL {α : Type} (enc : α ↪ List Bool) : Set (Set α)

The problems decided by one nondeterministic machine within logarithmic space with respect to the encoding enc: every computation prefix on enc a visits at most c * (Nat.log2 n + 1) work-tape cells, where n is the length of enc a, every branch halts, and a ∈ A exactly when some computation path halts with output [true] Sipser, Definition 8.1.

theorem Cslib.Complexity.mem_L_iff {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ L enc ↔ ∃ (c₁ : ℕ) (c₂ : ℕ) (t : α → ℕ), Turing.MultiTapeTM.DecidableInTimeAndSpace A enc t fun (a : α) => c₁ * (enc a).length.log2 + c₂

Membership in L is upstream decidability within some time and space c₁ * Nat.log2 n + c₂, the shape of DSPACE(log₂) in cslib pull request #767.

theorem Cslib.Complexity.mem_L_iff_mem_DSPACE {α : Type} {enc : α ↪ List Bool} {A : Set α} : A ∈ L enc ↔ A ∈ DSPACE enc Nat.log2

L is DSPACE (log₂), the definition of L in cslib pull request #767.

theorem Cslib.Complexity.L_subset_NL {α : Type} {enc : α ↪ List Bool} : L enc ⊆ NL enc

Deterministic logarithmic space is within nondeterministic logarithmic space: a deterministic machine is a nondeterministic one with one computation path (Turing.MultiTapeTM.ComputableInTimeAndSpace.exists_decidesInSpace).

theorem Cslib.Complexity.compl_mem_L {α : Type} {enc : α ↪ List Bool} {A : Set α} (h : A ∈ L enc) : Aᶜ ∈ L enc

L is closed under complement: negate the decider, a composition of logspace functions.

theorem Cslib.Complexity.L_eq_preimage_compl_L {α : Type} (enc : α ↪ List Bool) : L enc = compl ⁻¹' L enc

L equals its preimage under complement.

theorem Cslib.Complexity.L_subset_P {α : Type} {enc : α ↪ List Bool} : L enc ⊆ P enc

Logarithmic space is within polynomial time: a deterministic machine that halts within logarithmic space repeats no configuration it can read, of which there are polynomially many.

theorem Cslib.Complexity.L_subset_PSPACE {α : Type} {enc : α ↪ List Bool} : L enc ⊆ PSPACE enc

Deterministic logarithmic space is within polynomial space.

theorem Cslib.Complexity.NL_subset_NPSPACE {α : Type} {enc : α ↪ List Bool} : NL enc ⊆ NPSPACE enc

Nondeterministic logarithmic space is within nondeterministic polynomial space.

Logspace reductions

def Cslib.Complexity.LogSpaceReducible {α β : Type} (enc : α ↪ List Bool) (encB : β ↪ List Bool) (A : Set α) (B : Set β) : Prop

A reduces to B in logarithmic space: some f, computable in logarithmic space with respect to enc and encB, satisfies a ∈ A ↔ f a ∈ B. This is ManyOneReducibleBy for the maps computable in logarithmic space (logSpaceReducible_iff_manyOneReducibleBy).

theorem Cslib.Complexity.logSpaceReducible_iff_manyOneReducibleBy {α β : Type} {enc : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} : LogSpaceReducible enc encB A B ↔ ManyOneReducibleBy (fun (x : α → β) => Turing.MultiTapeTM.ComputableInLogSpace x enc encB) A B

Logspace reducibility is many-one reducibility by the maps computable in logarithmic space.

theorem Cslib.Complexity.LogSpaceReducible.refl {α : Type} (enc : α ↪ List Bool) (A : Set α) : LogSpaceReducible enc enc A A

Every problem reduces to itself in logarithmic space.

theorem Cslib.Complexity.LogSpaceReducible.trans {α β γ : Type} {enc : α ↪ List Bool} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {A : Set α} {B : Set β} {C : Set γ} (hAB : LogSpaceReducible enc encB A B) (hBC : LogSpaceReducible encB encC B C) : LogSpaceReducible enc encC A C

Logspace reductions compose.

theorem Cslib.Complexity.LogSpaceReducible.mem_L {α β : Type} {enc : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} (hAB : LogSpaceReducible enc encB A B) (hB : B ∈ L encB) : A ∈ L enc

L is closed under logspace reductions.

theorem Cslib.Complexity.LogSpaceReducible.compl {α β : Type} {enc : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} (h : LogSpaceReducible enc encB A B) : LogSpaceReducible enc encB Aᶜ Bᶜ

A logspace reduction between problems is one between their complements.

theorem Cslib.Complexity.LogSpaceReducible.polyTimeReducible {α β : Type} {enc : α ↪ List Bool} {encB : β ↪ List Bool} {A : Set α} {B : Set β} (h : LogSpaceReducible enc encB A B) : PolyTimeReducible enc encB A B

Logspace reductions are polynomial-time reductions.

def Cslib.Complexity.LogSpaceHard {β : Type} (C : {α : Type} → (α ↪ List Bool) → Set (Set α)) (encB : β ↪ List Bool) (B : Set β) : Prop

B is hard for the class C under logspace many-one reductions: every problem in C, with any encoding of its instances, reduces to B in logarithmic space. This is HardUnder for LogSpaceReducible.

def Cslib.Complexity.LogSpaceComplete {β : Type} (C : {α : Type} → (α ↪ List Bool) → Set (Set α)) (encB : β ↪ List Bool) (B : Set β) : Prop

B is complete for the class C under logspace many-one reductions: it is in C and every problem in C reduces to it in logarithmic space. This is CompleteUnder for LogSpaceReducible (logSpaceComplete_iff_completeUnder), with its second conjunct stated as LogSpaceHard.

theorem Cslib.Complexity.logSpaceHard_iff_hardUnder {β : Type} {encB : β ↪ List Bool} {B : Set β} {C : {α : Type} → (α ↪ List Bool) → Set (Set α)} : LogSpaceHard (fun {α : Type} => C) encB B ↔ HardUnder (fun {α : Type} (enc : α ↪ List Bool) => LogSpaceReducible enc encB) C B

Logspace hardness is hardness under LogSpaceReducible.

theorem Cslib.Complexity.logSpaceComplete_iff_completeUnder {β : Type} {encB : β ↪ List Bool} {B : Set β} {C : {α : Type} → (α ↪ List Bool) → Set (Set α)} : LogSpaceComplete (fun {α : Type} => C) encB B ↔ CompleteUnder (fun {α : Type} (enc : α ↪ List Bool) => LogSpaceReducible enc encB) C encB B

Logspace completeness is completeness under LogSpaceReducible.

theorem Cslib.Complexity.LogSpaceHard.trans {β γ : Type} {encB : β ↪ List Bool} {encC : γ ↪ List Bool} {B : Set β} {C : Set γ} {D : {α : Type} → (α ↪ List Bool) → Set (Set α)} (hB : LogSpaceHard (fun {α : Type} => D) encB B) (hBC : LogSpaceReducible encB encC B C) : LogSpaceHard (fun {α : Type} => D) encC C

Logspace hardness transfers along a logspace reduction.

theorem Cslib.Complexity.LogSpaceHard.subset_L {α β : Type} {encB : β ↪ List Bool} {B : Set β} {D : {α : Type} → (α ↪ List Bool) → Set (Set α)} (hB : LogSpaceHard (fun {α : Type} => D) encB B) (hL : B ∈ L encB) (enc : α ↪ List Bool) : D enc ⊆ L enc

A class with a logspace-hard problem in L is contained in L, for every encoding.

theorem Cslib.Complexity.LogSpaceComplete.mem_L_iff {β : Type} {encB : β ↪ List Bool} {B : Set β} {D : {α : Type} → (α ↪ List Bool) → Set (Set α)} (hB : LogSpaceComplete (fun {α : Type} => D) encB B) (hLD : ∀ {α : Type} (enc : α ↪ List Bool), L enc ⊆ D enc) : B ∈ L encB ↔ ∀ {α : Type} (enc : α ↪ List Bool), D enc = L enc

A problem complete for a class containing L is in L exactly when the class equals L, for every encoding of instances. For P and NL this is the L-analogue of Cslib.Complexity.NPComplete.mem_P_iff.

theorem Cslib.Complexity.LogSpaceHard.polyTimeHard {β : Type} {encB : β ↪ List Bool} {B : Set β} {D : {α : Type} → (α ↪ List Bool) → Set (Set α)} (h : LogSpaceHard (fun {α : Type} => D) encB B) : PolyTimeHard (fun {α : Type} => D) encB B

Hardness under logspace reductions implies hardness under polynomial-time reductions.

theorem Cslib.Complexity.LogSpaceComplete.polyTimeComplete {β : Type} {encB : β ↪ List Bool} {B : Set β} {D : {α : Type} → (α ↪ List Bool) → Set (Set α)} (h : LogSpaceComplete (fun {α : Type} => D) encB B) : PolyTimeComplete (fun {α : Type} => D) encB B

Completeness under logspace reductions implies completeness under polynomial-time reductions.