TM1BinaryAdapter

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

@[reducible]

def Undecidability.TM0FiniteRestriction.supportedInhabited {Gamma : Type u_1} {Q : Type u_2} [Inhabited Q] (M : Turing.TM0.Machine Gamma Q) (S : Finset Q) (hS : Turing.TM0.Supports M ↑S) : Inhabited ↥S

The initial state belongs to every certified support.

Equations

• Undecidability.TM0FiniteRestriction.supportedInhabited M S hS = { default := ⟨default, ⋯⟩ }

noncomputable def Undecidability.TM0FiniteRestriction.liftState {Gamma : Type u_1} {Q : Type u_2} [Inhabited Q] (M : Turing.TM0.Machine Gamma Q) (S : Finset Q) (hS : Turing.TM0.Supports M ↑S) (q : Q) : ↥S

Restrict a finitely supported TM0 to the finite subtype of states in its support.

Equations

• Undecidability.TM0FiniteRestriction.liftState M S hS q = if hq : q ∈ S then ⟨q, hq⟩ else default

@[simp]

theorem Undecidability.TM0FiniteRestriction.liftState_coe {Gamma : Type u_1} {Q : Type u_2} [Inhabited Q] (M : Turing.TM0.Machine Gamma Q) (S : Finset Q) (hS : Turing.TM0.Supports M ↑S) {q : Q} (hq : q ∈ S) : ↑(liftState M S hS q) = q

noncomputable def Undecidability.TM0FiniteRestriction.machine {Gamma : Type u_1} {Q : Type u_2} [Inhabited Q] (M : Turing.TM0.Machine Gamma Q) (S : Finset Q) (hS : Turing.TM0.Supports M ↑S) : Turing.TM0.Machine Gamma ↥S

The Post machine obtained by restricting the compiled machine to its finite state support.

Equations

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

def Undecidability.TM0FiniteRestriction.includeCfg {Gamma : Type u_1} {Q : Type u_2} [Inhabited Gamma] (S : Finset Q) : Turing.TM0.Cfg Gamma ↥S → Turing.TM0.Cfg Gamma Q

The configuration map including supported states into the original state type.

Equations

• Undecidability.TM0FiniteRestriction.includeCfg S { q := q, Tape := tape } = { q := ↑q, Tape := tape }

theorem Undecidability.TM0FiniteRestriction.step_map {Gamma : Type u_1} {Q : Type u_2} [Inhabited Gamma] [Inhabited Q] (M : Turing.TM0.Machine Gamma Q) (S : Finset Q) (hS : Turing.TM0.Supports M ↑S) (c : Turing.TM0.Cfg Gamma ↥S) : Option.map (includeCfg S) (Turing.TM0.step (machine M S hS) c) = Turing.TM0.step M (includeCfg S c)

theorem Undecidability.TM0FiniteRestriction.respects {Gamma : Type u_1} {Q : Type u_2} [Inhabited Gamma] [Inhabited Q] (M : Turing.TM0.Machine Gamma Q) (S : Finset Q) (hS : Turing.TM0.Supports M ↑S) : StateTransition.Respects (Turing.TM0.step (machine M S hS)) (Turing.TM0.step M) fun (c : Turing.TM0.Cfg Gamma ↥S) (d : Turing.TM0.Cfg Gamma Q) => includeCfg S c = d

theorem Undecidability.TM0FiniteRestriction.init_include {Gamma : Type u_1} {Q : Type u_2} [Inhabited Gamma] [Inhabited Q] (M : Turing.TM0.Machine Gamma Q) (S : Finset Q) (hS : Turing.TM0.Supports M ↑S) (input : List Gamma) : includeCfg S (Turing.TM0.init input) = Turing.TM0.init input

theorem Undecidability.TM0FiniteRestriction.eval_dom_iff {Gamma : Type u_1} {Q : Type u_2} [Inhabited Gamma] [Inhabited Q] (M : Turing.TM0.Machine Gamma Q) (S : Finset Q) (hS : Turing.TM0.Supports M ↑S) (input : List Gamma) : (Turing.TM0.eval (machine M S hS) input).Dom ↔ (Turing.TM0.eval M input).Dom

Restricting to a certified finite support preserves the halting domain.

structure Undecidability.TM1BinaryAdapter.Code (Γ : Type u_4) [Inhabited Γ] : Type u_4

A fixed-length binary encoding of a finite tape alphabet, with the blank symbol represented by an all-zero block.

• width : ℕ

  The fixed length of each binary code word.

• enc : Γ → List.Vector Bool self.width

  The fixed-width binary encoding of an alphabet symbol.

• dec : List.Vector Bool self.width → Γ

  The decoder from a fixed-width binary word to an alphabet symbol.

• enc_blank : self.enc default = List.Vector.replicate self.width false
• dec_enc (a : Γ) : self.dec (self.enc a) = a

theorem Undecidability.TM1BinaryAdapter.exists_code (Γ : Type u_4) [Inhabited Γ] [Finite Γ] : Nonempty (Code Γ)

Every inhabited finite alphabet admits a fixed-length binary code.

noncomputable def Undecidability.TM1BinaryAdapter.canonicalCode (Γ : Type u_4) [Inhabited Γ] [Finite Γ] : Code Γ

A canonical (noncomputably chosen) binary code for a finite alphabet.

Equations

• Undecidability.TM1BinaryAdapter.canonicalCode Γ = Classical.choice ⋯

def Undecidability.TM1BinaryAdapter.program {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] (B : Code Γ) (M : Λ → Turing.TM1.Stmt Γ Λ σ) : Turing.TM1to1.Λ' Γ Λ σ → Turing.TM1.Stmt Bool (Turing.TM1to1.Λ' Γ Λ σ) σ

The binary TM1 program produced by Mathlib's block-code compiler.

Equations

• Undecidability.TM1BinaryAdapter.program B M = Turing.TM1to1.tr B.enc B.dec M

def Undecidability.TM1BinaryAdapter.machine {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited σ] (B : Code Γ) (M : Λ → Turing.TM1.Stmt Γ Λ σ) : Turing.TM0.Machine Bool (Turing.TM1to0.Λ' (program B M))

Compile a finite-alphabet TM1 program all the way to a binary TM0.

Equations

• Undecidability.TM1BinaryAdapter.machine B M = Turing.TM1to0.tr (Undecidability.TM1BinaryAdapter.program B M)

def Undecidability.TM1BinaryAdapter.encodeInput {Γ : Type u_1} [Inhabited Γ] (B : Code Γ) (input : List Γ) : List Bool

Encode a finite input word by concatenating its fixed-width codewords.

Equations

• Undecidability.TM1BinaryAdapter.encodeInput B input = List.flatMap (fun (a : Γ) => (B.enc a).toList) input

theorem Undecidability.TM1BinaryAdapter.encodeInput_computable {Γ : Type u_1} [Inhabited Γ] [Primcodable Γ] [Finite Γ] (B : Code Γ) : Computable (encodeInput B)

Fixed-width block encoding of words over a finite computably coded alphabet is computable. No effectiveness hypothesis on the particular code table is needed: every function on a finite domain is primitive recursive.

theorem Undecidability.TM1BinaryAdapter.program_eval_dom_iff {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited σ] (B : Code Γ) (M : Λ → Turing.TM1.Stmt Γ Λ σ) (input : List Γ) : (Turing.TM1.eval (program B M) (encodeInput B input)).Dom ↔ (Turing.TM1.eval M input).Dom

Mathlib's binary block compiler preserves the halting domain.

theorem Undecidability.TM1BinaryAdapter.eval_dom_iff {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited σ] (B : Code Γ) (M : Λ → Turing.TM1.Stmt Γ Λ σ) (input : List Γ) : (Turing.TM0.eval (machine B M) (encodeInput B input)).Dom ↔ (Turing.TM1.eval M input).Dom

Compiling further from TM1 to TM0 preserves the halting domain.

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

A finite support for the compiled binary TM0, obtained by composing Mathlib's two support transformations.

Equations

• Undecidability.TM1BinaryAdapter.support B M S = Turing.TM1to0.trStmts (Undecidability.TM1BinaryAdapter.program B M) (Turing.TM1to1.trSupp M S)

theorem Undecidability.TM1BinaryAdapter.machine_supports {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited σ] [Fintype Γ] [Fintype σ] (B : Code Γ) (M : Λ → Turing.TM1.Stmt Γ Λ σ) (S : Finset Λ) (hS : Turing.TM1.Supports M S) : Turing.TM0.Supports (machine B M) ↑(support B M S)

A support certificate for the source program induces one for the binary TM0.

@[reducible]

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

The inhabited finite subtype of the compiled machine's certified support.

Equations

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

noncomputable def Undecidability.TM1BinaryAdapter.finiteMachine {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited σ] [Fintype Γ] [Fintype σ] (B : Code Γ) (M : Λ → Turing.TM1.Stmt Γ Λ σ) (S : Finset Λ) (hS : Turing.TM1.Supports M S) : Turing.TM0.Machine Bool ↥(support B M S)

Restrict the binary compiler output to its certified finite state set.

Equations

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

theorem Undecidability.TM1BinaryAdapter.finite_eval_dom_iff {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [Inhabited Γ] [Inhabited Λ] [Inhabited σ] [Fintype Γ] [Fintype σ] (B : Code Γ) (M : Λ → Turing.TM1.Stmt Γ Λ σ) (S : Finset Λ) (hS : Turing.TM1.Supports M S) (input : List Γ) : (Turing.TM0.eval (finiteMachine B M S hS) (encodeInput B input)).Dom ↔ (Turing.TM1.eval M input).Dom

The finite-state binary machine has exactly the source program's halting domain on encoded inputs.