Step machines

A step machine reads its input with a two-way head and keeps an arbitrary state. In each step, a pure function of the state and the symbol under the head gives the next state, a move of the head by at most one cell and a word to emit. It halts in the states where halt holds.

Step machines describe space-bounded computations without tapes: the space of a computation is the size of its states, while the position of the head costs nothing, since a Turing machine realizing the step machine keeps its input head at the same position. A machine whose states take at most s bits halts on an input of length n within (n + 2) * 3 ^ s steps, if it halts at all, since it never repeats a state and a head position before halting; in particular, a machine in logarithmic space halts within polynomially many steps.

Main definitions

• Turing.StepMachine: step machines.
• Turing.StepMachine.run: the configuration after a number of steps.
• Turing.StepMachine.HaltsAt: the first step at which a machine has halted.
• Turing.StepMachine.Simulates: a step machine simulates a system, with a fixed number of its steps per step of the system.

Main results

• Turing.StepMachine.Simulates.exists_haltsAt: a simulating machine halts when the simulated system does, with the same output.
• Turing.StepMachine.HaltsAt.lt_three_pow: a machine whose states take at most s bits halts within (n + 2) * 3 ^ s steps.
• Turing.StepMachine.HaltsAt.lt_pow_of_log: in space c * log₂ (n + 2), a machine halts within (n + 2) ^ (2 * c + 1) steps.

structure Turing.StepMachine (σ : Type u_1) (Γ : Type u_2) (Out : Type u_3) : Type (max (max u_1 u_2) u_3)

A step machine with states σ, input symbols Γ and output symbols Out: from the state q with a under the head, it moves to (step q a).1, moves its head by (step q a).2.1 and emits (step q a).2.2, unless halt q. The symbol under the head is none on the blanks before and after the input, and the head does not move beyond them. Returning to the start of the input needs no move of its own: move left until the blank before the input, then right.

• init : σ

  The initial state.

• halt : σ → Bool

  The halting states.

• step : σ → Option Γ → σ × SignType × List Out

  The next state, the move of the head and the emitted word.

structure Turing.StepMachine.Cfg {Γ : Type u_2} (σ : Type u_4) (Out : Type u_5) (input : List Γ) : Type (max u_4 u_5)

A configuration on input: the state, the position of the head and the output so far.

• state : σ

  The state.

• pos : Fin (input.length + 2)

  The position of the head, with the blanks at 0 and input.length + 1.

• out : List Out

  The output so far.

def Turing.StepMachine.initCfg {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} (m : StepMachine σ Γ Out) (input : List Γ) : Cfg σ Out input

The initial configuration: the initial state, the head on the first cell, no output.

def Turing.StepMachine.stepAt {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} (m : StepMachine σ Γ Out) {input : List Γ} (c : Cfg σ Out input) : σ × SignType × List Out

The step from the configuration c, on the symbol under its head.

def Turing.StepMachine.stepCfg {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} (m : StepMachine σ Γ Out) {input : List Γ} (c : Cfg σ Out input) : Cfg σ Out input

One step, unless the machine has halted.

def Turing.StepMachine.run {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} (m : StepMachine σ Γ Out) (input : List Γ) (t : ℕ) : Cfg σ Out input

The configuration after t steps on input.

def Turing.StepMachine.HaltsAt {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} (m : StepMachine σ Γ Out) (input : List Γ) (t : ℕ) : Prop

The machine has halted after exactly t steps, and not before.

def Turing.StepMachine.Computes {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} (m : StepMachine σ Γ Out) (input : List Γ) (out : List Out) : Prop

The machine halts on input with the output out.

def Turing.StepMachine.Cfg.core {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} {input : List Γ} (c : Cfg σ Out input) : σ × Fin (input.length + 2)

The state and the position of the head: all that the next steps depend on.

theorem Turing.StepMachine.run_succ {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} (m : StepMachine σ Γ Out) {input : List Γ} (t : ℕ) : m.run input (t + 1) = m.stepCfg (m.run input t)

theorem Turing.StepMachine.run_succ_of_not_halt {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} (m : StepMachine σ Γ Out) {input : List Γ} {t : ℕ} (h : m.halt (m.run input t).state = false) : m.run input (t + 1) = { state := (m.stepAt (m.run input t)).1, pos := moveInputPos (m.run input t).pos (m.stepAt (m.run input t)).2.1, out := (m.run input t).out ++ (m.stepAt (m.run input t)).2.2 }

A step from a configuration that has not halted.

theorem Turing.StepMachine.out_run {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} (m : StepMachine σ Γ Out) {input : List Γ} {t : ℕ} (ht : ∀ i < t, m.halt (m.run input i).state = false) : (m.run input t).out = (List.map (fun (i : ℕ) => (m.stepAt (m.run input i)).2.2) (List.range t)).flatten

Before halting, the output is what the steps emitted.

theorem Turing.StepMachine.out_run_prefix {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} (m : StepMachine σ Γ Out) {input : List Γ} {r t : ℕ} (h : r ≤ t) : (m.run input r).out <+: (m.run input t).out

The output only grows.

theorem Turing.StepMachine.run_add_of_halt {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} (m : StepMachine σ Γ Out) {input : List Γ} {t : ℕ} (h : m.halt (m.run input t).state = true) (n : ℕ) : m.run input (t + n) = m.run input t

A halted machine stays put.

theorem Turing.StepMachine.exists_haltsAt_le {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} (m : StepMachine σ Γ Out) {input : List Γ} {T : ℕ} (h : m.halt (m.run input T).state = true) : ∃ t ≤ T, m.HaltsAt input t ∧ m.run input t = m.run input T

A machine that has halted by the time T halts at some time up to T, with the configuration it has at T.

Simulations

structure Turing.StepMachine.Simulates {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} (m : StepMachine σ Γ Out) {α : Type u_4} (input : List Γ) (next : α → α) (halt : α → Bool) (out : α → List Out) (R : α → Cfg σ Out input → Prop) (d : ℕ) : Prop

m on input simulates the system next along R, with d steps of m per step of the system: R is kept by d steps from a state that has not halted, and matches the halting flags and the outputs.

• step (a : α) (c : Cfg σ Out input) : R a c → halt a = false → R (next a) (m.stepCfg^[d] c)
• halt_eq (a : α) (c : Cfg σ Out input) : R a c → m.halt c.state = halt a
• out_eq (a : α) (c : Cfg σ Out input) : R a c → c.out = out a

theorem Turing.StepMachine.Simulates.run {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} {m : StepMachine σ Γ Out} {input : List Γ} {α : Type u_4} {a₀ : α} {next : α → α} {halt : α → Bool} {out : α → List Out} {R : α → Cfg σ Out input → Prop} {d t₀ : ℕ} (h : m.Simulates input next halt out R d) (h₀ : R a₀ (m.run input t₀)) {u : ℕ} (hu : ∀ i < u, halt (next^[i] a₀) = false) : R (next^[u] a₀) (m.run input (t₀ + u * d))

From R at the time t₀, after u steps of the system, m has made u * d more steps along R.

theorem Turing.StepMachine.Simulates.exists_round {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} {m : StepMachine σ Γ Out} {input : List Γ} {α : Type u_4} {a₀ : α} {next : α → α} {halt : α → Bool} {out : α → List Out} {R : α → Cfg σ Out input → Prop} {d t₀ : ℕ} (h : m.Simulates input next halt out R d) (h₀ : R a₀ (m.run input t₀)) {u : ℕ} (hu : ∀ i < u, halt (next^[i] a₀) = false) (hd : 0 < d) {i : ℕ} (hi : i ≤ u * d) : ∃ (q : ℕ), ∃ j < d, (q < u ∨ q = u ∧ j = 0) ∧ R (next^[q] a₀) (m.run input (t₀ + q * d)) ∧ m.run input (t₀ + i) = m.stepCfg^[j] (m.run input (t₀ + q * d))

The rounds of a simulation: within u steps of the system, every time of m is j < d steps into a round q, which starts along R.

theorem Turing.StepMachine.Simulates.exists_haltsAt {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} {m : StepMachine σ Γ Out} {input : List Γ} {α : Type u_4} {a₀ : α} {next : α → α} {halt : α → Bool} {out : α → List Out} {R : α → Cfg σ Out input → Prop} {d t₀ : ℕ} (h : m.Simulates input next halt out R d) (h₀ : R a₀ (m.run input t₀)) {u : ℕ} (hu : ∀ i < u, halt (next^[i] a₀) = false) (hend : halt (next^[u] a₀) = true) : ∃ t ≤ t₀ + u * d, m.HaltsAt input t ∧ (m.run input t).out = out (next^[u] a₀)

Simulation: from R at the time t₀, when the system halts after u steps, m halts within u * d more steps, with the same output.

theorem Turing.StepMachine.core_stepCfg {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} (m : StepMachine σ Γ Out) {input : List Γ} {c₁ c₂ : Cfg σ Out input} (h : c₁.core = c₂.core) : (m.stepCfg c₁).core = (m.stepCfg c₂).core

The next core depends only on the current one.

theorem Turing.StepMachine.core_iterate {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} (m : StepMachine σ Γ Out) {input : List Γ} {c₁ c₂ : Cfg σ Out input} (h : c₁.core = c₂.core) (n : ℕ) : (m.stepCfg^[n] c₁).core = (m.stepCfg^[n] c₂).core

Runs from configurations with the same core keep having the same core.

theorem Turing.StepMachine.HaltsAt.core_ne_of_lt {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} (m : StepMachine σ Γ Out) {input : List Γ} {t i j : ℕ} (ht : m.HaltsAt input t) (hij : i < j) (hjt : j ≤ t) : (m.run input i).core ≠ (m.run input j).core

A machine never repeats a core before halting: a core shared by the steps i < j ≤ t would give the halted state of step t already at step t - j + i < t.

theorem Turing.StepMachine.HaltsAt.injOn_core {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} (m : StepMachine σ Γ Out) {input : List Γ} {t : ℕ} (ht : m.HaltsAt input t) : Set.InjOn (fun (i : ℕ) => (m.run input i).core) (Set.Iic t)

Before halting, the cores of a run are pairwise distinct.

theorem Turing.StepMachine.HaltsAt.lt_three_pow {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} (m : StepMachine σ Γ Out) {input : List Γ} (enc : σ ↪ List Bool) {s t : ℕ} (hs : ∀ (i : ℕ), (enc (m.run input i).state).length ≤ s) (ht : m.HaltsAt input t) : t < (input.length + 2) * 3 ^ s

A machine whose states take at most s bits halts within (n + 2) * 3 ^ s steps on an input of length n: its runs never repeat a state and a head position before halting, and there are fewer than 3 ^ s words of at most s bits.

theorem Turing.StepMachine.HaltsAt.lt_pow_of_log {σ : Type u_1} {Γ : Type u_2} {Out : Type u_3} (m : StepMachine σ Γ Out) {input : List Γ} (enc : σ ↪ List Bool) {c t : ℕ} (hs : ∀ (i : ℕ), (enc (m.run input i).state).length ≤ c * Nat.log 2 (input.length + 2)) (ht : m.HaltsAt input t) : t < (input.length + 2) ^ (2 * c + 1)

Logarithmic space gives polynomial time: a machine whose states take at most c * log₂ (n + 2) bits halts within (n + 2) ^ (2 * c + 1) steps on an input of length n.