Reusing the binary-track source simulation

The marked-input machine embeds the existing simulator's control after copying. Mapping source symbols to a tagged alphabet adds no source transitions.

def Complexity.MathlibTM0.MarkedMachine.sourceCfg (M : MarkedMachine) (c : M.Config) : M.binary.Config

Embed a source configuration in the alphabet with unused raw-bit symbols.

Equations

• M.sourceCfg c = Turing.TM0.Cfg.map { f := Complexity.MathlibTM0.MarkedMachine.Symbol.source, map_pt' := ⋯ } id c

theorem Complexity.MathlibTM0.MarkedMachine.source_init (M : MarkedMachine) (cells : List M.Alphabet) : M.sourceCfg (Turing.TM0.init cells) = Turing.TM0.init (List.map Symbol.source cells)

theorem Complexity.MathlibTM0.MarkedMachine.source_nth (M : MarkedMachine) (c : M.Config) (j : ℕ) : (M.sourceCfg c).Tape.nth ↑j = Symbol.source (c.Tape.nth ↑j)

theorem Complexity.MathlibTM0.MarkedMachine.source_step (M : MarkedMachine) (c : M.Config) : Turing.TM0.step M.binary.code (M.sourceCfg c) = Option.map M.sourceCfg (Turing.TM0.step M.code c)

theorem Complexity.MathlibTM0.MarkedMachine.source_run (M : MarkedMachine) (t : ℕ) (c : M.Config) : M.binary.run t (M.sourceCfg c) = Option.map M.sourceCfg (M.run t c)

def Complexity.MathlibTM0.MarkedMachine.liftCfg (M : MarkedMachine) {w : List Bool} (d : Turing.Cfg (Fintype.card M.binary.Alphabet) Bool (Control M.State) w) : Turing.Cfg (Fintype.card M.binary.Alphabet) Bool M.TargetState w

Embed a configuration of the existing simulator in the marked-input machine.

Equations

• M.liftCfg d = Turing.Cfg.mapState (Option.map Sum.inr) d

theorem Complexity.MathlibTM0.MarkedMachine.lift_step (M : MarkedMachine) {w : List Bool} (d : Turing.Cfg (Fintype.card M.binary.Alphabet) Bool (Control M.State) w) : Turing.MultiTapeTM.step (M.liftCfg d) = M.liftCfg (Turing.MultiTapeTM.step d)

theorem Complexity.MathlibTM0.MarkedMachine.lift_run (M : MarkedMachine) {w : List Bool} (d : Turing.Cfg (Fintype.card M.binary.Alphabet) Bool (Control M.State) w) (t : ℕ) : Turing.MultiTapeTM.runFrom (M.liftCfg d) t = M.liftCfg (Turing.MultiTapeTM.runFrom d t)