Tape-layout combinators: extra work tapes and output retargeting

Two DTM combinators that change a machine's tape layout without changing its behavior:

• TM.liftTM tm m — pad tm : TM n with m never-used work tapes, giving a TM (n + m) that decides/computes exactly as tm does, in the same time bound. The extra tapes bounce off ▷ on the first step (respecting δ_right_of_start) and then park at cell 1 forever, writing □ over the □ already there.
• TM.retargetOutput tm — redirect the output actions of tm : TM n to a fresh work tape n (the Fin.last n tape), giving a TM (n + 1) whose real output tape is idled. Used to "compute a value onto a work tape", e.g. materializing a clock value for downstream composition.

Correspondence proofs

Both combinators are proved correct by a step-commutation lemma through a configuration embedding (liftCfg / retargetCfg): one step of the derived machine on an embedded configuration equals one step of tm, embedded. The embeddings park the dummy tapes at cell 1 with blank cells; the initial configuration instead has dummy heads at cell 0 (on ▷), so the step lemma is stated for any dummy tape with cells = Tape.init [] and head ≤ 1 — covering both the initial bounce and the parked steady state (mirroring NTM.pad0).

The time bounds are preserved exactly (no + 1): the dummy-tape bounce happens during the simulated machine's own first step.

def Complexity.TM.liftTM {n : ℕ} (tm : TM n) (m : ℕ) : TM (n + m)

Pad tm : TM n with m never-used work tapes. Work tapes 0..n-1 (indexed by Fin.castAdd m i) behave exactly as tm's; the extra tapes n..n+m-1 write back what they read (readBackWrite) and idle (idleDir): they bounce off ▷ at the first step and then park at cell 1 forever. Input and output behavior is unchanged.

Equations

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

def Complexity.TM.liftCfg {n : ℕ} (tm : TM n) (m : ℕ) (c : Cfg n tm.Q) : Cfg (n + m) tm.Q

Embed a configuration of tm : TM n into one of tm.liftTM m: work tapes i < n are c's, the extras are the canonical parked blank tape (head 1, blank cells). State, input, and output are shared.

Equations

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

@[simp]

theorem Complexity.TM.liftCfg_state {n : ℕ} (tm : TM n) (m : ℕ) (c : Cfg n tm.Q) : (tm.liftCfg m c).state = c.state

liftCfg leaves the state unchanged.

@[simp]

theorem Complexity.TM.liftCfg_input {n : ℕ} (tm : TM n) (m : ℕ) (c : Cfg n tm.Q) : (tm.liftCfg m c).input = c.input

liftCfg leaves the input tape unchanged.

@[simp]

theorem Complexity.TM.liftCfg_output {n : ℕ} (tm : TM n) (m : ℕ) (c : Cfg n tm.Q) : (tm.liftCfg m c).output = c.output

liftCfg leaves the output tape unchanged.

theorem Complexity.TM.liftCfg_work_lt {n : ℕ} (tm : TM n) (m : ℕ) (c : Cfg n tm.Q) (i : Fin (n + m)) (h : ↑i < n) : (tm.liftCfg m c).work i = c.work ⟨↑i, h⟩

liftCfg maps the first n work tapes to c's work tapes.

theorem Complexity.TM.liftCfg_work_ge {n : ℕ} (tm : TM n) (m : ℕ) (c : Cfg n tm.Q) (i : Fin (n + m)) (h : n ≤ ↑i) : (tm.liftCfg m c).work i = (Tape.init []).move Dir3.right

liftCfg maps the extra work tapes to the parked blank tape.

theorem Complexity.TM.liftTM_step_liftCfg {n : ℕ} (tm : TM n) (m : ℕ) (c : Cfg n tm.Q) : (tm.liftTM m).step (tm.liftCfg m c) = Option.map (tm.liftCfg m) (tm.step c)

Step commutation on embedded configurations: once the extra tapes are parked, tm.liftTM m steps exactly as tm does through liftCfg.

theorem Complexity.TM.liftTM_decidesInTime {n : ℕ} (tm : TM n) (m : ℕ) {L : Language} {T : ℕ → ℕ} (h : tm.DecidesInTime L T) : (tm.liftTM m).DecidesInTime L T

Lifting preserves deciding, with the same time bound. The extra work tapes never interfere: the lifted machine's run tracks tm's run step for step.

theorem Complexity.TM.liftTM_computesInTime {n : ℕ} (tm : TM n) (m : ℕ) {f : List Bool → List Bool} {T : ℕ → ℕ} (h : tm.ComputesInTime f T) : (tm.liftTM m).ComputesInTime f T

Lifting preserves function computation, with the same time bound.

theorem Complexity.TM.liftTM_decidesInSpace {n : ℕ} (tm : TM n) (m : ℕ) {L : Language} {S : ℕ → ℕ} (h : tm.DecidesInSpace L S) : (tm.liftTM m).DecidesInSpace L fun (k : ℕ) => max (S k) 1

Lifting preserves space bounds up to the parked cell. The extra work tapes' heads never move past cell 1, so tm.liftTM m decides L in space max (S ·) 1.

def Complexity.TM.retargetOutput {n : ℕ} (tm : TM n) : TM (n + 1)

Redirect tm's output actions to a fresh work tape. retargetOutput tm : TM (n + 1) behaves like tm, except that the output write and direction are applied to work tape n (the Fin.last n tape), whose read is fed to tm.δ as the virtual output head; the real output tape is idled (readBackWrite/idleDir). Work tapes 0..n-1 (indexed by Fin.castSucc i) and the input tape behave as before.

Equations

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

def Complexity.TM.retargetCfg {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) : Cfg (n + 1) tm.Q

Embed a configuration of tm : TM n into one of tm.retargetOutput: work tapes i < n are c's, work tape n is c's output tape, and the real output tape is the canonical parked blank tape.

Equations

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

@[simp]

theorem Complexity.TM.retargetCfg_state {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) : (tm.retargetCfg c).state = c.state

retargetCfg leaves the state unchanged.

@[simp]

theorem Complexity.TM.retargetCfg_input {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) : (tm.retargetCfg c).input = c.input

retargetCfg leaves the input tape unchanged.

theorem Complexity.TM.retargetCfg_work_lt {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) (i : Fin (n + 1)) (h : ↑i < n) : (tm.retargetCfg c).work i = c.work ⟨↑i, h⟩

retargetCfg maps the first n work tapes to c's work tapes.

theorem Complexity.TM.retargetCfg_work_last {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) : (tm.retargetCfg c).work (Fin.last n) = c.output

retargetCfg maps the last work tape to c's output tape.

theorem Complexity.TM.retargetOutput_step_retargetCfg {n : ℕ} (tm : TM n) (c : Cfg n tm.Q) : tm.retargetOutput.step (tm.retargetCfg c) = Option.map tm.retargetCfg (tm.step c)

Step commutation on embedded configurations: once the real output tape is parked, tm.retargetOutput steps exactly as tm does through retargetCfg.

theorem Complexity.TM.retargetOutput_computesInTime {n : ℕ} (tm : TM n) {f : List Bool → List Bool} {T : ℕ → ℕ} (h : tm.ComputesInTime f T) (x : List Bool) : ∃ (c' : Cfg (n + 1) tm.Q), ∃ t ≤ T x.length, tm.retargetOutput.reachesIn t (tm.retargetOutput.initCfg x) c' ∧ tm.retargetOutput.halted c' ∧ (c'.work (Fin.last n)).HasOutput (f x)

Output retargeting preserves computation, with the same time bound. If tm computes f within time T, then retargetOutput tm halts within T(|x|) steps with f x written on work tape n (the Fin.last n tape). This is the form needed to compose "compute a clock value onto a work tape".