Retargeted-input computation seams

An ordinary machine begins with every head on ▷; its first transition moves all heads right and may also change the control state. A phase-composed machine usually enters its next phase with tapes already parked at cell 1. This file defines an executable wrapper that resumes a machine after that compulsory sentinel transition while reading its input from the last work tape.

Main definitions

• TM.retargetInputStartState — control state after the sentinel transition
• TM.retargetInputStarted — virtual-input machine entered with heads at cell 1
• TM.retargetInputStartedCfg — canonical entry configuration for a virtual input

def Complexity.TM.retargetInputStartState {k : ℕ} (M : TM k) : M.Q

The source control state produced by its first transition from the all-▷ initial head positions.

Equations

• M.retargetInputStartState = (M.δ M.qstart Complexity.Γ.start (fun (x : Fin k) => Complexity.Γ.start) Complexity.Γ.start).1

def Complexity.TM.retargetInputStarted {k : ℕ} (M : TM k) : TM (k + 1)

Read the source input from work tape k, starting from the already-parked post-sentinel configuration. If the source starts halted, the wrapper also starts halted; otherwise its start state is retargetInputStartState M.

The transition function and halt state are exactly those of retargetInput M.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.TM.retargetInputStartedCfg {k : ℕ} (M : TM k) (y : List Bool) (realInput : Tape) : Cfg (k + 1) M.retargetInputStarted.Q

Canonical phase-entry configuration for retargetInputStarted M: virtual input y is on the last work tape at head 1; source work tapes and the real output are parked and blank. The ignored real input tape is arbitrary.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.TM.retargetInputStartedCfg_state {k : ℕ} (M : TM k) (y : List Bool) (realInput : Tape) : (M.retargetInputStartedCfg y realInput).state = M.retargetInputStarted.qstart

@[simp]

theorem Complexity.TM.retargetInputStartedCfg_input {k : ℕ} (M : TM k) (y : List Bool) (realInput : Tape) : (M.retargetInputStartedCfg y realInput).input = realInput

@[simp]

theorem Complexity.TM.retargetInputStartedCfg_output {k : ℕ} (M : TM k) (y : List Bool) (realInput : Tape) : (M.retargetInputStartedCfg y realInput).output = (Tape.init []).move Dir3.right

theorem Complexity.TM.retargetInputStartedCfg_work_lt {k : ℕ} (M : TM k) (y : List Bool) (realInput : Tape) (i : Fin (k + 1)) (h : ↑i < k) : (M.retargetInputStartedCfg y realInput).work i = (Tape.init []).move Dir3.right

@[simp]

theorem Complexity.TM.retargetInputStartedCfg_work_last {k : ℕ} (M : TM k) (y : List Bool) (realInput : Tape) : (M.retargetInputStartedCfg y realInput).work ⟨k, ⋯⟩ = (Tape.init (List.map Γ.ofBool y)).move Dir3.right