Step machines simulating read machines

A read machine reads its input at an address; a Turing.StepMachine sees the cell under its head and moves it by one cell per step. Turing.ReadMachine.toStepMachine keeps the position of the head in its state: before each step of the read machine that reads the address a, it moves the head to the cell of a, at position a + 1, and then takes that step on the bit there. It stops at the blank after the input if a is beyond it, which reads as false, as for the read machine.

Main definitions

• Turing.ReadMachine.toStepMachine: the simulating step machine.

Main results

• Turing.ReadMachine.computes_toStepMachine: if the read machine halts with an output, the step machine computes that output.

def Turing.ReadMachine.stepAt {σ : Type u_1} (m : ReadMachine σ) (q : σ) (pos : ℕ) (b : Bool) : (σ × ℕ) × SignType × List Bool

The step of the read machine, keeping the head position pos.

def Turing.ReadMachine.toStepMachine {σ : Type u_1} (m : ReadMachine σ) : StepMachine (σ × ℕ) Bool Bool

The step machine simulating m, with the position of its head in its state.

def Turing.ReadMachine.Represents {σ : Type u_1} {x : List Bool} (c : Cfg σ) (d : StepMachine.Cfg (σ × ℕ) Bool x) : Prop

The configurations of the step machine that represent c: the state of c with the head at the position in the state, and the same output.

theorem Turing.ReadMachine.stepCfg_read {σ : Type u_1} {m : ReadMachine σ} {x : List Bool} {d : StepMachine.Cfg (σ × ℕ) Bool x} (hhalt : m.halt d.state.1 = false) {b : Bool} (hb : m.toStepMachine.step d.state (MultiTapeTM.inputSymbolAt x d.pos) = m.stepAt d.state.1 d.state.2 b) : m.toStepMachine.stepCfg d = { state := ((m.step d.state.1 b).1, d.state.2), pos := d.pos, out := d.out ++ (m.step d.state.1 b).2 }

The step of the read machine itself.

theorem Turing.ReadMachine.readBit_eq {σ : Type u_1} {m : ReadMachine σ} {x : List Bool} {q : σ} {A : ℕ} (h : m.addr q = some A) : m.readBit x q = x.getD A false

theorem Turing.ReadMachine.exists_iterate_stepCfg_some {σ : Type u_1} {m : ReadMachine σ} {x : List Bool} {q : σ} {A : ℕ} (hA : m.addr q = some A) (hhalt : m.halt q = false) (out : List Bool) (w : ℕ) (d : StepMachine.Cfg (σ × ℕ) Bool x) : d.state = (q, ↑d.pos) → d.out = out → ↑d.pos - (A + 1) + (A + 1 - ↑d.pos) ≤ w → ∃ (k : ℕ), Represents (m.next x { state := q, out := out }) (m.toStepMachine.stepCfg^[k] d)

The walk of the head to the cell of the address read next, and the step there.

theorem Turing.ReadMachine.exists_iterate_stepCfg {σ : Type u_1} {m : ReadMachine σ} {x : List Bool} {c : Cfg σ} {d : StepMachine.Cfg (σ × ℕ) Bool x} (h : Represents c d) : ∃ (k : ℕ), Represents (m.next x c) (m.toStepMachine.stepCfg^[k] d)

One step of the read machine is simulated by steps of the step machine; a halted read machine stays put, in zero steps.

theorem Turing.ReadMachine.exists_run_represents {σ : Type u_1} {m : ReadMachine σ} (x : List Bool) (n : ℕ) : ∃ (t : ℕ), Represents (m.run x n) (m.toStepMachine.run x t)

The steps of the read machine are simulated by the step machine.

theorem Turing.ReadMachine.computes_toStepMachine {σ : Type u_1} {m : ReadMachine σ} {x : List Bool} {n : ℕ} (h : m.halt (m.run x n).state = true) : m.toStepMachine.Computes x (m.run x n).out

The step machine computes the output of the read machine, if it halts.

def Turing.ReadMachine.Follows {σ : Type u_1} {m : ReadMachine σ} (x : List Bool) (d : StepMachine.Cfg (σ × ℕ) Bool x) : Prop

The configurations of the step machine on x that follow the read machine: the head at the position in the state, and the state and the output of a configuration of the read machine.

theorem Turing.ReadMachine.Follows.stepCfg {σ : Type u_1} {m : ReadMachine σ} {x : List Bool} {d : StepMachine.Cfg (σ × ℕ) Bool x} (h : Follows x d) : Follows x (m.toStepMachine.stepCfg d)

A step of the step machine keeps it following the read machine.

theorem Turing.ReadMachine.exists_state_run {σ : Type u_1} {m : ReadMachine σ} (x : List Bool) (t : ℕ) : ∃ (j : ℕ), (m.toStepMachine.run x t).state = ((m.run x j).state, (m.toStepMachine.run x t).state.2) ∧ (m.toStepMachine.run x t).state.2 ≤ x.length + 1

The states of the step machine: every state it reaches is a state of the read machine, with a position at most the length of the input plus one.