Machines reading their input by address

A read machine has a state, and in each state either halts or takes a step. A step may read the bit of the input at an address given by the state, and may emit output bits. It is a convenient intermediate model for space-bounded algorithms that consult their input at computed positions: Turing.StepMachines, which move a head one cell at a time, simulate read machines by keeping the head position in their state.

Main definitions

• Turing.ReadMachine: read machines, with an initial state, a halting test, the address read by a step and the step itself.
• Turing.ReadMachine.run: the configuration after a number of steps.

Main results

• Turing.ReadMachine.run_add: runs compose.
• Turing.ReadMachine.runFrom_loop: a loop of a read machine, emitting a word in each round.

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

A machine reading its input by address. In a state q that is not halting, it reads the input bit at addr q (if any; false beyond the input or without an address), and moves to (step q b).1, emitting (step q b).2.

• init : σ

  The initial state.

• halt : σ → Bool

  The halting states.

• addr : σ → Option ℕ

  The address of the input bit read by the next step, if any.

• step : σ → Bool → σ × List Bool

  The next state and the emitted bits, given the bit read.

structure Turing.ReadMachine.Cfg (σ : Type u_2) : Type u_2

A configuration: the state and the output so far.

• state : σ

  The state.

• out : List Bool

  The output so far.

def Turing.ReadMachine.readBit {σ : Type u_1} (m : ReadMachine σ) (x : List Bool) (q : σ) : Bool

The bit read in state q.

def Turing.ReadMachine.next {σ : Type u_1} (m : ReadMachine σ) (x : List Bool) (c : Cfg σ) : Cfg σ

One step on the input x; halting configurations are fixed.

def Turing.ReadMachine.runFrom {σ : Type u_1} (m : ReadMachine σ) (x : List Bool) (c : Cfg σ) (n : ℕ) : Cfg σ

The configuration after n steps on the input x, from c.

def Turing.ReadMachine.run {σ : Type u_1} (m : ReadMachine σ) (x : List Bool) (n : ℕ) : Cfg σ

The configuration after n steps on the input x.

theorem Turing.ReadMachine.runFrom_add {σ : Type u_1} (m : ReadMachine σ) (x : List Bool) (c : Cfg σ) (n k : ℕ) : m.runFrom x c (n + k) = m.runFrom x (m.runFrom x c n) k

theorem Turing.ReadMachine.run_add {σ : Type u_1} (m : ReadMachine σ) (x : List Bool) (n k : ℕ) : m.run x (n + k) = m.runFrom x (m.run x n) k

theorem Turing.ReadMachine.runFrom_one {σ : Type u_1} (m : ReadMachine σ) (x : List Bool) (c : Cfg σ) : m.runFrom x c 1 = m.next x c

theorem Turing.ReadMachine.runFrom_succ {σ : Type u_1} (m : ReadMachine σ) (x : List Bool) (c : Cfg σ) (n : ℕ) : m.runFrom x c (n + 1) = m.runFrom x (m.next x c) n

theorem Turing.ReadMachine.next_of_not_halt {σ : Type u_1} (m : ReadMachine σ) (x : List Bool) {c : Cfg σ} (h : m.halt c.state = false) : m.next x c = { state := (m.step c.state (m.readBit x c.state)).fst, out := c.out ++ (m.step c.state (m.readBit x c.state)).snd }

A step from a state that is not halting.

theorem Turing.ReadMachine.runFrom_of_halt {σ : Type u_1} (m : ReadMachine σ) (x : List Bool) {c : Cfg σ} (h : m.halt c.state = true) (n : ℕ) : m.runFrom x c n = c

Halting configurations are fixed.

theorem Turing.ReadMachine.run_eq_of_halt {σ : Type u_1} (m : ReadMachine σ) (x : List Bool) {n n' : ℕ} (h : m.halt (m.run x n).state = true) (hn : n ≤ n') : m.run x n' = m.run x n

After halting, the configuration stays.

theorem Turing.ReadMachine.runFrom_loop {σ : Type u_1} (m : ReadMachine σ) (x : List Bool) (s : ℕ → σ) (e : ℕ → List Bool) {M : ℕ} (h : ∀ (i : ℕ), i < M → m.halt (s i) = false ∧ m.step (s i) (m.readBit x (s i)) = (s (i + 1), e i)) (out : List Bool) {j : ℕ} (hj : j ≤ M) : m.runFrom x { state := s 0, out := out } j = { state := s j, out := out ++ (List.map e (List.range j)).flatten }

A loop of a read machine: if from the state s i the machine steps to s (i + 1) and emits e i, for i < M, then after j ≤ M steps from s 0 it is in s j, having emitted e 0, …, e (j - 1).