Renaming states and symbols

Injections eS of states and eY of symbols rename actions (Turing.Action.map) and configurations (Turing.Cfg.map). The renamed machine Turing.MultiTapeTM.map eS eY tm acts as tm on renamed states and symbols and halts elsewhere, so its runs from renamed configurations are the renamed runs of tm.

Main definitions

• Turing.Action.map, Turing.Cfg.map: renamed actions and configurations.
• Turing.MultiTapeTM.map: the renamed machine.

Main results

• Turing.MultiTapeTM.runFrom_map_map: the run of the renamed machine is the renamed run.

def Turing.Action.map {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Symbol' : Type u_3} {State' : Type u_4} (eS : State ↪ State') (eY : Symbol ↪ Symbol') (a : Action k Symbol State) : Action k Symbol' State'

An action with renamed states and symbols.

@[simp]

theorem Turing.Action.map_inputTape {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Symbol' : Type u_3} {State' : Type u_4} (eS : State ↪ State') (eY : Symbol ↪ Symbol') (a : Action k Symbol State) : (map eS eY a).inputTape = a.inputTape

@[simp]

theorem Turing.Action.map_output {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Symbol' : Type u_3} {State' : Type u_4} (eS : State ↪ State') (eY : Symbol ↪ Symbol') (a : Action k Symbol State) : (map eS eY a).output = Option.map (⇑eY) a.output

@[simp]

theorem Turing.Action.map_workTapes {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Symbol' : Type u_3} {State' : Type u_4} (eS : State ↪ State') (eY : Symbol ↪ Symbol') (a : Action k Symbol State) (i : Fin k) : (map eS eY a).workTapes i = (Option.map (Option.map ⇑eY) (a.workTapes i).1, (a.workTapes i).2)

@[simp]

theorem Turing.Action.map_state {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Symbol' : Type u_3} {State' : Type u_4} (eS : State ↪ State') (eY : Symbol ↪ Symbol') (a : Action k Symbol State) : (map eS eY a).state = Option.map (⇑eS) a.state

def Turing.Cfg.map {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Symbol' : Type u_3} {State' : Type u_4} {input : List Symbol} (eS : State ↪ State') (eY : Symbol ↪ Symbol') (c : Cfg k Symbol State input) : Cfg k Symbol' State' (List.map (⇑eY) input)

A configuration with renamed states and symbols.

@[simp]

theorem Turing.Cfg.map_state {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Symbol' : Type u_3} {State' : Type u_4} {input : List Symbol} (eS : State ↪ State') (eY : Symbol ↪ Symbol') (c : Cfg k Symbol State input) : (map eS eY c).state = Option.map (⇑eS) c.state

@[simp]

theorem Turing.Cfg.map_workTapes {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Symbol' : Type u_3} {State' : Type u_4} {input : List Symbol} (eS : State ↪ State') (eY : Symbol ↪ Symbol') (c : Cfg k Symbol State input) (i : Fin k) (z : ℤ) : (map eS eY c).workTapes i z = Option.map (⇑eY) (c.workTapes i z)

@[simp]

theorem Turing.Cfg.map_output {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Symbol' : Type u_3} {State' : Type u_4} {input : List Symbol} (eS : State ↪ State') (eY : Symbol ↪ Symbol') (c : Cfg k Symbol State input) : (map eS eY c).output = List.map (⇑eY) c.output

@[simp]

theorem Turing.Cfg.map_inputPos {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Symbol' : Type u_3} {State' : Type u_4} {input : List Symbol} (eS : State ↪ State') (eY : Symbol ↪ Symbol') (c : Cfg k Symbol State input) : (map eS eY c).inputPos = Fin.cast ⋯ c.inputPos

@[simp]

theorem Turing.Cfg.map_workTapePos {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Symbol' : Type u_3} {State' : Type u_4} {input : List Symbol} (eS : State ↪ State') (eY : Symbol ↪ Symbol') (c : Cfg k Symbol State input) (a✝ : Fin k) : (map eS eY c).workTapePos a✝ = c.workTapePos a✝

@[simp]

theorem Turing.Cfg.inputSymbol_map {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Symbol' : Type u_3} {State' : Type u_4} {input : List Symbol} (eS : State ↪ State') (eY : Symbol ↪ Symbol') (c : Cfg k Symbol State input) : (map eS eY c).inputSymbol = Option.map (⇑eY) c.inputSymbol

@[simp]

theorem Turing.Cfg.workTapeSymbols_map {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Symbol' : Type u_3} {State' : Type u_4} {input : List Symbol} (eS : State ↪ State') (eY : Symbol ↪ Symbol') (c : Cfg k Symbol State input) (i : Fin k) : (map eS eY c).workTapeSymbols i = Option.map (⇑eY) (c.workTapeSymbols i)

theorem Turing.Cfg.map_init {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Symbol' : Type u_3} {State' : Type u_4} {input : List Symbol} (eS : State ↪ State') (eY : Symbol ↪ Symbol') (q₀ : State) : map eS eY (init q₀ input) = init (eS q₀) (List.map (⇑eY) input)

@[simp]

theorem Turing.Action.apply_map {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Symbol' : Type u_3} {State' : Type u_4} {input : List Symbol} (eS : State ↪ State') (eY : Symbol ↪ Symbol') (a : Action k Symbol State) (c : Cfg k Symbol State input) : (map eS eY a).apply (Cfg.map eS eY c) = Cfg.map eS eY (a.apply c)

def Turing.MultiTapeTM.haltAction {k : ℕ} {Symbol : Type u_1} {State : Type u_2} : Action k Symbol State

The halting action, which leaves every tape alone.

noncomputable def Turing.MultiTapeTM.map {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Symbol' : Type u_3} {State' : Type u_4} (eS : State ↪ State') (eY : Symbol ↪ Symbol') (tm : MultiTapeTM k Symbol State) : MultiTapeTM k Symbol' State'

tm with renamed states and symbols: on renamed states and symbols it acts as tm, elsewhere it halts.

@[simp]

theorem Turing.MultiTapeTM.q₀_map {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Symbol' : Type u_3} {State' : Type u_4} (eS : State ↪ State') (eY : Symbol ↪ Symbol') (tm : MultiTapeTM k Symbol State) : (map eS eY tm).q₀ = eS tm.q₀

@[simp]

theorem Turing.MultiTapeTM.tr_map {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Symbol' : Type u_3} {State' : Type u_4} (eS : State ↪ State') (eY : Symbol ↪ Symbol') (tm : MultiTapeTM k Symbol State) (q : State) (i : Option Symbol) (w : Fin k → Option Symbol) : (map eS eY tm).tr (eS q) (Option.map (⇑eY) i) (Option.map ⇑eY ∘ w) = Action.map eS eY (tm.tr q i w)

theorem Turing.MultiTapeTM.step_map {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Symbol' : Type u_3} {State' : Type u_4} {input : List Symbol} (eS : State ↪ State') (eY : Symbol ↪ Symbol') (tm : MultiTapeTM k Symbol State) (c : Cfg k Symbol State input) : step (Cfg.map eS eY c) = Cfg.map eS eY (step c)

A step of the renamed machine is the renamed step.

theorem Turing.MultiTapeTM.runFrom_map_map {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {Symbol' : Type u_3} {State' : Type u_4} {input : List Symbol} (eS : State ↪ State') (eY : Symbol ↪ Symbol') (tm : MultiTapeTM k Symbol State) (c : Cfg k Symbol State input) (t : ℕ) : runFrom (Cfg.map eS eY c) t = Cfg.map eS eY (runFrom c t)

The run of the renamed machine is the renamed run.