Logarithmic space on deterministic machines

Space is upstream's measure (Turing.MultiTapeNTM.RunPath.space): the number of distinct work-tape cells visited by the heads, summed over the work tapes. The read-only input tape and the write-only, append-only output tape are not charged, so a machine may read an input, and emit an output, much longer than its workspace Sipser, Section 8.4.

Turing.MultiTapeTM.ComputableInLogSpace f encIn encOut asks for one machine with a binary alphabet and finitely many states that computes f within space c * (Nat.log2 n + 1) on encoded inputs of length n, for a constant c, and halts. These are the functions computable in logarithmic space Arora and Barak, Section 4.3; the summand 1 keeps the bound positive on inputs of length at most one, where each work tape still costs a cell.

No time bound is imposed, because one follows. A machine never repeats the part of its configuration it can still read, the input head position and the storage (Turing.Cfg.core), before it halts: the next core depends only on the current one. So a machine that halts within space s halts within (n + 2) * storageBound Bool State k s steps (Turing.MultiTapeTM.haltsAt_le_card), by upstream's count of storages. Under a logarithmic space bound this is polynomial in n, so logspace functions are computable in polynomial time and have polynomially long values (Turing.MultiTapeTM.ComputableInLogSpace.exists_polyBounded_time, Turing.MultiTapeTM.ComputableInLogSpace.polyBounded_length). This is the time bound of the inclusion DSPACE(s) ⊆ DTIME(2 ^ O(s)) of cslib pull request #767 (ComputesInTimeAndSpace.truncate there), stated for the current machine API.

Composition is in CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.Composition.Recompute. It is kept apart because its machine is built from the universal machine; this file does not depend on that machine.

Main definitions

• Turing.MultiTapeTM.ComputableInLogSpace: computability in logarithmic space.

Main results

• Turing.MultiTapeTM.haltsAt_le_card: a halting machine within space s halts within (n + 2) * storageBound Symbol State k s steps.
• Turing.MultiTapeTM.ComputableInLogSpace.exists_polyBounded_time: logspace computations take polynomial time.
• Turing.MultiTapeTM.ComputableInLogSpace.polyBounded_length: logspace functions have polynomially long values.
• Turing.MultiTapeTM.ComputableInLogSpace.id, Turing.MultiTapeTM.ComputableInLogSpace.const, Turing.MultiTapeTM.ComputableInLogSpace.of_finite, Turing.MultiTapeTM.ComputableInLogSpace.congr, Turing.MultiTapeTM.ComputableInLogSpace.of_eq: the identity, constants and functions on finite types are computable in logarithmic space, and congruence.
• Turing.MultiTapeTM.ComputableInLogSpace.computableInPolyTime, Turing.MultiTapeTM.ComputableInLogSpace.computableTidilyInPolyTime: logspace functions are computable in polynomial time.
• ComputableInLogSpace is registered with fun_prop, with the inclusion in polynomial time as a one-way transition.
• Turing.MultiTapeTM.Transducer.computableInLogSpace: functions computed by finite-state transducers are computable in logarithmic space.
• Turing.MultiTapeTM.polyBounded_log: logarithmic bounds are polynomially bounded.
• Turing.MultiTapeTM.computableInLogSpace_frame: framing an encoded input is computable in logarithmic space.

References

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

Halting within the number of cores

theorem Turing.MultiTapeTM.core_runFrom_eq_of_core_eq {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {c₁ c₂ : Cfg k Symbol State input} (h : c₁.core = c₂.core) (m : ℕ) : (runFrom c₁ m).core = (runFrom c₂ m).core

Runs from configurations with equal cores keep equal cores, since a step does not read the output.

theorem Turing.MultiTapeTM.haltsAt_le_card {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} [Fintype Symbol] [Fintype State] {s u : ℕ} (hs : tm.RunsInSpace input s) (hu : tm.HaltsAt (tm.initCfg input) u) : u ≤ (input.length + 2) * storageBound Symbol State k s

A halting machine halts within the number of its cores. Before it halts, a machine within space s repeats no core (input head position and storage), since from a repeated core it would never halt; so it halts within (n + 2) * storageBound Symbol State k s steps on an input of length n.

theorem Turing.MultiTapeTM.ComputesInTimeAndSpace.of_card {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} [Fintype Symbol] [Fintype State] {output : List Symbol} {t s : ℕ} (h : tm.ComputesInTimeAndSpace input output t s) : tm.ComputesInTimeAndSpace input output ((input.length + 2) * storageBound Symbol State k s) s

A machine that halts on input within space s does so within (n + 2) * storageBound Symbol State k s steps, with the same output.

Computability in logarithmic space

def Turing.MultiTapeTM.ComputableInLogSpace {α β : Type} (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) : Prop

f is computable in logarithmic space: some machine with a binary alphabet and finitely many states computes f with respect to encIn and encOut, halting, within space c * (Nat.log2 n + 1) on encoded inputs of length n, for a constant c. The input and the output are not charged.

theorem Turing.MultiTapeTM.polyBounded_log {δ : Type u_1} (size : δ → ℕ) (c : ℕ) : PolyBounded size fun (a : δ) => c * ((size a).log2 + 1)

The logarithmic bounds c * (log₂ n + 1) are polynomially bounded (Cslib.polynomiallyBounded_mul_log2_add_one).

theorem Turing.MultiTapeTM.ComputableInLogSpace.exists_polyBounded_time {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ComputableInLogSpace f encIn encMid) : ∃ (t : α → ℕ) (c : ℕ), PolyBounded (fun (a : α) => (encIn a).length) t ∧ ComputableInTimeAndSpace f encIn encMid t fun (a : α) => c * ((encIn a).length.log2 + 1)

Logspace computations take polynomial time.

theorem Turing.MultiTapeTM.ComputableInLogSpace.polyBounded_length {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ComputableInLogSpace f encIn encMid) : PolyBounded (fun (a : α) => (encIn a).length) fun (a : α) => (encMid (f a)).length

Logspace functions have polynomially long values, since a machine emits at most one symbol per step.

theorem Turing.MultiTapeTM.ComputableInLogSpace.computableTidilyInPolyTime {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ComputableInLogSpace f encIn encMid) : ComputableTidilyInPolyTime f encIn encMid

Logspace functions are computable in polynomial time, tidily.

theorem Turing.MultiTapeTM.ComputableInLogSpace.computableInPolyTime {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ComputableInLogSpace f encIn encMid) : ComputableInPolyTime f encIn encMid

Logspace functions are computable in polynomial time.

theorem Turing.MultiTapeTM.ComputableInLogSpace.id {α : Type} {encIn : α ↪ List Bool} : ComputableInLogSpace (fun (a : α) => a) encIn encIn

The identity is computable in logarithmic space. The zero-space bound itself is Turing.MultiTapeTM.computableInTimeAndSpace_id.

theorem Turing.MultiTapeTM.ComputableInLogSpace.congr {α β γ : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {f : α → β} {g : α → γ} (hf : ComputableInLogSpace f encIn encMid) (h : ∀ (a : α), encOut (g a) = encMid (f a)) : ComputableInLogSpace g encIn encOut

A function whose encoded values agree with those of a logspace function is computable in logarithmic space, by the same machine.

theorem Turing.MultiTapeTM.ComputableInLogSpace.congr_fun {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f g : α → β} (hf : ComputableInLogSpace f encIn encMid) (h : ∀ (a : α), g a = f a) : ComputableInLogSpace g encIn encMid

A function pointwisely equal to a logspace function is computable in logarithmic space, by the same machine.

theorem Turing.MultiTapeTM.ComputableInLogSpace.of_eq {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encMid (f a) = encIn a) : ComputableInLogSpace f encIn encMid

A function whose encoded values equal its encoded arguments is computable in logarithmic space, by the machine of the identity.

theorem Turing.MultiTapeTM.ComputableInLogSpace.const {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} (b : β) : ComputableInLogSpace (fun (x : α) => b) encIn encMid

Constant functions are computable in logarithmic space. The zero-space bound itself is Turing.MultiTapeTM.computableInTimeAndSpace_of_const.

theorem Turing.MultiTapeTM.ComputableInLogSpace.of_finite {α β : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} [Finite α] (f : α → β) : ComputableInLogSpace f encIn encMid

Functions on a finite type are computable in logarithmic space. The zero-space bound itself is Turing.MultiTapeTM.computableInTimeAndSpace_of_finite.

Automation

ComputableInLogSpace is a fun_prop predicate. The identity and constants are its core rules here. Its composition rule is registered in CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.Composition.Recompute, so fun_prop needs that module to decompose a goal; pairing, projections, case distinctions and word operations are registered in CslibFrontier/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/Words.lean, and the counter-program primitives in CslibFrontier.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.CounterProgram.Words. The inclusion in polynomial time is a one-way transition rule: a logspace certificate closes a plain polynomial-time goal, and there is no rule back, so the search has no cycle.

theorem Turing.MultiTapeTM.Transducer.computableInLogSpace {Q : Type} [Finite Q] (τ : Transducer Bool Q) {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (hf : ∀ (a : α), encOut (f a) = τ.run τ.q₀ (encIn a)) : ComputableInLogSpace f encIn encOut

A function computed by a finite-state transducer is computable in logarithmic space: the transducer runs without work tapes.

theorem Turing.MultiTapeTM.computableInLogSpace_frame {α : Type} (enc : α ↪ List Bool) : ComputableInLogSpace (fun (a : α) => enc a) enc (encFramed encBits)

Framing an encoded instance is computable in logarithmic space, by a finite-state transducer (Turing.MultiTapeTM.Transducer.computableInLogSpace).