Raw configurations for the multi-tape to TM2 compiler

Main definitions

• Turing.MultiTapeTM.ToTM2.Data: finite stacks representing a binary native configuration.
• Turing.MultiTapeTM.ToTM2.Data.step: apply one native action to the raw configuration.
• Turing.MultiTapeTM.ToTM2.Data.run: execute a native machine with raw stacks.
• Turing.MultiTapeTM.ToTM2.Data.Represents: agreement with a native configuration.

Main results

• Turing.MultiTapeTM.ToTM2.Data.represents_run: raw execution agrees with native execution.
• Turing.MultiTapeTM.ToTM2.Data.input_length_run: input storage is exactly the input length.
• Turing.MultiTapeTM.ToTM2.Data.output_prefix_run: chronological output grows by extension.
• Turing.MultiTapeTM.ToTM2.Data.sum_work_span_run_le: native space bounds raw work storage.

structure Turing.MultiTapeTM.ToTM2.Data (k : ℕ) (State : Type) : Type

A native binary configuration stored as finite stacks, with chronological output.

• state : Option State

  The current state, or none after halting.

• input : Input Bool

  The bounded read-only input zipper.

• work : Fin k → RawTape Bool

  The work tapes, retaining all visited cells.

• output : List Bool

  Symbols emitted so far, in chronological order.

theorem Turing.MultiTapeTM.ToTM2.Data.ext {k : ℕ} {State : Type} {x y : Data k State} (state : x.state = y.state) (input : x.input = y.input) (work : x.work = y.work) (output : x.output = y.output) : x = y

theorem Turing.MultiTapeTM.ToTM2.Data.ext_iff {k : ℕ} {State : Type} {x y : Data k State} : x = y ↔ x.state = y.state ∧ x.input = y.input ∧ x.work = y.work ∧ x.output = y.output

def Turing.MultiTapeTM.ToTM2.Data.init {k : ℕ} {State : Type} (q₀ : State) (input : List Bool) : Data k State

Initialize the input zipper and blank work tapes.

def Turing.MultiTapeTM.ToTM2.Data.step {k : ℕ} {State : Type} (d : Data k State) (a : Action k Bool State) : Data k State

Apply an action, including the output and movement of its final halting step.

noncomputable def Turing.MultiTapeTM.ToTM2.Data.totalStep {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) (d : Data k State) : Data k State

Select and apply the native transition, staying put once halted.

noncomputable def Turing.MultiTapeTM.ToTM2.Data.runFrom {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) (d : Data k State) (t : ℕ) : Data k State

Execute a fixed number of total steps from an arbitrary raw configuration.

noncomputable def Turing.MultiTapeTM.ToTM2.Data.run {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) (input : List Bool) (t : ℕ) : Data k State

Execute a fixed number of total steps from the initial raw configuration.

structure Turing.MultiTapeTM.ToTM2.Data.Represents {k : ℕ} {State : Type} (d : Data k State) {sourceInput : List Bool} (cfg : Cfg k Bool State sourceInput) : Prop

Raw fields agree with the corresponding native state, heads, tapes and output.

• state : d.state = cfg.state

  The control states agree.

• input : d.input.Represents sourceInput cfg.inputPos

  The input zipper represents the native bounded head.

• work (i : Fin k) : (d.work i).Represents (cfg.workTapes i) (cfg.workTapePos i)

  Each work tape represents its native integer-indexed tape and head.

• output : d.output = cfg.output

  Output is chronological in both representations.

@[simp]

theorem Turing.MultiTapeTM.ToTM2.Data.runFrom_zero {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) (d : Data k State) : runFrom tm d 0 = d

theorem Turing.MultiTapeTM.ToTM2.Data.runFrom_succ {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) (d : Data k State) (t : ℕ) : runFrom tm d (t + 1) = totalStep tm (runFrom tm d t)

The next raw configuration is one total step from the preceding configuration.

@[simp]

theorem Turing.MultiTapeTM.ToTM2.Data.run_zero {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) (input : List Bool) : run tm input 0 = init tm.q₀ input

theorem Turing.MultiTapeTM.ToTM2.Data.run_succ {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) (input : List Bool) (t : ℕ) : run tm input (t + 1) = totalStep tm (run tm input t)

The next raw configuration on an input is obtained by one total step.

theorem Turing.MultiTapeTM.ToTM2.Data.totalStep_of_halt {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) {d : Data k State} (h : d.state = none) : totalStep tm d = d

Halted raw configurations are fixed by the total step.

theorem Turing.MultiTapeTM.ToTM2.Data.totalStep_of_state {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) {d : Data k State} {q : State} (h : d.state = some q) : totalStep tm d = d.step (tm.tr q d.input.read fun (i : Fin k) => (d.work i).head)

A live raw configuration applies the transition selected from its current reads.

theorem Turing.MultiTapeTM.ToTM2.Data.Represents.init {k : ℕ} {State : Type} (q₀ : State) (input : List Bool) : (Data.init q₀ input).Represents (Cfg.init q₀ input)

Initialization represents the native initial configuration.

theorem Turing.MultiTapeTM.ToTM2.Data.Represents.step {k : ℕ} {State : Type} {d : Data k State} {sourceInput : List Bool} {cfg : Cfg k Bool State sourceInput} (h : d.Represents cfg) (a : Action k Bool State) : (d.step a).Represents (a.apply cfg)

Applying the same action preserves every field of the representation.

theorem Turing.MultiTapeTM.ToTM2.Data.Represents.totalStep {k : ℕ} {State : Type} {d : Data k State} {sourceInput : List Bool} {cfg : Cfg k Bool State sourceInput} (h : d.Represents cfg) (tm : MultiTapeTM k Bool State) : (Data.totalStep tm d).Represents (MultiTapeTM.step cfg)

Raw and native configurations select the same action and take corresponding total steps.

theorem Turing.MultiTapeTM.ToTM2.Data.Represents.runFrom {k : ℕ} {State : Type} {d : Data k State} {sourceInput : List Bool} {cfg : Cfg k Bool State sourceInput} (h : d.Represents cfg) (tm : MultiTapeTM k Bool State) (t : ℕ) : (Data.runFrom tm d t).Represents (MultiTapeTM.runFrom cfg t)

Any number of raw total steps represents the same number of native total steps.

theorem Turing.MultiTapeTM.ToTM2.Data.represents_run {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) (input : List Bool) (t : ℕ) : (run tm input t).Represents (MultiTapeTM.runFrom (tm.initCfg input) t)

Raw execution from initialization agrees with the native execution, even after halting.

theorem Turing.MultiTapeTM.ToTM2.Data.input_length_run {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) (input : List Bool) (t : ℕ) : (run tm input t).input.left.length + (run tm input t).input.right.length = input.length

At every time, the raw input stacks retain exactly the original input length.

theorem Turing.MultiTapeTM.ToTM2.Data.output_run {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) (input : List Bool) (t : ℕ) : (run tm input t).output = (MultiTapeTM.runFrom (tm.initCfg input) t).output

The raw output is exactly the native chronological output.

theorem Turing.MultiTapeTM.ToTM2.Data.state_run {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) (input : List Bool) (t : ℕ) : (run tm input t).state = (MultiTapeTM.runFrom (tm.initCfg input) t).state

The raw control state agrees with the native state at every time.

theorem Turing.MultiTapeTM.ToTM2.Data.output_prefix_step {k : ℕ} {State : Type} (d : Data k State) (a : Action k Bool State) : d.output <+: (d.step a).output

Each action only appends to the output.

theorem Turing.MultiTapeTM.ToTM2.Data.output_prefix_totalStep {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) (d : Data k State) : d.output <+: (totalStep tm d).output

Total steps only append to the output, including a step which halts.

theorem Turing.MultiTapeTM.ToTM2.Data.output_prefix_run {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) (input : List Bool) {t u : ℕ} (h : t ≤ u) : (run tm input t).output <+: (run tm input u).output

Earlier raw outputs are prefixes of all later raw outputs.

theorem Turing.MultiTapeTM.ToTM2.Data.output_length_run_mono {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) (input : List Bool) : Monotone fun (t : ℕ) => (run tm input t).output.length

The amount of output never decreases.

theorem Turing.MultiTapeTM.ToTM2.Data.run_eq_of_halt {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) (input : List Bool) {t u : ℕ} (hle : t ≤ u) (hhalt : (run tm input t).state = none) : run tm input u = run tm input t

Raw execution stays at its final configuration after halting.

theorem Turing.MultiTapeTM.ToTM2.Data.output_length_run_le_of_halt {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) (input : List Bool) {t : ℕ} (hhalt : (run tm input t).state = none) (u : ℕ) : (run tm input u).output.length ≤ (run tm input t).output.length

Every intermediate output is bounded by the output of a terminating run.

theorem Turing.MultiTapeTM.ToTM2.Data.output_prefix_run_of_computes {k : ℕ} {State : Type} {tm : MultiTapeTM k Bool State} {input output : List Bool} (h : tm.Computes input output) (t : ℕ) : (run tm input t).output <+: output

Every raw output is a prefix of the complete output of a terminating native computation.

theorem Turing.MultiTapeTM.ToTM2.Data.output_length_run_le_of_computes {k : ℕ} {State : Type} {tm : MultiTapeTM k Bool State} {input output : List Bool} (h : tm.Computes input output) (t : ℕ) : (run tm input t).output.length ≤ output.length

A terminating native output bounds every intermediate raw output, without a time term.

theorem Turing.MultiTapeTM.ToTM2.Data.Represents.work_totalStep {k : ℕ} {State : Type} {d : Data k State} {sourceInput : List Bool} {cfg : Cfg k Bool State sourceInput} (h : d.Represents cfg) (tm : MultiTapeTM k Bool State) (i : Fin k) : (Data.totalStep tm d).work i = (d.work i).step (RawTape.nativeAction tm cfg i)

Each raw total step uses precisely the tape action along the represented native step.

theorem Turing.MultiTapeTM.ToTM2.Data.work_run_eq_tape_run {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) (input : List Bool) (t : ℕ) (i : Fin k) : (run tm input t).work i = RawTape.run tm input t i

The work tapes coincide with the raw tapes used by the exact visited-space theorem.

theorem Turing.MultiTapeTM.ToTM2.Data.sum_work_span_run_eq_space {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) (input : List Bool) (t : ℕ) : ∑ i : Fin k, ((run tm input t).work i).span = (MultiTapeNTM.RunPath.ofDeterministic tm (tm.initCfg input) t).space

Summed raw work-tape storage is exactly native visited space.

theorem Turing.MultiTapeTM.ToTM2.Data.sum_work_sides_run_add_eq_space {k : ℕ} {State : Type} (tm : MultiTapeTM k Bool State) (input : List Bool) (t : ℕ) : ∑ i : Fin k, (((run tm input t).work i).left.length + ((run tm input t).work i).right.length) + k = (MultiTapeNTM.RunPath.ofDeterministic tm (tm.initCfg input) t).space

Side-stack storage omits exactly the one current cell held in control for each work tape.

theorem Turing.MultiTapeTM.ToTM2.Data.sum_work_span_run_le {k : ℕ} {State : Type} {tm : MultiTapeTM k Bool State} {input : List Bool} {s : ℕ} (hs : tm.RunsInSpace input s) (t : ℕ) : ∑ i : Fin k, ((run tm input t).work i).span ≤ s

A native space certificate bounds all raw work storage, independently of runtime.

theorem Turing.MultiTapeTM.ToTM2.Data.sum_work_sides_run_le {k : ℕ} {State : Type} {tm : MultiTapeTM k Bool State} {input : List Bool} {s : ℕ} (hs : tm.RunsInSpace input s) (t : ℕ) : ∑ i : Fin k, (((run tm input t).work i).left.length + ((run tm input t).work i).right.length) ≤ s

The sum of raw side-stack lengths is bounded by native space.