Partrec Code → TM0 Assembly

This file assembles the full chain Code → TM2 → TM1 → TM0, proving that any partial recursive function (given as ToPartrec.Code) can be evaluated by a TM0 machine.

Main results

• partrec_init_trCfg — TrCfg for PartrecToTM2.init (the key lemma)
• code_to_tm0_halts — full chain: Code halts iff TM0 halts
• code_to_tm0 — existential form, without finite state restriction
• code_to_tm0_fintype / code_to_tm0_fintype_general — finite-state TM0 realizations for unary and list inputs

Stack Equality

theorem partrec_init_stk_eq (c : Turing.ToPartrec.Code) (v : List ℕ) : (Turing.PartrecToTM2.init c v).stk = (Turing.TM2.init Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.trList v)).stk

The stacks of PartrecToTM2.init c v equal those of TM2.init K'.main (trList v).

TrCfg for PartrecToTM2.init

theorem partrec_init_trCfg (c : Turing.ToPartrec.Code) (v : List ℕ) : Turing.TM2to1.TrCfg (Turing.PartrecToTM2.init c v) { l := Option.map Turing.TM2to1.Λ'.normal (Turing.PartrecToTM2.init c v).l, var := (Turing.PartrecToTM2.init c v).var, Tape := (Turing.TM1.init (Turing.TM2to1.trInit Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.trList v))).Tape }

Chain Type Abbreviations

@[reducible, inline]

abbrev ChainΓ : Type

Equations

• ChainΓ = Turing.TM2to1.Γ' Turing.PartrecToTM2.K' fun (x : Turing.PartrecToTM2.K') => Turing.PartrecToTM2.Γ'

@[reducible, inline]

abbrev ChainΛ_TM1 : Type

Equations

• ChainΛ_TM1 = Turing.TM2to1.Λ' Turing.PartrecToTM2.K' (fun (x : Turing.PartrecToTM2.K') => Turing.PartrecToTM2.Γ') Turing.PartrecToTM2.Λ' (Option Turing.PartrecToTM2.Γ')

@[reducible, inline]

abbrev ChainTM1 : Turing.TM2to1.Λ' Turing.PartrecToTM2.K' (fun (x : Turing.PartrecToTM2.K') => Turing.PartrecToTM2.Γ') Turing.PartrecToTM2.Λ' (Option Turing.PartrecToTM2.Γ') → Turing.TM1.Stmt (Turing.TM2to1.Γ' Turing.PartrecToTM2.K' fun (x : Turing.PartrecToTM2.K') => Turing.PartrecToTM2.Γ') (Turing.TM2to1.Λ' Turing.PartrecToTM2.K' (fun (x : Turing.PartrecToTM2.K') => Turing.PartrecToTM2.Γ') Turing.PartrecToTM2.Λ' (Option Turing.PartrecToTM2.Γ')) (Option Turing.PartrecToTM2.Γ')

Equations

• ChainTM1 = Turing.TM2to1.tr Turing.PartrecToTM2.tr

@[reducible, inline]

abbrev ChainTM0 : Turing.TM0.Machine (Turing.TM2to1.Γ' Turing.PartrecToTM2.K' fun (x : Turing.PartrecToTM2.K') => Turing.PartrecToTM2.Γ') (Turing.TM1to0.Λ' ChainTM1)

Equations

• ChainTM0 = Turing.TM1to0.tr ChainTM1

@[reducible, inline]

abbrev ChainΛ_TM0 : Type

Equations

• ChainΛ_TM0 = Turing.TM1to0.Λ' ChainTM1

instance instFintypeK'_langlib : Fintype Turing.PartrecToTM2.K'

Equations

• instFintypeK'_langlib = Fintype.ofList [Turing.PartrecToTM2.K'.main, Turing.PartrecToTM2.K'.rev, Turing.PartrecToTM2.K'.aux, Turing.PartrecToTM2.K'.stack] instFintypeK'_langlib._proof_1

instance instFintypeΓ'_langlib : Fintype Turing.PartrecToTM2.Γ'

Equations

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

theorem code_eval_iff_tm2 (c : Turing.ToPartrec.Code) (v : List ℕ) : (c.eval v).Dom ↔ (Turing.eval (Turing.TM2.step Turing.PartrecToTM2.tr) (Turing.PartrecToTM2.init c v)).Dom

TM2 halts iff Code evaluates.

Full Chain: Code → TM0

theorem code_to_tm0_halts (c : Turing.ToPartrec.Code) (v : List ℕ) : have cfg₁ := { l := Option.map Turing.TM2to1.Λ'.normal (Turing.PartrecToTM2.init c v).l, var := (Turing.PartrecToTM2.init c v).var, Tape := (Turing.TM1.init (Turing.TM2to1.trInit Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.trList v))).Tape }; have cfg₀ := Turing.TM1to0.trCfg ChainTM1 cfg₁; have q₀ := cfg₀.q; have input := Turing.TM2to1.trInit Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.trList v); (c.eval v).Dom ↔ (Turing.TM0.eval (ParrecToTM0.tm0Reroot ChainTM0 q₀) input).Dom

Full chain: Code → TM0 (eval form).

Support Chain (for Fintype states)

def chainSuppTM2 (c : Turing.ToPartrec.Code) : Finset Turing.PartrecToTM2.Λ'

The TM2 support set for a given code c.

Equations

• chainSuppTM2 c = Turing.PartrecToTM2.codeSupp c Turing.PartrecToTM2.Cont'.halt

noncomputable def chainSuppTM1 (c : Turing.ToPartrec.Code) : Finset ChainΛ_TM1

The TM1 support set.

Equations

• chainSuppTM1 c = Turing.TM2to1.trSupp Turing.PartrecToTM2.tr (chainSuppTM2 c)

noncomputable def chainSuppTM0 (c : Turing.ToPartrec.Code) : Finset ChainΛ_TM0

The TM0 support set.

Equations

• chainSuppTM0 c = Turing.TM1to0.trStmts ChainTM1 (chainSuppTM1 c)

Full Chain with Fintype States

@[reducible, inline]

abbrev chainTM1Cfg (c : Turing.ToPartrec.Code) (v : List ℕ) : Turing.TM1.Cfg ChainΓ ChainΛ_TM1 (Option Turing.PartrecToTM2.Γ')

The initial TM1 config for the chain.

Equations

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

theorem chainTM0_trCfg_eq_nc (c : Turing.ToPartrec.Code) (n : ℕ) : Turing.TM1to0.trCfg (Turing.TM2to1.tr Turing.PartrecToTM2.tr) (chainTM1Cfg c [n]) = { q := default, Tape := Turing.Tape.mk₁ (Turing.TM2to1.trInit Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.trList [n])) }

theorem chainTM0_trCfg_eq_general (c : Turing.ToPartrec.Code) (v : List ℕ) : Turing.TM1to0.trCfg (Turing.TM2to1.tr Turing.PartrecToTM2.tr) (chainTM1Cfg c v) = { q := default, Tape := Turing.Tape.mk₁ (Turing.TM2to1.trInit Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.trList v)) }

Generalized version of chainTM0_trCfg_eq_nc for arbitrary v : List ℕ. Works because the TM0 state depends only on the Code c (via the non-canonical Inhabited instance), not on the input list. The var component of init c v is always none : Option Γ'.

theorem code_to_tm0_fintype (c : Turing.ToPartrec.Code) : ∃ (ΛTy : Type) (x : Inhabited ΛTy) (x_1 : Fintype ΛTy) (M : Turing.TM0.Machine ChainΓ ΛTy), ∀ (n : ℕ), (c.eval [n]).Dom ↔ (Turing.TM0.eval M (Turing.TM2to1.trInit Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.trList [n]))).Dom

Full chain: Code → TM0 with Fintype states.

This is the strengthened version of code_to_tm0 that provides Fintype Λ. The key insight is to override the Inhabited PartrecToTM2.Λ' instance to ⟨trNormal c halt⟩ (matching tr_supports), then thread the non-canonical @[expose] public instance through the entire chain. The resulting TM0 machine is definitionally the same as ChainTM0 (since TM1to0.tr ignores Inhabited), but the support proof uses the non-canonical default.

theorem code_to_tm0_fintype_general (c : Turing.ToPartrec.Code) : ∃ (ΛTy : Type) (x : Inhabited ΛTy) (x_1 : Fintype ΛTy) (M : Turing.TM0.Machine ChainΓ ΛTy), ∀ (v : List ℕ), (c.eval v).Dom ↔ (Turing.TM0.eval M (Turing.TM2to1.trInit Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.trList v))).Dom

Generalized chain: Code → TM0 with Fintype states and multi-element input.

Same as code_to_tm0_fintype but works for arbitrary v : List ℕ instead of just [n]. The machine and state space are identical — only the input encoding trInit K'.main (trList v) varies with the input list.