TM0 Restriction to Finite Support

Given a TM0 machine supported by a finite set of states, we construct an equivalent TM0 machine whose state type is a subtype, hence Fintype.

Main results

• Turing.TM0.restrict — restrict a TM0 machine to a finite support set
• Turing.TM0.restrict_eval_dom_iff — the restricted machine halts iff the original does

noncomputable def Turing.TM0.restrict {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] (M : Machine Γ Λ) (S : Finset Λ) (hS : Supports M ↑S) : Machine Γ { q : Λ // q ∈ S }

Restrict a TM0 machine to states in a finite support set S. Since the machine is supported by S, all transitions stay within S, so the restriction doesn't change behavior.

Equations

• Turing.TM0.restrict M S hS ⟨q, hq⟩ a = match hm : M q a with | some (q', s) => have hq' := ⋯; some (⟨q', hq'⟩, s) | none => none

def Turing.TM0.restrictRel {Γ : Type u_1} {Λ : Type u_2} [Inhabited Γ] (S : Finset Λ) : Cfg Γ { q : Λ // q ∈ S } → Cfg Γ Λ → Prop

The bisimulation relation: configs are related when the restricted config's state projects to the original config's state, and tapes are equal.

Equations

• Turing.TM0.restrictRel S c₂ c₁ = (c₁.q = ↑c₂.q ∧ c₁.Tape = c₂.Tape)

theorem Turing.TM0.restrict_respects {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] [Inhabited Γ] (M : Machine Γ Λ) (S : Finset Λ) (hS : Supports M ↑S) : Respects (step M) (step (restrict M S hS)) fun (c₁ : Cfg Γ Λ) (c₂ : Cfg Γ { q : Λ // q ∈ S }) => restrictRel S c₂ c₁

theorem Turing.TM0.restrict_init_rel {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] [Inhabited Γ] (M : Machine Γ Λ) (S : Finset Λ) (hS : Supports M ↑S) (l : List Γ) : restrictRel S (init l) (init l)

theorem Turing.TM0.restrict_eval_dom_iff {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] [Inhabited Γ] (M : Machine Γ Λ) (S : Finset Λ) (hS : Supports M ↑S) (l : List Γ) : (eval M l).Dom ↔ (eval (restrict M S hS) l).Dom

The restricted TM0 halts if and only if the original does.

Uses Turing.tr_eval_dom with the bisimulation relation restrictRel.