Machines with random access to their input, in logarithmic space

A query machine (Turing.QueryMachine) reads its input by position: from a state s it asks for the input bit at position query s, receives it (none past the end of the input), moves to next (s, b) and emits emit (s, b), until halted s; it then emits finish s. The state is abstract, so query machines are a convenient way to describe logarithmic-space algorithms that jump around in their input: counters, tuples of elements, indices into tables.

Such a machine runs within logarithmic space when its states have logarithmic encodings and its parts are computable within space linear in the encoded state (Turing.QueryMachine.computableInLogSpace), and more generally within the space of its states, once that is at least logarithmic (Turing.QueryMachine.computableInSpace). The proof is a multi-pass fold over the input (Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.multiPassFold): each pass simulates one step, scanning the whole input with a binary position counter to fetch the queried bit, so that only the state, the counter and the fetched bit are ever stored Sipser, Section 8.4.

Implementation notes

Christian Reitwiessner's read machines (Turing.ReadMachine) are the same kind of model, simulated by step machines that move a head one cell at a time. A query machine differs in two ways that the algorithms built on it need: a read past the end of the input returns none rather than false, so that a machine can find the end of its input (as a check of the shape of an encoded input must), and a final word is emitted at the halt. Its logarithmic-space bound is proved directly from the multi-pass fold.

Main definitions

• Turing.QueryMachine: a machine with random access to its input.
• Turing.QueryMachine.encStateRead: the encoding of a state with the bit it reads.
• Turing.QueryMachine.run, Turing.QueryMachine.output: its run and its output.

Main results

• Turing.QueryMachine.computableInSpace: a query machine whose states along its runs have length O(S), for a bound S at least logarithmic in the input, and whose parts are computable in linear space, computes a function in space O(S).
• Turing.QueryMachine.computableInLogSpace: a query machine with logarithmic states and parts computable in linear space computes a function in logarithmic space.
• Turing.QueryMachine.output_add_of_halted: increasing the clock after halting preserves output.

References

• M. Sipser, Introduction to the Theory of Computation, Section 8.4

structure Turing.QueryMachine (σ : Type u_1) : Type u_1

A query machine: from the state s it reads the input bit at position query s (none past the end of the input), moves to next (s, b) and emits emit (s, b), until halted s; at the end it emits finish s.

• init : σ

  The initial state.

• query : σ → ℕ

  The position of the input bit read in a state.

• next : σ × Option Bool → σ

  The next state, given the bit read.

• emit : σ × Option Bool → List Bool

  The word emitted by a step, given the bit read.

• halted : σ → Bool

  Whether the machine has halted.

• finish : σ → List Bool

  The word emitted at the end.

@[reducible, inline]

abbrev Turing.QueryMachine.encStateRead {τ : Type} (encS : τ ↪ List Bool) : τ × Option Bool ↪ List Bool

The encoding of the arguments of next and emit: a state paired with the bit read, which is none past the end of the input. The state is framed and the optional bit takes at most two bits, so the encoded length is 2 * (encS s).length + 1 plus at most 2.

def Turing.QueryMachine.read {σ : Type u_1} (M : QueryMachine σ) (w : List Bool) (s : σ) : Option Bool

The input bit read in a state, none past the end of the input.

def Turing.QueryMachine.step {σ : Type u_1} (M : QueryMachine σ) (w : List Bool) (s : σ) : σ

A step on the input w; halted states are fixed.

def Turing.QueryMachine.run {σ : Type u_1} (M : QueryMachine σ) (w : List Bool) (t : ℕ) : σ

The state after t steps on the input w.

def Turing.QueryMachine.output {σ : Type u_1} (M : QueryMachine σ) (w : List Bool) (t : ℕ) : List Bool

The output of a run halted by step t: emissions stop at the first halted state, then the final word is appended. Once the run has halted, increasing t leaves the output unchanged.

theorem Turing.QueryMachine.output_eq_of_not_halted {σ : Type u_1} (M : QueryMachine σ) (w : List Bool) {t : ℕ} (h : ∀ i < t, M.halted (M.run w i) = false) : M.output w t = (List.map (fun (i : ℕ) => M.emit (M.run w i, M.read w (M.run w i))) (List.range t)).flatten ++ M.finish (M.run w t)

Before the first halt, every scheduled step contributes its emission.

@[simp]

theorem Turing.QueryMachine.run_zero {σ : Type u_1} (M : QueryMachine σ) (w : List Bool) : M.run w 0 = M.init

theorem Turing.QueryMachine.run_succ {σ : Type u_1} (M : QueryMachine σ) (w : List Bool) (t : ℕ) : M.run w (t + 1) = M.step w (M.run w t)

theorem Turing.QueryMachine.run_add_of_halted {σ : Type u_1} (M : QueryMachine σ) (w : List Bool) {t : ℕ} (h : M.halted (M.run w t) = true) (k : ℕ) : M.run w (t + k) = M.run w t

A halted machine stays put.

theorem Turing.QueryMachine.halted_run_iff {σ : Type u_1} (M : QueryMachine σ) (w : List Bool) {T : ℕ} (hT : M.halted (M.run w T) = true) (hpre : ∀ t < T, M.halted (M.run w t) = false) (t : ℕ) : M.halted (M.run w t) = true ↔ T ≤ t

After the first halt, the machine is halted and stays put.

theorem Turing.QueryMachine.run_eq_of_le {σ : Type u_1} (M : QueryMachine σ) (w : List Bool) {T : ℕ} (hT : M.halted (M.run w T) = true) {t : ℕ} (h : T ≤ t) : M.run w t = M.run w T

theorem Turing.QueryMachine.output_succ_of_halted {σ : Type u_1} (M : QueryMachine σ) (w : List Bool) {t : ℕ} (h : M.halted (M.run w t) = true) : M.output w (t + 1) = M.output w t

A halted state emits no further step output.

theorem Turing.QueryMachine.output_add_of_halted {σ : Type u_1} (M : QueryMachine σ) (w : List Bool) {t : ℕ} (h : M.halted (M.run w t) = true) (k : ℕ) : M.output w (t + k) = M.output w t

Extra clock steps after halting neither repeat emissions nor append another final word.

The passes of the simulation

@[reducible, inline]

abbrev Turing.QueryMachine.Simulation.PassState (σ : Type u_2) : Type u_2

The state of a pass of the simulation: the state of the machine, the position in the input, and the bit fetched so far.

def Turing.QueryMachine.Simulation.passNext {σ : Type u_1} (M : QueryMachine σ) (p : PassState σ × Bool) : PassState σ

Scanning one input bit: count the position, and fetch the bit if it is the queried one.

def Turing.QueryMachine.Simulation.passEmit {σ : Type u_1} (M : QueryMachine σ) (q : PassState σ) : List Bool

The word emitted at the end of a pass: that of the simulated step.

def Turing.QueryMachine.Simulation.passEnd {σ : Type u_1} (M : QueryMachine σ) (q : PassState σ) : PassState σ

The end of a pass: the simulated step, with the counter and the fetched bit reset.

def Turing.QueryMachine.Simulation.passCont {σ : Type u_1} (M : QueryMachine σ) (q : PassState σ) : Bool

Another pass follows while the machine has not halted.

def Turing.QueryMachine.Simulation.passFinish {σ : Type u_1} (M : QueryMachine σ) (q : PassState σ) : List Bool

The final word.

theorem Turing.QueryMachine.Simulation.streamState_passNext {σ : Type u_1} (M : QueryMachine σ) (w : List Bool) (s : σ) {j : ℕ} (hj : j ≤ w.length) : MultiTapeTM.streamState (s, 0, none) (passNext M) w j = (s, j, (List.take j w)[M.query s]?)

theorem Turing.QueryMachine.Simulation.streamState_passNext_length {σ : Type u_1} (M : QueryMachine σ) (w : List Bool) (s : σ) : MultiTapeTM.streamState (s, 0, none) (passNext M) w w.length = (s, w.length, M.read w s)

theorem Turing.QueryMachine.Simulation.passState_eq {σ : Type u_1} (M : QueryMachine σ) (w : List Bool) (i : ℕ) : MultiTapeTM.passState (M.init, 0, none) (passNext M) (passEnd M) w i = (M.run w i, 0, none)

The parts of the simulation, in linear space

@[reducible, inline]

abbrev Turing.QueryMachine.Simulation.encPass {τ : Type} (encS : τ ↪ List Bool) : PassState τ ↪ List Bool

The encoding of the states of a pass.

theorem Turing.QueryMachine.Simulation.passNext_inSpace {σ' : Type} {M' : QueryMachine σ'} {encS' : σ' ↪ List Bool} (hquery : MultiTapeTM.ComputableInSpace M'.query encS' MultiTapeTM.encNat fun (s : σ') => (encS' s).length) : MultiTapeTM.ComputableInSpace (passNext M') (MultiTapeTM.encPair (encPass encS') MultiTapeTM.encBool) (encPass encS') fun (p : PassState σ' × Bool) => ((MultiTapeTM.encPair (encPass encS') MultiTapeTM.encBool) p).length

theorem Turing.QueryMachine.Simulation.passEmit_inSpace {σ' : Type} {M' : QueryMachine σ'} {encS' : σ' ↪ List Bool} (hemit : MultiTapeTM.ComputableInSpace M'.emit (encStateRead encS') MultiTapeTM.encBits fun (p : σ' × Option Bool) => ((encStateRead encS') p).length) (hhalted : MultiTapeTM.ComputableInSpace M'.halted encS' MultiTapeTM.encBool fun (s : σ') => (encS' s).length) : MultiTapeTM.ComputableInSpace (passEmit M') (encPass encS') MultiTapeTM.encBits fun (q : PassState σ') => ((encPass encS') q).length

theorem Turing.QueryMachine.Simulation.passEnd_inSpace {σ' : Type} {M' : QueryMachine σ'} {encS' : σ' ↪ List Bool} (hnext : MultiTapeTM.ComputableInSpace M'.next (encStateRead encS') encS' fun (p : σ' × Option Bool) => ((encStateRead encS') p).length) (hhalted : MultiTapeTM.ComputableInSpace M'.halted encS' MultiTapeTM.encBool fun (s : σ') => (encS' s).length) : MultiTapeTM.ComputableInSpace (passEnd M') (encPass encS') (encPass encS') fun (q : PassState σ') => ((encPass encS') q).length

theorem Turing.QueryMachine.Simulation.passCont_inSpace {σ' : Type} {M' : QueryMachine σ'} {encS' : σ' ↪ List Bool} (hhalted : MultiTapeTM.ComputableInSpace M'.halted encS' MultiTapeTM.encBool fun (s : σ') => (encS' s).length) : MultiTapeTM.ComputableInSpace (passCont M') (encPass encS') MultiTapeTM.encBool fun (q : PassState σ') => ((encPass encS') q).length

theorem Turing.QueryMachine.Simulation.passFinish_inSpace {σ' : Type} {M' : QueryMachine σ'} {encS' : σ' ↪ List Bool} (hfinish : MultiTapeTM.ComputableInSpace M'.finish encS' MultiTapeTM.encBits fun (s : σ') => (encS' s).length) : MultiTapeTM.ComputableInSpace (passFinish M') (encPass encS') MultiTapeTM.encBits fun (q : PassState σ') => ((encPass encS') q).length

Logarithmic space

theorem Turing.QueryMachine.Simulation.length_encPass_le {τ : Type} (encS : τ ↪ List Bool) (q : PassState τ) : ((encPass encS) q).length ≤ 2 * (encS q.1).length + 2 * (MultiTapeTM.encNat q.2.1).length + 4

theorem Turing.QueryMachine.computableInSpace {α β : Type} {enc : α ↪ List Bool} {encOut : β ↪ List Bool} {σ : Type} {encS : σ ↪ List Bool} (M : QueryMachine σ) (hquery : MultiTapeTM.ComputableInSpace M.query encS MultiTapeTM.encNat fun (s : σ) => (encS s).length) (hnext : MultiTapeTM.ComputableInSpace M.next (encStateRead encS) encS fun (p : σ × Option Bool) => ((encStateRead encS) p).length) (hemit : MultiTapeTM.ComputableInSpace M.emit (encStateRead encS) MultiTapeTM.encBits fun (p : σ × Option Bool) => ((encStateRead encS) p).length) (hhalted : MultiTapeTM.ComputableInSpace M.halted encS MultiTapeTM.encBool fun (s : σ) => (encS s).length) (hfinish : MultiTapeTM.ComputableInSpace M.finish encS MultiTapeTM.encBits fun (s : σ) => (encS s).length) {f : α → β} (time : α → ℕ) (hhalt : ∀ (a : α), M.halted (M.run (enc a) (time a)) = true) (hpre : ∀ (a : α), ∀ t < time a, M.halted (M.run (enc a) t) = false) (hf : ∀ (a : α), encOut (f a) = M.output (enc a) (time a)) (S : α → ℕ) (hlog : ∀ (a : α), (enc a).length.log2 + 1 ≤ S a) (hsize : ∃ (c : ℕ), ∀ (a : α), ∀ t ≤ time a, (encS (M.run (enc a) t)).length ≤ c * S a) : ∃ (t : α → ℕ) (c : ℕ), MultiTapeTM.ComputableInTimeAndSpace f enc encOut t fun (a : α) => c * S a

Query machines run in the space of their states. Let a query machine halt on every encoded input enc a, first after time a steps, with output encOut (f a). If its states along these runs have encodings of length O(S a), where S a is at least logarithmic in the length of the input, and its query, transition, emission, halting test and final word are computable within space linear in the encoded state, then f is computable within space O(S a). The input is not charged, so S may be much smaller than the length of the input.

theorem Turing.QueryMachine.computableInLogSpace {α β : Type} {enc : α ↪ List Bool} {encOut : β ↪ List Bool} {σ : Type} {encS : σ ↪ List Bool} (M : QueryMachine σ) (hquery : MultiTapeTM.ComputableInSpace M.query encS MultiTapeTM.encNat fun (s : σ) => (encS s).length) (hnext : MultiTapeTM.ComputableInSpace M.next (encStateRead encS) encS fun (p : σ × Option Bool) => ((encStateRead encS) p).length) (hemit : MultiTapeTM.ComputableInSpace M.emit (encStateRead encS) MultiTapeTM.encBits fun (p : σ × Option Bool) => ((encStateRead encS) p).length) (hhalted : MultiTapeTM.ComputableInSpace M.halted encS MultiTapeTM.encBool fun (s : σ) => (encS s).length) (hfinish : MultiTapeTM.ComputableInSpace M.finish encS MultiTapeTM.encBits fun (s : σ) => (encS s).length) {f : α → β} (time : α → ℕ) (hhalt : ∀ (a : α), M.halted (M.run (enc a) (time a)) = true) (hpre : ∀ (a : α), ∀ t < time a, M.halted (M.run (enc a) t) = false) (hf : ∀ (a : α), encOut (f a) = M.output (enc a) (time a)) (hsize : ∃ (c : ℕ), ∀ (a : α), ∀ t ≤ time a, (encS (M.run (enc a) t)).length ≤ c * ((enc a).length.log2 + 1)) : MultiTapeTM.ComputableInLogSpace f enc encOut

Query machines run in logarithmic space. Let a query machine halt on every encoded input enc a, first after time a steps, with output encOut (f a). If its states along these runs have encodings of logarithmic length in the length of the input, and its query, transition, emission, halting test and final word are computable within space linear in the encoded state, then f is computable in logarithmic space.