Extending a machine with additional work tapes

extendTapes tm e, for an embedding e : Fin k ↪ Fin k', runs tm inside a machine with more work tapes. The tapes selected by e are used by tm: target tape e j plays the role of source tape j. The remaining tapes are left unchanged.

The configuration map embed e cfg extraTapes extraPos places cfg on the selected tapes and initialises the remaining tapes from extraTapes and extraPos.

The main lemmas show that one step and an entire run of the larger machine mirror the corresponding step and run of tm.

Main definitions

• Turing.MultiTapeTM.partialInv: the partial inverse of the tape embedding.
• Turing.MultiTapeTM.extendTapes: the machine with reindexed work tapes.
• Turing.MultiTapeTM.embed: the corresponding configuration map.
• Turing.MultiTapeTM.tapeEmb: the embedding placing the only tape of a one-tape machine on tape i, and Turing.MultiTapeTM.noTapes: the embedding of a machine without work tapes.

Main results

• Turing.MultiTapeTM.step_embed and Turing.MultiTapeTM.runFrom_embed: the one-step and run-level mirroring lemmas.
• Turing.MultiTapeTM.workTapePos_embed_of_not_range: the extra tapes never move.
• Turing.MultiTapeTM.spaceUsed_embed_le: the resulting space bound.
• Turing.MultiTapeTM.oneTapeCfg: the one-tape view of a configuration.
• Turing.MultiTapeTM.runFrom_tapeEmb, Turing.MultiTapeTM.spaceUsed_tapeEmb_le: the run and the space of a one-tape machine placed on work tape i.
• Turing.MultiTapeTM.TransformsTapes.tapeEmb: a one-tape specification, read on tape i.
• Turing.MultiTapeTM.runFrom_noTapes, Turing.MultiTapeTM.spaceUsed_noTapes_le: the run and the space of a machine without work tapes, placed in a machine with k of them.

def Turing.MultiTapeTM.partialInv {k k' : ℕ} (e : Fin k ↪ Fin k') (l : Fin k') : Option (Fin k)

The computable analogue of Function.partialInv for an embedding e: partialInv e l = some j when e j = l (such j is unique by injectivity), and none when l lies outside the range of e.

Equations

• Turing.MultiTapeTM.partialInv e l = if h : l ∈ Set.range ⇑e then some (e.invOfMemRange ⟨l, h⟩) else none

theorem Turing.MultiTapeTM.partialInv_isPartialInv {k k' : ℕ} (e : Fin k ↪ Fin k') : Function.IsPartialInv (⇑e) (partialInv e)

partialInv e is a partial inverse of e.

noncomputable def Turing.MultiTapeTM.extendTapes {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') : MultiTapeTM k' Symbol State

tm run on the tapes selected by the embedding e, leaving other tapes untouched: work tape e j plays the role of tm's tape j, and any tape outside range e is never written and never moves.

Equations

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

@[simp]

theorem Turing.MultiTapeTM.extendTapes_q₀ {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') : (tm.extendTapes e).q₀ = tm.q₀

def Turing.MultiTapeTM.embed {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) : Cfg k' Symbol State input

A configuration of tm, embedded: tape j goes to tape e j, the tapes outside range e carry the given extraTapes contents and extraPos head positions.

Equations

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

@[simp]

theorem Turing.MultiTapeTM.partialInv_embed {k k' : ℕ} (e : Fin k ↪ Fin k') (j : Fin k) : partialInv e (e j) = some j

The partial inverse recovers the source tape of an embedded tape.

theorem Turing.MultiTapeTM.partialInv_eq_none {k k' : ℕ} (e : Fin k ↪ Fin k') {l : Fin k'} (hl : l ∉ Set.range ⇑e) : partialInv e l = none

Outside the range of e, the partial inverse is undefined.

theorem Turing.MultiTapeTM.partialInv_eq_some {k k' : ℕ} (e : Fin k ↪ Fin k') {l : Fin k'} {j : Fin k} (h : partialInv e l = some j) : e j = l

If the partial inverse is some j, then e j = l.

@[simp]

theorem Turing.MultiTapeTM.embed_inputSymbol {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) : (embed e cfg extraTapes extraPos).inputSymbol = cfg.inputSymbol

@[simp]

theorem Turing.MultiTapeTM.embed_workTapes_embed {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (j : Fin k) : (embed e cfg extraTapes extraPos).workTapes (e j) = cfg.workTapes j

@[simp]

theorem Turing.MultiTapeTM.embed_workTapePos_embed {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (j : Fin k) : (embed e cfg extraTapes extraPos).workTapePos (e j) = cfg.workTapePos j

@[simp]

theorem Turing.MultiTapeTM.embed_workTapeSymbols_embed {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (j : Fin k) : (embed e cfg extraTapes extraPos).workTapeSymbols (e j) = cfg.workTapeSymbols j

theorem Turing.MultiTapeTM.step_embed {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) : step (embed e cfg extraTapes extraPos) = embed e (step cfg) extraTapes extraPos

Reindexing is a step-semiconjugation: the reindexed machine acts on the embedded tapes exactly as tm does, and never touches the extra tapes.

theorem Turing.MultiTapeTM.runFrom_embed {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (n : ℕ) : runFrom (embed e cfg extraTapes extraPos) n = embed e (runFrom cfg n) extraTapes extraPos

The reindexed run mirrors the original, with the extra tapes held fixed throughout.

theorem Turing.MultiTapeTM.workTapePos_embed_of_not_range {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (n : ℕ) {l : Fin k'} (hl : l ∉ Set.range ⇑e) : (runFrom (embed e cfg extraTapes extraPos) n).workTapePos l = extraPos l

The head of a tape outside range e never leaves its starting position.

theorem Turing.MultiTapeTM.spaceUsed_embed_le {k k' : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (tm : MultiTapeTM k Symbol State) (e : Fin k ↪ Fin k') (cfg : Cfg k Symbol State input) (extraTapes : Fin k' → ℤ → Option Symbol) (extraPos : Fin k' → ℤ) (n : ℕ) : spaceUsed (embed e cfg extraTapes extraPos) n ≤ spaceUsed cfg n + (k' - k)

Space bound for a reindexed run. The embedded tapes contribute the space used by tm, while each of the remaining k' - k tapes never moves and contributes at most one cell.

Placing a one-tape machine on a single work tape

def Turing.MultiTapeTM.tapeEmb {k : ℕ} (i : Fin k) : Fin 1 ↪ Fin k

The embedding that places the only work tape of a one-tape machine on tape i.

Equations

• Turing.MultiTapeTM.tapeEmb i = { toFun := fun (x : Fin 1) => i, inj' := ⋯ }

@[simp]

theorem Turing.MultiTapeTM.tapeEmb_apply {k : ℕ} (i : Fin k) (j : Fin 1) : (tapeEmb i) j = i

@[simp]

theorem Turing.MultiTapeTM.range_tapeEmb {k : ℕ} (i : Fin k) : Set.range ⇑(tapeEmb i) = {i}

@[simp]

theorem Turing.MultiTapeTM.partialInv_tapeEmb {k : ℕ} (i l : Fin k) : partialInv (tapeEmb i) l = if l = i then some 0 else none

Tape i is the image of the only tape of a one-tape machine, and no other tape is.

theorem Turing.MultiTapeTM.embed_tapeEmb {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {k : ℕ} (i : Fin k) (cfg : Cfg 1 Symbol State input) (tapes : Fin k → ℤ → Option Symbol) (heads : Fin k → ℤ) : embed (tapeEmb i) cfg tapes heads = { state := cfg.state, inputPos := cfg.inputPos, workTapes := Function.update tapes i (cfg.workTapes 0), workTapePos := Function.update heads i (cfg.workTapePos 0), output := cfg.output }

A one-tape configuration placed on tape i leaves every other tape as it was.

def Turing.MultiTapeTM.oneTapeCfg {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {k : ℕ} (i : Fin k) (cfg : Cfg k Symbol State input) : Cfg 1 Symbol State input

The one-tape view of a configuration of a machine with k work tapes: the tape and head of tape i, with everything else as it is.

Equations

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

theorem Turing.MultiTapeTM.embed_oneTapeCfg {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {k : ℕ} (i : Fin k) (cfg : Cfg k Symbol State input) : embed (tapeEmb i) (oneTapeCfg i cfg) cfg.workTapes cfg.workTapePos = cfg

A configuration is its own one-tape view on tape i, placed back on tape i.

theorem Turing.MultiTapeTM.runFrom_tapeEmb {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {k : ℕ} (tm : MultiTapeTM 1 Symbol State) (i : Fin k) (cfg : Cfg k Symbol State input) (n : ℕ) : runFrom cfg n = embed (tapeEmb i) (runFrom (oneTapeCfg i cfg) n) cfg.workTapes cfg.workTapePos

Running a one-tape machine on work tape i. The run is the run on the one-tape view of the configuration, placed back on tape i; every other tape and head keeps its starting value. Combine with embed_tapeEmb to read off the resulting configuration.

theorem Turing.MultiTapeTM.spaceUsed_tapeEmb_le {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {k : ℕ} (tm : MultiTapeTM 1 Symbol State) (i : Fin k) (cfg : Cfg k Symbol State input) (n : ℕ) : spaceUsed cfg n ≤ spaceUsed (oneTapeCfg i cfg) n + (k - 1)

Space bound for a one-tape machine placed on tape i: the space of the one-tape run, plus one cell for each tape the machine does not use.

theorem Turing.MultiTapeTM.TransformsTapes.tapeEmb {Symbol : Type u_1} {State : Type u_2} {k : ℕ} {tm : MultiTapeTM 1 Symbol State} {P : List Symbol → (Fin 1 → List Symbol) → Prop} {Q : List Symbol → (Fin 1 → List Symbol) → (Fin 1 → List Symbol) → List Symbol → Prop} {t s : ℕ} (h : tm.TransformsTapes P Q t s) (i : Fin k) : (tm.extendTapes (MultiTapeTM.tapeEmb i)).TransformsTapes (fun (input : List Symbol) (ws : Fin k → List Symbol) => P input fun (x : Fin 1) => ws i) (fun (input : List Symbol) (ws ws' : Fin k → List Symbol) (emitted : List Symbol) => ∃ (v : Fin 1 → List Symbol), Q input (fun (x : Fin 1) => ws i) v emitted ∧ ws' = Function.update ws i (v 0)) t (s + (k - 1))

A one-tape specification on tape i. A one-tape machine placed on tape i transforms the word on that tape as it did on its own tape and leaves every other word alone; each remaining tape costs one cell.

def Turing.MultiTapeTM.noTapes (k : ℕ) : Fin 0 ↪ Fin k

The embedding of a machine without work tapes into a machine with k of them.

Equations

• Turing.MultiTapeTM.noTapes k = { toFun := Fin.elim0, inj' := ⋯ }

@[simp]

theorem Turing.MultiTapeTM.partialInv_noTapes {k : ℕ} (l : Fin k) : partialInv (noTapes k) l = none

No tape is in the range of noTapes.

def Turing.MultiTapeTM.noTapesCfg {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {k : ℕ} (cfg : Cfg k Symbol State input) : Cfg 0 Symbol State input

The view of a configuration as a configuration of a machine without work tapes.

Equations

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

theorem Turing.MultiTapeTM.embed_noTapes {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {k : ℕ} (cfg : Cfg 0 Symbol State input) (tapes : Fin k → ℤ → Option Symbol) (heads : Fin k → ℤ) : embed (noTapes k) cfg tapes heads = { state := cfg.state, inputPos := cfg.inputPos, workTapes := tapes, workTapePos := heads, output := cfg.output }

A configuration without work tapes, placed in a machine with k of them, only contributes its state, its input head and its output.

theorem Turing.MultiTapeTM.embed_noTapesCfg {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {k : ℕ} (cfg : Cfg k Symbol State input) : embed (noTapes k) (noTapesCfg cfg) cfg.workTapes cfg.workTapePos = cfg

A configuration is its tapeless view, placed back on its tapes.

theorem Turing.MultiTapeTM.runFrom_noTapes {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {k : ℕ} (tm : MultiTapeTM 0 Symbol State) (cfg : Cfg k Symbol State input) (n : ℕ) : runFrom cfg n = { state := (runFrom (noTapesCfg cfg) n).state, inputPos := (runFrom (noTapesCfg cfg) n).inputPos, workTapes := cfg.workTapes, workTapePos := cfg.workTapePos, output := (runFrom (noTapesCfg cfg) n).output }

Running a machine without work tapes inside a machine with k of them. Only the state, the input head and the output change; every work tape and work head keeps its starting value.

theorem Turing.MultiTapeTM.spaceUsed_noTapes_le {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {k : ℕ} (tm : MultiTapeTM 0 Symbol State) (cfg : Cfg k Symbol State input) (n : ℕ) : spaceUsed cfg n ≤ k

Space bound for a machine without work tapes: one cell for each tape it does not use.