SupportedTM1Thue

Part of the dependency closure of the small undecidable group constructions.

@[reducible, inline]

noncomputable abbrev Undecidability.SupportedTM1Thue.State {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] [Fintype Γ] [Fintype σ] (B : TM1BinaryAdapter.Code Γ) (M : Λ → Turing.TM1.Stmt Γ Λ σ) (S : Finset Λ) : Finset (Turing.TM1to0.Λ' (TM1BinaryAdapter.program B M))

The finite supported state type used in the one-tape-to-Thue reduction.

Equations

• Undecidability.SupportedTM1Thue.State B M S = Undecidability.TM1BinaryAdapter.support B M S

@[reducible, inline]

noncomputable abbrev Undecidability.SupportedTM1Thue.Alphabet {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] [Fintype Γ] [Fintype σ] (B : TM1BinaryAdapter.Code Γ) (M : Λ → Turing.TM1.Stmt Γ Λ σ) (S : Finset Λ) : Type (max (max u_1 u_2) u_3)

The alphabet of the Thue system simulating the supported one-tape machine.

Equations

• Undecidability.SupportedTM1Thue.Alphabet B M S = Undecidability.PostMachine.Symbol (Undecidability.TM0PostAdapter.Phase ↥(Undecidability.SupportedTM1Thue.State B M S))

noncomputable def Undecidability.SupportedTM1Thue.postMachine {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited σ] [Fintype Γ] [Fintype σ] (B : TM1BinaryAdapter.Code Γ) (M : Λ → Turing.TM1.Stmt Γ Λ σ) (S : Finset Λ) (hS : Turing.TM1.Supports M S) : PostMachine.Machine (TM0PostAdapter.Phase ↥(State B M S))

The combined write-and-move machine obtained from a supported source TM1, after binary compilation and restriction to finite state.

Equations

• Undecidability.SupportedTM1Thue.postMachine B M S hS = Undecidability.TM0PostAdapter.machine (Undecidability.TM1BinaryAdapter.finiteMachine B M S hS)

noncomputable def Undecidability.SupportedTM1Thue.start {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited σ] [Fintype Γ] [Fintype σ] (B : TM1BinaryAdapter.Code Γ) (M : Λ → Turing.TM1.Stmt Γ Λ σ) (S : Finset Λ) (hS : Turing.TM1.Supports M S) (input : List Γ) : List (Alphabet B M S)

The Thue word encoding the initial configuration on a source input.

Equations

• Undecidability.SupportedTM1Thue.start B M S hS input = Undecidability.PostMachine.encode (Undecidability.TM0PostAdapter.init (Undecidability.TM1BinaryAdapter.encodeInput B input))

def Undecidability.SupportedTM1Thue.binaryStart {Q : Type u_4} [Inhabited Q] (input : List Bool) : List (PostMachine.Symbol (TM0PostAdapter.Phase Q))

The binary initial configuration of the one-tape simulation.

Equations

• Undecidability.SupportedTM1Thue.binaryStart input = Undecidability.PostMachine.encode (Undecidability.TM0PostAdapter.init input)

theorem Undecidability.SupportedTM1Thue.start_computable {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited σ] [Fintype Γ] [Fintype σ] (B : TM1BinaryAdapter.Code Γ) (M : Λ → Turing.TM1.Stmt Γ Λ σ) (S : Finset Λ) (hS : Turing.TM1.Supports M S) [Primcodable Γ] [Primcodable (Alphabet B M S)] : Computable (start B M S hS)

The reduction from source input words to initial Thue words is computable.

theorem Undecidability.SupportedTM1Thue.thue_iff_eval_dom {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited σ] [Fintype Γ] [Fintype σ] (B : TM1BinaryAdapter.Code Γ) (M : Λ → Turing.TM1.Stmt Γ Λ σ) (S : Finset Λ) (hS : Turing.TM1.Supports M S) (input : List Γ) : ThueEq (PostMachine.system (postMachine B M S hS)) (start B M S hS input) PostMachine.target ↔ (Turing.TM1.eval M input).Dom

The resulting finite fixed-target Thue system recognizes precisely the halting inputs of the supported source program.

theorem Undecidability.SupportedTM1Thue.system_finite {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited σ] [Fintype Γ] [Fintype σ] (B : TM1BinaryAdapter.Code Γ) (M : Λ → Turing.TM1.Stmt Γ Λ σ) (S : Finset Λ) (hS : Turing.TM1.Supports M S) : Set.Finite (PostMachine.system (postMachine B M S hS))

The Thue presentation used above has finitely many rules.