Effect-free specializations of the common machine

With no oracle channels, an action is exactly an upstream Turing.Action and a configuration is exactly an upstream Turing.Cfg. Choosing Id or Set supplies the deterministic or nondeterministic transition interface. The conversions preserve each step, including halted and stuck configurations; there is no clock rescaling or simulation overhead.

Main definitions

• Turing.MultiTapeMachine.Action.emptyOracleEquiv: remove empty communication instructions.
• Turing.MultiTapeMachine.Config.emptyOracleEquiv: remove empty communication state.
• Turing.MultiTapeTM.toMachine, Turing.MultiTapeNTM.toMachine: embed upstream machines.
• Turing.MultiTapeMachine.toTM, Turing.MultiTapeMachine.toNTM: recover upstream machines.

Main results

• Turing.MultiTapeMachine.step_toTM: deterministic steps commute with conversion.
• Turing.MultiTapeMachine.step_toNTM_iff: nondeterministic steps commute with conversion.

def Turing.MultiTapeMachine.Action.emptyOracleEquiv {k : ℕ} {Symbol : Type u_1} {State : Type u_2} : Action k Symbol State Empty ≃ Turing.Action k Symbol State

With no channels there are no queries or communication updates.

def Turing.MultiTapeMachine.Config.emptyOracleEquiv {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} : Config k Symbol State Empty input ≃ Cfg k Symbol State input

Empty communication state contains no information beyond the upstream configuration.

theorem Turing.MultiTapeMachine.Config.eq_iff_tapes_eq {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} {cfg cfg' : Config k Symbol State Empty input} : cfg = cfg' ↔ cfg.tapes = cfg'.tapes

A configuration without communication channels is determined by its tapes.

def Turing.MultiTapeMachine.toTM {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (machine : MultiTapeMachine k Symbol State Empty Id) : MultiTapeTM k Symbol State

Recover the deterministic upstream machine from an effect-free transition table.

def Turing.MultiTapeMachine.toNTM {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (machine : MultiTapeMachine k Symbol State Empty Set) : MultiTapeNTM k Symbol State

Recover the nondeterministic upstream transition relation from the set of permitted actions.

def Turing.MultiTapeMachine.step {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeMachine k Symbol State Empty Id) (cfg : Config k Symbol State Empty input) : Config k Symbol State Empty input

One deterministic step without oracle channels. Halted configurations are fixed points.

def Turing.MultiTapeMachine.Step {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeMachine k Symbol State Empty Set) (cfg next : Config k Symbol State Empty input) : Prop

One nondeterministic step without channels. Empty transition sets remain stuck, while halted configurations step only to themselves, as in upstream's relation.

theorem Turing.MultiTapeMachine.initialConfig_toTM {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (machine : MultiTapeMachine k Symbol State Empty Id) (input : List Symbol) : (machine.initialConfig input).tapes = machine.toTM.initCfg input

The initial configurations correspond without modifying any tape.

theorem Turing.MultiTapeMachine.initialConfig_toNTM {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (machine : MultiTapeMachine k Symbol State Empty Set) (input : List Symbol) : (machine.initialConfig input).tapes = machine.toNTM.initCfg input

The initial configurations correspond for a nondeterministic transition table.

theorem Turing.MultiTapeMachine.step_toTM {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeMachine k Symbol State Empty Id) (cfg : Config k Symbol State Empty input) : (machine.step cfg).tapes = MultiTapeTM.step cfg.tapes

Recovering an upstream machine preserves a deterministic step exactly.

theorem Turing.MultiTapeMachine.step_toNTM_iff {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {input : List Symbol} (machine : MultiTapeMachine k Symbol State Empty Set) (cfg next : Config k Symbol State Empty input) : machine.Step cfg next ↔ machine.toNTM.Step cfg.tapes next.tapes

Recovering an upstream machine preserves all nondeterministic successors, including the absence of successors at a stuck configuration.

noncomputable def Turing.MultiTapeTM.toMachine {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (machine : MultiTapeTM k Symbol State) : MultiTapeMachine k Symbol State Empty Id

Embed a deterministic upstream machine in the common table using Id for its choices.

def Turing.MultiTapeNTM.toMachine {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (machine : MultiTapeNTM k Symbol State) : MultiTapeMachine k Symbol State Empty Set

Embed an upstream nondeterministic machine using precisely its permitted actions.

theorem Turing.MultiTapeTM.toMachine_toTM_tr {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (machine : MultiTapeTM k Symbol State) (state : State) (symbol : Option Symbol) (work : Fin k → Option Symbol) : machine.toMachine.toTM.tr state symbol work = machine.tr state symbol work

A deterministic embedding retains the original transition function.

theorem Turing.MultiTapeTM.toMachine_toTM {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (machine : MultiTapeTM k Symbol State) : machine.toMachine.toTM = machine

A deterministic embedding retains the original machine, including its transition relation.

theorem Turing.MultiTapeNTM.toMachine_toNTM {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (machine : MultiTapeNTM k Symbol State) : machine.toMachine.toNTM = machine

A nondeterministic embedding retains the original relation, including empty choices.

theorem Turing.MultiTapeMachine.toTM_toMachine {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (machine : MultiTapeMachine k Symbol State Empty Id) : machine.toTM.toMachine = machine

Converting a deterministic table to upstream and back retains the complete table.

theorem Turing.MultiTapeMachine.toNTM_toMachine {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (machine : MultiTapeMachine k Symbol State Empty Set) : machine.toNTM.toMachine = machine

Converting a nondeterministic table to upstream and back retains every permitted action.

noncomputable def Turing.MultiTapeMachine.tmEquiv {k : ℕ} {Symbol : Type u_1} {State : Type u_2} : MultiTapeMachine k Symbol State Empty Id ≃ MultiTapeTM k Symbol State

The effect-free deterministic machine is precisely upstream's machine type.

def Turing.MultiTapeMachine.ntmEquiv {k : ℕ} {Symbol : Type u_1} {State : Type u_2} : MultiTapeMachine k Symbol State Empty Set ≃ MultiTapeNTM k Symbol State

The effect-free nondeterministic machine is precisely upstream's machine type.