Deterministic Multi-Tape Turing Machines are Nondeterministic

Embeds MultiTapeTM into MultiTapeNTM and shows the embedding preserves computation.

toNTM permits exactly the transition tr prescribes: nondeterminism is the possibility of several, so having exactly one is the special case. A deterministic computation is then witnessed by the machine's own run. Both models idle once the machine has halted, so that run has exactly t steps for every t and its measures match runFrom and spaceUsed directly, with no reasoning about the step at which the machine halted.

Important Declarations

• MultiTapeTM.toNTM: every deterministic machine is a nondeterministic one
• MultiTapeTM.toNTMComputationPath: the machine's own run, as a computation of toNTM
• MultiTapeTM.toNTM_computes: every deterministic computation is a nondeterministic one

def Turing.MultiTapeTM.toNTM {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (tm : MultiTapeTM k Symbol State) : MultiTapeNTM k Symbol State

Every deterministic machine is a nondeterministic one whose relation is a singleton.

Equations

• tm.toNTM = { q₀ := tm.q₀, Tr := fun (q : State) (input : Option Symbol) (work : Fin k → Option Symbol) (action : Turing.Action k Symbol State) => action = tm.tr q input work }

@[simp]

theorem Turing.MultiTapeTM.toNTM_initCfg {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (tm : MultiTapeTM k Symbol State) (input : List Symbol) : tm.toNTM.initCfg input = initCfg input

theorem Turing.MultiTapeTM.toNTM_step {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (c : Cfg k Symbol State input) : tm.toNTM.Step c (step c)

Each step of tm is a step of its nondeterministic reading. This holds at a halted configuration too, where both models idle.

theorem Turing.MultiTapeTM.isChain_map_range {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} (cfg : Cfg k Symbol State input) (t : ℕ) : List.IsChain tm.toNTM.Step (List.map (runFrom cfg) (List.range (t + 1)))

The configurations the machine passes through form a chain of steps.

def Turing.MultiTapeTM.toNTMComputationPath {k : ℕ} {State : Type u_1} {Symbol : Type u_2} (tm : MultiTapeTM k Symbol State) (input : List Symbol) (t : ℕ) : tm.toNTM.ComputationPath input

The machine's own run for t steps, as a computation of its nondeterministic reading: the configuration reached after each step.

Equations

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

@[simp]

theorem Turing.MultiTapeTM.toNTMComputationPath_time {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {t : ℕ} : (tm.toNTMComputationPath input t).time = t

@[simp]

theorem Turing.MultiTapeTM.toNTMComputationPath_cfgs {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {t : ℕ} : (tm.toNTMComputationPath input t).cfgs = List.map (runFrom (initCfg input)) (List.range (t + 1))

@[simp]

theorem Turing.MultiTapeTM.toNTMComputationPath_last {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {t : ℕ} : (tm.toNTMComputationPath input t).last = runFrom (initCfg input) t

@[simp]

theorem Turing.MultiTapeTM.toNTMComputationPath_space {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {t : ℕ} : (tm.toNTMComputationPath input t).space = spaceUsed (initCfg input) t

theorem Turing.MultiTapeTM.toNTM_computes {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : List Symbol} {tm : MultiTapeTM k Symbol State} {output : List Symbol} {t s : ℕ} (h : tm.ComputesInTimeAndSpace input output t s) : tm.toNTM.ComputesInExactTimeAndSpace input output t s

Every deterministic computation is a nondeterministic one, witnessed by the machine's own run.