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_reachesIn_initCfg_of_pos {n : ℕ} (tm : TM n) (m : ℕ) (x : List Bool) {t : ℕ} {c' : Cfg n tm.Q} (ht : 0 < t) (h : tm.reachesIn t (tm.initCfg x) c') : (tm.liftTM m).reachesIn t ((tm.liftTM m).initCfg x) (tm.liftCfg m c')

A positive-length run of a lifted machine from genuine initialization has the exact liftCfg endpoint of the underlying run. The positivity hypothesis excludes the sole mismatch at time zero, when the extra tapes have not yet bounced from cell 0 to their canonical parked position at cell 1.

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_reachesIn_retargetCfg_frame {n : ℕ} (tm : TM n) {t : ℕ} {c c' : Cfg n tm.Q} (h : tm.reachesIn t c c') : tm.retargetOutput.reachesIn t (tm.retargetCfg c) (tm.retargetCfg c')

Redirecting output to a fresh work tape preserves every exact run through the canonical configuration embedding.

theorem Complexity.TM.retargetOutput_reachesIn_init_boundary {n : ℕ} (tm : TM n) (x : List Bool) {t : ℕ} {c' : Cfg n tm.Q} (h : tm.reachesIn t (tm.initCfg x) c') : ∃ (C' : Cfg (n + 1) tm.Q), tm.retargetOutput.reachesIn t (tm.retargetOutput.initCfg x) C' ∧ C'.state = c'.state ∧ C'.work (Fin.last n) = c'.output ∧ C'.output.cells = (Tape.init []).cells ∧ C'.output.head ≤ 1

A run of an output-retargeted machine leaves the virtual output on the last work tape and keeps the real output blank with its head at cell zero or one. A subsequent combinator transition therefore parks it at cell one.

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".

theorem Complexity.TM.retargetOutput_computesInTime_boundary {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) ∧ c'.output.cells = (Tape.init []).cells ∧ c'.output.head ≤ 1

Output retargeting with the blank real-output frame exposed. This is the form used by sequential function composition.

theorem Complexity.TM.IsTransducer.liftTM {n : ℕ} {tm : TM n} (h : tm.IsTransducer) (m : ℕ) : (tm.liftTM m).IsTransducer

Padding by unused work tapes preserves one-way output behavior.

theorem Complexity.TM.retargetOutput_isTransducer {n : ℕ} (tm : TM n) : tm.retargetOutput.IsTransducer

Redirecting output to a work tape leaves the real output direction idle, so the resulting machine is always a one-way-output transducer.