TM0 Re-rooting and Chain Infrastructure

This file provides infrastructure for the Partrec → TM0 compilation chain.

Main results

TM0 Re-rooting

• ParrecToTM0.Rooted — wrapper type with custom default
• ParrecToTM0.tm0Reroot — re-root a TM0 to start from an arbitrary state
• ParrecToTM0.tm0Reroot_eval_dom — re-rooting preserves halting (Dom)

Chain Dom Preservation

• ParrecToTM0.tm2to1_dom_general — TM2 → TM1 preserves Dom for arbitrary initial configs
• ParrecToTM0.tm1to0_dom_general — TM1 → TM0 preserves Dom for arbitrary initial configs

TM0 Re-rooting

structure ParrecToTM0.Rooted (Λ : Type u_1) (q₀ : Λ) : Type u_1

Wrapper type that allows re-rooting to a specified initial state.

• val : Λ

theorem ParrecToTM0.Rooted.ext_iff {Λ : Type u_1} {q₀ : Λ} {x y : Rooted Λ q₀} : x = y ↔ x.val = y.val

theorem ParrecToTM0.Rooted.ext {Λ : Type u_1} {q₀ : Λ} {x y : Rooted Λ q₀} (val : x.val = y.val) : x = y

instance ParrecToTM0.instInhabitedRooted {Λ : Type u_1} {q₀ : Λ} : Inhabited (Rooted Λ q₀)

Equations

• ParrecToTM0.instInhabitedRooted = { default := { val := q₀ } }

def ParrecToTM0.tm0Reroot {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (q₀ : Λ) : Turing.TM0.Machine Γ (Rooted Λ q₀)

Re-root a TM0 machine to start from state q₀ instead of default.

Equations

• ParrecToTM0.tm0Reroot M q₀ { val := q } a = Option.map (fun (x : Λ × Turing.TM0.Stmt Γ) => match x with | (q', s) => ({ val := q' }, s)) (M q a)

theorem ParrecToTM0.tm0Reroot_respects {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] [Inhabited Γ] (M : Turing.TM0.Machine Γ Λ) (q₀ : Λ) : Turing.Respects (Turing.TM0.step M) (Turing.TM0.step (tm0Reroot M q₀)) fun (c₁ : Turing.TM0.Cfg Γ Λ) (c₂ : Turing.TM0.Cfg Γ (Rooted Λ q₀)) => c₁.q = c₂.q.val ∧ c₁.Tape = c₂.Tape

theorem ParrecToTM0.tm0Reroot_eval_dom {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] [Inhabited Γ] (M : Turing.TM0.Machine Γ Λ) (q₀ : Λ) (l : List Γ) : (Turing.eval (Turing.TM0.step M) { q := q₀, Tape := Turing.Tape.mk₁ l }).Dom ↔ (Turing.TM0.eval (tm0Reroot M q₀) l).Dom

Evaluation of the re-rooted TM0 starting from q₀ preserves halting.

Chain Dom Preservation for Arbitrary Initial Configs

theorem ParrecToTM0.tm2to1_dom_general {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ) (cfg₂ : Turing.TM2.Cfg Γ Λ σ) (cfg₁ : Turing.TM1.Cfg (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ) (hrel : Turing.TM2to1.TrCfg cfg₂ cfg₁) : (Turing.eval (Turing.TM1.step (Turing.TM2to1.tr M)) cfg₁).Dom ↔ (Turing.eval (Turing.TM2.step M) cfg₂).Dom

TM2 → TM1 preserves Dom for arbitrary initial configs related by TrCfg.

theorem ParrecToTM0.tm1to0_dom_general {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] {σ : Type u_3} [Inhabited σ] [Inhabited Γ] (M : Λ → Turing.TM1.Stmt Γ Λ σ) (cfg₁ : Turing.TM1.Cfg Γ Λ σ) : (Turing.eval (Turing.TM0.step (Turing.TM1to0.tr M)) (Turing.TM1to0.trCfg M cfg₁)).Dom ↔ (Turing.eval (Turing.TM1.step M) cfg₁).Dom

TM1 → TM0 preserves Dom for arbitrary initial configs.

Fintype States

theorem ParrecToTM0.tm1to0_fintype_states {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] {σ : Type u_3} [Inhabited σ] [Fintype σ] (M : Λ → Turing.TM1.Stmt Γ Λ σ) {S : Finset Λ} (hS : Turing.TM1.Supports M S) : Turing.TM0.Supports (Turing.TM1to0.tr M) ↑(Turing.TM1to0.trStmts M S)

The TM1 → TM0 translation preserves support (re-exported for convenience).

Re-rooting Support

def ParrecToTM0.rootedEmbFn {Λ : Type u_1} {q₀ : Λ} : Λ ↪ Rooted Λ q₀

Embedding function for Rooted: wraps a value into a Rooted.

Equations

• ParrecToTM0.rootedEmbFn = { toFun := fun (q : Λ) => { val := q }, inj' := ⋯ }

theorem ParrecToTM0.tm0Reroot_supports {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] [Inhabited Γ] (M : Turing.TM0.Machine Γ Λ) (S : Finset Λ) (hS : Turing.TM0.Supports M ↑S) (q₀ : Λ) (hq₀ : q₀ ∈ S) : Turing.TM0.Supports (tm0Reroot M q₀) ↑(Finset.map rootedEmbFn S)

If TM0.Supports M S and q₀ ∈ S, then tm0Reroot M q₀ is supported by the image of S under the Rooted embedding.

noncomputable def ParrecToTM0.tm0RestrictReroot {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] [Inhabited Γ] (M : Turing.TM0.Machine Γ Λ) (S : Finset Λ) (hS : Turing.TM0.Supports M ↑S) (q₀ : Λ) (hq₀ : q₀ ∈ S) : let S' := Finset.map rootedEmbFn S; have _hS' := ⋯; Turing.TM0.Machine Γ { q : Rooted Λ q₀ // q ∈ S' }

Restrict + reroot a TM0: combine re-rooting and restriction into one step. Given TM0.Supports M S with q₀ ∈ S, produce a TM0 with Fintype states that halts on l iff the original does when started from q₀.

Equations

• ParrecToTM0.tm0RestrictReroot M S hS q₀ hq₀ = Turing.TM0.restrict (ParrecToTM0.tm0Reroot M q₀) (Finset.map ParrecToTM0.rootedEmbFn S) ⋯

noncomputable def ParrecToTM0.tm0RestrictReroot_fintype {Λ : Type u_1} (S : Finset Λ) (q₀ : Λ) : Fintype { q : Rooted Λ q₀ // q ∈ Finset.map rootedEmbFn S }

Equations

• ParrecToTM0.tm0RestrictReroot_fintype S q₀ = Finset.Subtype.fintype (Finset.map ParrecToTM0.rootedEmbFn S)

theorem ParrecToTM0.tm0RestrictReroot_eval_dom {Γ : Type u_1} {Λ : Type u_2} [Inhabited Λ] [Inhabited Γ] (M : Turing.TM0.Machine Γ Λ) (S : Finset Λ) (hS : Turing.TM0.Supports M ↑S) (q₀ : Λ) (hq₀ : q₀ ∈ S) (l : List Γ) : (Turing.eval (Turing.TM0.step M) { q := q₀, Tape := Turing.Tape.mk₁ l }).Dom ↔ (Turing.TM0.eval (tm0RestrictReroot M S hS q₀ hq₀) l).Dom

The restrict+reroot machine halts iff the original does when started from q₀.