Compilation of Search Procedures to TM0

This file proves the key compilation theorem: if a language can be expressed as { w | ∃ a : α, test a w = true } for a Primcodable witness type α and a Computable₂ test function, then the language is TM-recognizable by a TM0 machine.

Main results

• search_is_partrec — the µ-search is Partrec
• code_to_tm0 — Code → TM0 evaluation
• search_halts_tm0 — the search is TM0-recognizable (with an internal Fintype tape alphabet)
• is_TM_of_searchable — searchable languages are internally TM-recognizable

Architecture note

This file compiles computable witness search to the internal Partrec-chain TM0 alphabet. The final alphabet/encoding bridge to is_TM is supplied by CodeToTMDirect.lean.

Fintype instances for Partrec types

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

Equations

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

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

Equations

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

Search Step Function

def searchStep {T α : Type} [Encodable α] (test : α → List T → Bool) (w : List T) (n : ℕ) : Bool

The "step" function of the search: enumerate the n-th witness and test it.

Equations

• searchStep test w n = match Encodable.decode n with | some a => test a w | none => false

theorem searchStep_iff {T α : Type} [Encodable α] (test : α → List T → Bool) (w : List T) : (∃ (n : ℕ), searchStep test w n = true) ↔ ∃ (a : α), test a w = true

The search succeeds iff there exists a witness.

Sub-problem 1: Computable₂ test → Code (PROVED)

theorem search_is_partrec {T α : Type} [Primcodable T] [Primcodable α] (test : α → List T → Bool) (hc : Computable₂ test) : ∃ (c : Turing.ToPartrec.Code), ∀ (w : List T), (∃ (a : α), test a w = true) ↔ (c.eval [Encodable.encode w]).Dom

Sub-problem 1 (PROVED): The µ-search over a computable test is Partrec.

Sub-problem 2: Code → TM0 (PROVED)

theorem code_to_tm0 (c : Turing.ToPartrec.Code) : ∃ (Γ : Type) (Λ : Type) (x : Inhabited Λ) (x_1 : Inhabited Γ) (x_2 : Fintype Γ) (encode_input : ℕ → List Γ) (M : Turing.TM0.Machine Γ Λ), ∀ (n : ℕ), (c.eval [n]).Dom ↔ (Turing.TM0.eval M (encode_input n)).Dom

Sub-problem 2 (PROVED): Partrec Code → TM0 evaluation.

Core Compilation Theorem (PROVED)

theorem search_halts_tm0 {T : Type} [Primcodable T] {α : Type} [Primcodable α] (test : α → List T → Bool) (hc : Computable₂ test) : ∃ (Γ : Type) (x : Inhabited Γ) (x_1 : Fintype Γ) (Λ : Type) (x_2 : Inhabited Λ) (M : Turing.TM0.Machine Γ Λ) (enc : List T → List Γ), ∀ (w : List T), (∃ (a : α), test a w = true) ↔ (Turing.TM0.eval M (enc w)).Dom

The core compilation theorem.

The enumerate-and-test search pattern is implementable by a TM0 machine over the Partrec chain's internal Fintype alphabet ChainΓ. The TM0 halts on enc w if and only if there exists a witness a such that test a w = true.

This theorem captures the full mathematical content: computable search procedures yield TM-recognizable languages. The tape alphabet is the chain's internal alphabet rather than Option T; converting to Option T requires alphabet simulation (see tm0_alphabet_simulation below).

Main Compilation Theorem

theorem is_TM_of_searchable {T : Type} [Primcodable T] {α : Type} [Primcodable α] (test : α → List T → Bool) (hc : Computable₂ test) (L : Language T) (hL : L = {w : List T | ∃ (a : α), test a w = true}) : ∃ (Γ : Type) (x : Inhabited Γ) (x_1 : Fintype Γ) (Λ : Type) (x_2 : Inhabited Λ) (M : Turing.TM0.Machine Γ Λ) (enc : List T → List Γ), ∀ (w : List T), w ∈ L ↔ (Turing.TM0.eval M (enc w)).Dom

Main Compilation Theorem: If we can search over a Primcodable domain with a Computable₂ test, the resulting language is TM-recognizable (with an internal Fintype tape alphabet).

This is the is_TM-style result (without Fintype on states). For the full is_TM result (with Option T tape alphabet), see

Strengthened versions with Fintype states

theorem code_to_tm0_with_fintype (c : Turing.ToPartrec.Code) : ∃ (Γ : Type) (Λ : Type) (x : Inhabited Λ) (x_1 : Inhabited Γ) (x_2 : Fintype Γ) (x_3 : Fintype Λ) (encode_input : ℕ → List Γ) (M : Turing.TM0.Machine Γ Λ), ∀ (n : ℕ), (c.eval [n]).Dom ↔ (Turing.TM0.eval M (encode_input n)).Dom

Strengthened code_to_tm0 with Fintype states.

theorem search_halts_tm0_fintype {T : Type} [Primcodable T] {α : Type} [Primcodable α] (test : α → List T → Bool) (hc : Computable₂ test) : ∃ (Γ : Type) (x : Inhabited Γ) (x_1 : Fintype Γ) (Λ : Type) (x_2 : Inhabited Λ) (x_3 : Fintype Λ) (M : Turing.TM0.Machine Γ Λ) (enc : List T → List Γ), ∀ (w : List T), (∃ (a : α), test a w = true) ↔ (Turing.TM0.eval M (enc w)).Dom

Strengthened search_halts_tm0 with Fintype states.

theorem is_TM_of_searchable_fintype {T : Type} [Primcodable T] {α : Type} [Primcodable α] (test : α → List T → Bool) (hc : Computable₂ test) (L : Language T) (hL : L = {w : List T | ∃ (a : α), test a w = true}) : ∃ (Γ : Type) (x : Inhabited Γ) (x_1 : Fintype Γ) (Λ : Type) (x_2 : Inhabited Λ) (x_3 : Fintype Λ) (M : Turing.TM0.Machine Γ Λ) (enc : List T → List Γ), ∀ (w : List T), w ∈ L ↔ (Turing.TM0.eval M (enc w)).Dom

Strengthened is_TM_of_searchable with Fintype states.