The already verified Mathlib compilers turn the preceding four-stack machine into a deterministic one-tape Post machine.

def Undecidability.fixedUniversalEval (n : ℕ) : Part ℕ

The unary universal partial function used for the fixed machine. Its input is the natural-number code of a partial-recursive program, and that program is run on the fixed input 0.

Equations

• Undecidability.fixedUniversalEval n = (Denumerable.ofNat Nat.Partrec.Code n).eval 0

theorem Undecidability.fixedUniversalEval_partrec : Partrec fixedUniversalEval

theorem Undecidability.exists_fixed_universal_code : ∃ (c : Turing.ToPartrec.Code), ∀ (n : ℕ), (c.eval [n]).Dom ↔ (fixedUniversalEval n).Dom

A code in Mathlib's list-oriented partial-recursive basis which computes the unary universal partial function. This is the fixed program subsequently compiled to a Turing machine.

@[reducible, inline]

abbrev Undecidability.FixedMachine.State : Type

The state type of the universal multi-tape machine compiling partial recursive codes.

Equations

• Undecidability.FixedMachine.State = Turing.PartrecToTM2.Λ'

@[reducible, inline]

abbrev Undecidability.FixedMachine.Symbol : Type

The symbol type of the universal multi-tape machine.

Equations

• Undecidability.FixedMachine.Symbol = Turing.PartrecToTM2.Γ'

@[reducible, inline]

abbrev Undecidability.FixedMachine.Stack : Type

The tape-index type of the universal multi-tape machine.

Equations

• Undecidability.FixedMachine.Stack = Turing.PartrecToTM2.K'

@[instance_reducible]

instance Undecidability.FixedMachine.stackFintype : Fintype Turing.PartrecToTM2.K'

Equations

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

@[instance_reducible]

noncomputable instance Undecidability.FixedMachine.symbolPrimcodable : Primcodable Symbol

Equations

• Undecidability.FixedMachine.symbolPrimcodable = Primcodable.ofEquiv (Fin (Fintype.card Undecidability.FixedMachine.Symbol)) (Fintype.equivFin Undecidability.FixedMachine.Symbol)

theorem Undecidability.FixedMachine.tm2_eval_dom_iff (c : Turing.ToPartrec.Code) (n : ℕ) : (Turing.TM2.eval Turing.PartrecToTM2.tr Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.trList [n])).Dom ↔ (c.eval [n]).Dom

With the initial-state instance specialized to the program c, Mathlib's standard TM2.init is definitionally the configuration used by the verified partial-recursive-to-machine compiler.

@[reducible, inline]

abbrev Undecidability.FixedMachine.TapeSymbol : Type

The alphabet of the one-tape simulation of the universal multi-tape machine.

Equations

• Undecidability.FixedMachine.TapeSymbol = Turing.TM2to1.Γ' Undecidability.FixedMachine.Stack fun (x : Undecidability.FixedMachine.Stack) => Undecidability.FixedMachine.Symbol

@[reducible, inline]

abbrev Undecidability.FixedMachine.StackColumn : Type

A column recording the optional symbol on each tape of the multi-tape machine.

Equations

• Undecidability.FixedMachine.StackColumn = (Undecidability.FixedMachine.Stack → Option Undecidability.FixedMachine.Symbol)

@[instance_reducible]

noncomputable instance Undecidability.FixedMachine.stackColumnPrimcodable : Primcodable StackColumn

Equations

• Undecidability.FixedMachine.stackColumnPrimcodable = Primcodable.ofEquiv (Fin (Fintype.card Undecidability.FixedMachine.StackColumn)) (Fintype.equivFin Undecidability.FixedMachine.StackColumn)

@[instance_reducible]

noncomputable instance Undecidability.FixedMachine.tapeSymbolPrimcodable : Primcodable TapeSymbol

Equations

• Undecidability.FixedMachine.tapeSymbolPrimcodable = id inferInstance

@[reducible, inline]

abbrev Undecidability.FixedMachine.OneTapeState : Type

The state type of the one-tape simulation of the universal multi-tape machine.

Equations

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

def Undecidability.FixedMachine.oneTapeProgram : OneTapeState → Turing.TM1.Stmt TapeSymbol OneTapeState (Option Symbol)

The transition program of the one-tape simulation of the universal multi-tape machine.

Equations

• Undecidability.FixedMachine.oneTapeProgram = Turing.TM2to1.tr Turing.PartrecToTM2.tr

@[reducible, inline]

abbrev Undecidability.FixedMachine.PostState : Type

The state type obtained by compiling the one-tape machine to a Post machine.

Equations

• Undecidability.FixedMachine.PostState = Turing.TM1to0.Λ' Undecidability.FixedMachine.oneTapeProgram

@[reducible]

def Undecidability.FixedMachine.stateInhabited (c : Turing.ToPartrec.Code) : Inhabited State

The initial state furnishing an inhabited instance for a specified partial recursive code.

Equations

• Undecidability.FixedMachine.stateInhabited c = { default := Turing.PartrecToTM2.trNormal c Turing.PartrecToTM2.Cont'.halt }

@[reducible]

def Undecidability.FixedMachine.oneTapeStateInhabited (c : Turing.ToPartrec.Code) : Inhabited OneTapeState

The initial state furnishing an inhabited instance for the one-tape simulation.

Equations

• Undecidability.FixedMachine.oneTapeStateInhabited c = Turing.TM2to1.Λ'.inhabited

@[reducible]

def Undecidability.FixedMachine.postStateInhabited (c : Turing.ToPartrec.Code) : Inhabited PostState

The initial state furnishing an inhabited instance for the compiled Post machine.

Equations

• Undecidability.FixedMachine.postStateInhabited c = Turing.TM1to0.instInhabitedΛ' Undecidability.FixedMachine.oneTapeProgram

def Undecidability.FixedMachine.postMachine (c : Turing.ToPartrec.Code) : Turing.TM0.Machine TapeSymbol PostState

The Post machine compiling a specified partial recursive code.

Equations

• Undecidability.FixedMachine.postMachine c = Turing.TM1to0.tr Undecidability.FixedMachine.oneTapeProgram

def Undecidability.FixedMachine.postInput (n : ℕ) : List TapeSymbol

The one-tape input encoding of a natural-number input to the universal machine.

Equations

• Undecidability.FixedMachine.postInput n = Turing.TM2to1.trInit Turing.PartrecToTM2.K'.main (Turing.PartrecToTM2.trList [n])

theorem Undecidability.FixedMachine.trNat_computable : Computable Turing.PartrecToTM2.trNat

theorem Undecidability.FixedMachine.trSingleton_computable : Computable fun (n : ℕ) => Turing.PartrecToTM2.trList [n]

theorem Undecidability.FixedMachine.trInit_main_computable : Computable fun (L : List Symbol) => Turing.TM2to1.trInit Turing.PartrecToTM2.K'.main L

theorem Undecidability.FixedMachine.postInput_computable : Computable postInput

The variable input word for the fixed Post machine is computably obtained from the natural-number program code.

theorem Undecidability.FixedMachine.postInput_encode_computable : Computable fun (p : Nat.Partrec.Code) => postInput (Encodable.encode p)

theorem Undecidability.FixedMachine.post_eval_dom_iff (c : Turing.ToPartrec.Code) (n : ℕ) : (Turing.TM0.eval (postMachine c) (postInput n)).Dom ↔ (c.eval [n]).Dom

noncomputable def Undecidability.FixedMachine.oneTapeSupport (c : Turing.ToPartrec.Code) : Finset OneTapeState

The explicit finite support of the intermediate deterministic one-tape machine. This is exposed for bridges that operate at the TM1 level.

Equations

• Undecidability.FixedMachine.oneTapeSupport c = Turing.TM2to1.trSupp Turing.PartrecToTM2.tr (Turing.PartrecToTM2.codeSupp c Turing.PartrecToTM2.Cont'.halt)

theorem Undecidability.FixedMachine.oneTapeProgram_supports (c : Turing.ToPartrec.Code) : Turing.TM1.Supports oneTapeProgram (oneTapeSupport c)

theorem Undecidability.FixedMachine.post_halting_not_computable (c : Turing.ToPartrec.Code) (hc : ∀ (n : ℕ), (c.eval [n]).Dom ↔ (fixedUniversalEval n).Dom) : ¬ComputablePred fun (input : List TapeSymbol) => (Turing.TM0.eval (postMachine c) input).Dom

theorem Undecidability.FixedMachine.oneTape_halting_not_computable (c : Turing.ToPartrec.Code) (hc : ∀ (n : ℕ), (c.eval [n]).Dom ↔ (fixedUniversalEval n).Dom) : ¬ComputablePred fun (input : List TapeSymbol) => (Turing.TM1.eval oneTapeProgram input).Dom

Undecidability already holds for the intermediate deterministic one-tape machine, before compiling it to a Post machine.