Alphabet Simulation for TM0

This file proves that a TM0 machine over a finite alphabet Γ₁ can be simulated by a TM0 machine over another finite alphabet Γ₂, provided there exists an injection from Γ₁ to Γ₂ that maps default to default.

Main results

• TM0AlphabetSim.lift_eval_dom — evaluation preserves Dom under alphabet embedding

noncomputable def TM0AlphabetSim.liftMachine {Γ₁ Γ₂ Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine Γ₁ Λ) (emb : Γ₁ → Γ₂) (inv : Γ₂ → Γ₁) : Turing.TM0.Machine Γ₂ Λ

Lift a TM0 machine from alphabet Γ₁ to Γ₂ via an embedding/inverse pair. The inverse maps Γ₂ symbols back to Γ₁ (left inverse of emb).

Equations

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

noncomputable def TM0AlphabetSim.embPM {Γ₁ Γ₂ : Type} [Inhabited Γ₁] [Inhabited Γ₂] (emb : Γ₁ → Γ₂) (hemb_default : emb default = default) : Turing.PointedMap Γ₁ Γ₂

The PointedMap from the embedding function.

Equations

• TM0AlphabetSim.embPM emb hemb_default = { f := emb, map_pt' := hemb_default }

def TM0AlphabetSim.liftRel {Γ₁ Γ₂ : Type} [Inhabited Γ₁] [Inhabited Γ₂] {Λ : Type} (emb : Γ₁ → Γ₂) (inv : Γ₂ → Γ₁) (_hemb : ∀ (a : Γ₁), inv (emb a) = a) (hemb_default : emb default = default) : Turing.TM0.Cfg Γ₁ Λ → Turing.TM0.Cfg Γ₂ Λ → Prop

The relation between Γ₁ configs and Γ₂ configs under the alphabet lift.

Equations

• TM0AlphabetSim.liftRel emb inv _hemb hemb_default c₁ c₂ = (c₁.q = c₂.q ∧ c₂.Tape = Turing.Tape.map (TM0AlphabetSim.embPM emb hemb_default) c₁.Tape)

theorem TM0AlphabetSim.lift_respects {Γ₁ Γ₂ : Type} [Inhabited Γ₁] [Inhabited Γ₂] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine Γ₁ Λ) (emb : Γ₁ → Γ₂) (inv : Γ₂ → Γ₁) (hemb : ∀ (a : Γ₁), inv (emb a) = a) (hemb_default : emb default = default) : Turing.Respects (Turing.TM0.step M) (Turing.TM0.step (liftMachine M emb inv)) (liftRel emb inv hemb hemb_default)

theorem TM0AlphabetSim.lift_init_rel {Γ₁ Γ₂ : Type} [Inhabited Γ₁] [Inhabited Γ₂] {Λ : Type} [Inhabited Λ] (emb : Γ₁ → Γ₂) (inv : Γ₂ → Γ₁) (hemb : ∀ (a : Γ₁), inv (emb a) = a) (hemb_default : emb default = default) (l : List Γ₁) : liftRel emb inv hemb hemb_default (Turing.TM0.init l) (Turing.TM0.init (List.map emb l))

theorem TM0AlphabetSim.lift_eval_dom {Γ₁ Γ₂ : Type} [Inhabited Γ₁] [Inhabited Γ₂] {Λ : Type} [Inhabited Λ] (M : Turing.TM0.Machine Γ₁ Λ) (emb : Γ₁ → Γ₂) (inv : Γ₂ → Γ₁) (hemb : ∀ (a : Γ₁), inv (emb a) = a) (hemb_default : emb default = default) (l : List Γ₁) : (Turing.TM0.eval M l).Dom ↔ (Turing.TM0.eval (liftMachine M emb inv) (List.map emb l)).Dom

Evaluation preserves Dom under alphabet lift.

Inverse-default-fiber-preserving lift

noncomputable def TM0AlphabetSim.invPM {Γ₁ Γ₂ : Type} [Inhabited Γ₁] [Inhabited Γ₂] (inv : Γ₂ → Γ₁) (hinv_default : inv default = default) : Turing.PointedMap Γ₂ Γ₁

The PointedMap from an inverse function.

Equations

• TM0AlphabetSim.invPM inv hinv_default = { f := inv, map_pt' := hinv_default }

noncomputable def TM0AlphabetSim.liftWritePreserveDefaultFiber {Γ₁ Γ₂ : Type} [Inhabited Γ₁] (emb : Γ₁ → Γ₂) (inv : Γ₂ → Γ₁) [DecidableEq Γ₁] (current : Γ₂) (a : Γ₁) : Γ₂

Write translation for the inverse-relation lift.

When the source writes default, target symbols that already map to default are preserved. This lets the target alphabet carry protected symbols that the source machine observes as blanks.

Equations

• TM0AlphabetSim.liftWritePreserveDefaultFiber emb inv current a = if a = default then if inv current = default then current else emb default else emb a

noncomputable def TM0AlphabetSim.liftMachinePreserveDefaultFiber {Γ₁ Γ₂ : Type} [Inhabited Γ₁] {Λ : Type} [Inhabited Λ] [DecidableEq Γ₁] (M : Turing.TM0.Machine Γ₁ Λ) (emb : Γ₁ → Γ₂) (inv : Γ₂ → Γ₁) : Turing.TM0.Machine Γ₂ Λ

Lift a TM0 machine while preserving target symbols in the inverse-default fiber whenever the source writes default.

Equations

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

def TM0AlphabetSim.liftInvRel {Γ₁ Γ₂ : Type} [Inhabited Γ₁] [Inhabited Γ₂] {Λ : Type} (inv : Γ₂ → Γ₁) (hinv_default : inv default = default) : Turing.TM0.Cfg Γ₁ Λ → Turing.TM0.Cfg Γ₂ Λ → Prop

Inverse-form relation between source and target configurations.

The target tape may contain symbols outside the embedding image; the source tape only has to be recovered by mapping target symbols through inv.

Equations

• TM0AlphabetSim.liftInvRel inv hinv_default c₁ c₂ = (c₁.q = c₂.q ∧ c₁.Tape = Turing.Tape.map (TM0AlphabetSim.invPM inv hinv_default) c₂.Tape)

theorem TM0AlphabetSim.inv_liftWritePreserveDefaultFiber {Γ₁ Γ₂ : Type} [Inhabited Γ₁] [DecidableEq Γ₁] (emb : Γ₁ → Γ₂) (inv : Γ₂ → Γ₁) (hemb : ∀ (a : Γ₁), inv (emb a) = a) (current : Γ₂) (a : Γ₁) : inv (liftWritePreserveDefaultFiber emb inv current a) = a

theorem TM0AlphabetSim.lift_preserveDefaultFiber_respects {Γ₁ Γ₂ : Type} [Inhabited Γ₁] [Inhabited Γ₂] {Λ : Type} [Inhabited Λ] [DecidableEq Γ₁] (M : Turing.TM0.Machine Γ₁ Λ) (emb : Γ₁ → Γ₂) (inv : Γ₂ → Γ₁) (hemb : ∀ (a : Γ₁), inv (emb a) = a) (hinv_default : inv default = default) : Turing.Respects (Turing.TM0.step M) (Turing.TM0.step (liftMachinePreserveDefaultFiber M emb inv)) (liftInvRel inv hinv_default)

theorem TM0AlphabetSim.liftInv_init_rel {Γ₁ Γ₂ : Type} [Inhabited Γ₁] [Inhabited Γ₂] {Λ : Type} [Inhabited Λ] (inv : Γ₂ → Γ₁) (hinv_default : inv default = default) (l : List Γ₂) : liftInvRel inv hinv_default (Turing.TM0.init (List.map inv l)) (Turing.TM0.init l)

theorem TM0AlphabetSim.lift_preserveDefaultFiber_eval_dom {Γ₁ Γ₂ : Type} [Inhabited Γ₁] [Inhabited Γ₂] {Λ : Type} [Inhabited Λ] [DecidableEq Γ₁] (M : Turing.TM0.Machine Γ₁ Λ) (emb : Γ₁ → Γ₂) (inv : Γ₂ → Γ₁) (hemb : ∀ (a : Γ₁), inv (emb a) = a) (hinv_default : inv default = default) (l : List Γ₂) : (Turing.TM0.eval M (List.map inv l)).Dom ↔ (Turing.TM0.eval (liftMachinePreserveDefaultFiber M emb inv) l).Dom

Evaluation preserves Dom for the inverse-default-fiber-preserving lift.