Computable functions

This file contains the definition of a Turing machine with some finiteness conditions (bundling the definition of TM2 in StackTuringMachine.lean), a definition of when a TM gives a certain output (in a certain time), and the definition of computability (in polynomial time or any time function) of a function between two types that have an encoding (as in Encoding.lean).

Main theorems

• idComputableInPolyTime : a TM + a proof it computes the identity on a type in polytime.
• idComputable : a TM + a proof it computes the identity on a type.

Implementation notes

To count the execution time of a Turing machine, we have decided to count the number of times the step function is used. Each step executes a statement (of type Stmt); this is a function, and generally contains multiple "fundamental" steps (pushing, popping, and so on). However, as functions only contain a finite number of executions and each one is executed at most once, this execution time is up to multiplication by a constant the amount of fundamental steps.

structure Turing.FinTM2 : Type 1

A bundled TM2 (an equivalent of the classical Turing machine, defined starting from the namespace Turing.TM2 in StackTuringMachine.lean), with an input and output stack, a main function, an initial state and some finiteness guarantees.

• K : Type

  index type of stacks

• kDecidableEq : DecidableEq self.K
• kFin : Fintype self.K

  A TM2 machine has finitely many stacks.

• k₀ : self.K

  input resp. output stack

• k₁ : self.K

  input resp. output stack

• Γ : self.K → Type

  type of stack elements

• Λ : Type

  type of function labels

• main : self.Λ

  a main function: the initial function that is executed, given by its label

• ΛFin : Fintype self.Λ

  A TM2 machine has finitely many function labels.

• σ : Type

  type of states of the machine

• initialState : self.σ

  the initial state of the machine

• σFin : Fintype self.σ

  a TM2 machine has finitely many internal states.

• Γk₀Fin : Fintype (self.Γ self.k₀)

  Each internal stack is finite.

• m : self.Λ → TM2.Stmt self.Γ self.Λ self.σ

  the program itself, i.e. one function for every function label

@[implicit_reducible]

instance Turing.FinTM2.decidableEqK (tm : FinTM2) : DecidableEq tm.K

Equations

• tm.decidableEqK = tm.kDecidableEq

@[implicit_reducible]

instance Turing.FinTM2.inhabitedσ (tm : FinTM2) : Inhabited tm.σ

Equations

• tm.inhabitedσ = { default := tm.initialState }

def Turing.FinTM2.Stmt (tm : FinTM2) : Type

The type of statements (functions) corresponding to this TM.

Equations

• tm.Stmt = Turing.TM2.Stmt tm.Γ tm.Λ tm.σ

@[implicit_reducible]

instance Turing.FinTM2.inhabitedStmt (tm : FinTM2) : Inhabited tm.Stmt

Equations

• tm.inhabitedStmt = inferInstanceAs (Inhabited (Turing.TM2.Stmt tm.Γ tm.Λ tm.σ))

def Turing.FinTM2.Cfg (tm : FinTM2) : Type

The type of configurations (functions) corresponding to this TM.

Equations

• tm.Cfg = Turing.TM2.Cfg tm.Γ tm.Λ tm.σ

@[implicit_reducible]

instance Turing.FinTM2.inhabitedCfg (tm : FinTM2) : Inhabited tm.Cfg

Equations

• tm.inhabitedCfg = Turing.TM2.Cfg.inhabited tm.Γ tm.Λ tm.σ

def Turing.FinTM2.step (tm : FinTM2) : tm.Cfg → Option tm.Cfg

The step function corresponding to this TM.

Equations

• tm.step = Turing.TM2.step tm.m

def Turing.initList (tm : FinTM2) (s : List (tm.Γ tm.k₀)) : tm.Cfg

The initial configuration corresponding to a list in the input alphabet.

Equations

• Turing.initList tm s = { l := some tm.main, var := tm.initialState, stk := fun (k : tm.K) => if h : k = tm.k₀ then ⋯.mpr s else [] }

def Turing.haltList (tm : FinTM2) (s : List (tm.Γ tm.k₁)) : tm.Cfg

The final configuration corresponding to a list in the output alphabet.

Equations

• Turing.haltList tm s = { l := none, var := tm.initialState, stk := fun (k : tm.K) => if h : k = tm.k₁ then ⋯.mpr s else [] }

@[deprecated StateTransition.EvalsTo (since := "2026-03-06")]

def Turing.EvalsTo {σ : Type u_1} (f : σ → Option σ) (a : σ) (b : Option σ) : Type

Alias of StateTransition.EvalsTo.

Equations

• @Turing.EvalsTo = @StateTransition.EvalsTo

@[deprecated StateTransition.EvalsToInTime (since := "2026-03-06")]

def Turing.EvalsToInTime {σ : Type u_1} (f : σ → Option σ) (a : σ) (b : Option σ) (m : ℕ) : Type

Alias of StateTransition.EvalsToInTime.

Equations

• @Turing.EvalsToInTime = @StateTransition.EvalsToInTime

def Turing.TM2Outputs (tm : FinTM2) (l : List (tm.Γ tm.k₀)) (l' : Option (List (tm.Γ tm.k₁))) : Type

A proof of tm outputting l' when given l.

Equations

• Turing.TM2Outputs tm l l' = StateTransition.EvalsTo tm.step (Turing.initList tm l) (Option.map (Turing.haltList tm) l')

def Turing.TM2OutputsInTime (tm : FinTM2) (l : List (tm.Γ tm.k₀)) (l' : Option (List (tm.Γ tm.k₁))) (m : ℕ) : Type

A proof of tm outputting l' when given l in at most m steps.

Equations

• Turing.TM2OutputsInTime tm l l' m = StateTransition.EvalsToInTime tm.step (Turing.initList tm l) (Option.map (Turing.haltList tm) l') m

def Turing.TM2OutputsInTime.toTM2Outputs {tm : FinTM2} {l : List (tm.Γ tm.k₀)} {l' : Option (List (tm.Γ tm.k₁))} {m : ℕ} (h : TM2OutputsInTime tm l l' m) : TM2Outputs tm l l'

The forgetful map, forgetting the upper bound on the number of steps.

Equations

• h.toTM2Outputs = h.toEvalsTo

structure Turing.TM2ComputableAux (Γ₀ Γ₁ : Type) : Type 1

A (bundled TM2) Turing machine with input alphabet equivalent to Γ₀ and output alphabet equivalent to Γ₁.

• tm : FinTM2

  the underlying bundled TM2

• inputAlphabet : self.tm.Γ self.tm.k₀ ≃ Γ₀

  the input alphabet is equivalent to Γ₀

• outputAlphabet : self.tm.Γ self.tm.k₁ ≃ Γ₁

  the output alphabet is equivalent to Γ₁

structure Turing.TM2Computable {α β αΓ βΓ : Type} (ea : α → List αΓ) (eb : β → List βΓ) (f : α → β) extends Turing.TM2ComputableAux αΓ βΓ : Type 1

A Turing machine + a proof it outputs f.

• tm : FinTM2
• inputAlphabet : self.tm.Γ self.tm.k₀ ≃ αΓ
• outputAlphabet : self.tm.Γ self.tm.k₁ ≃ βΓ
• outputsFun (a : α) : TM2Outputs self.tm (List.map self.inputAlphabet.invFun (ea a)) (some (List.map self.outputAlphabet.invFun (eb (f a))))

  a proof this machine outputs f

structure Turing.TM2ComputableInTime {α β αΓ βΓ : Type} (ea : α → List αΓ) (eb : β → List βΓ) (f : α → β) extends Turing.TM2ComputableAux αΓ βΓ : Type 1

A Turing machine + a time function + a proof it outputs f in at most time(input.length) steps.

• tm : FinTM2
• inputAlphabet : self.tm.Γ self.tm.k₀ ≃ αΓ
• outputAlphabet : self.tm.Γ self.tm.k₁ ≃ βΓ
• time : ℕ → ℕ

  a time function

• outputsFun (a : α) : TM2OutputsInTime self.tm (List.map self.inputAlphabet.invFun (ea a)) (some (List.map self.outputAlphabet.invFun (eb (f a)))) (self.time (ea a).length)

  proof this machine outputs f in at most time(input.length) steps

structure Turing.TM2ComputableInPolyTime {α β αΓ βΓ : Type} (ea : α → List αΓ) (eb : β → List βΓ) (f : α → β) extends Turing.TM2ComputableAux αΓ βΓ : Type 1

A Turing machine + a polynomial time function + a proof it outputs f in at most time(input.length) steps.

• tm : FinTM2
• inputAlphabet : self.tm.Γ self.tm.k₀ ≃ αΓ
• outputAlphabet : self.tm.Γ self.tm.k₁ ≃ βΓ
• time : Polynomial ℕ

  a polynomial time function

• outputsFun (a : α) : TM2OutputsInTime self.tm (List.map self.inputAlphabet.invFun (ea a)) (some (List.map self.outputAlphabet.invFun (eb (f a)))) (Polynomial.eval (ea a).length self.time)

  proof that this machine outputs f in at most time(input.length) steps

def Turing.TM2ComputableInTime.toTM2Computable {α β αΓ βΓ : Type} {ea : α → List αΓ} {eb : β → List βΓ} {f : α → β} (h : TM2ComputableInTime ea eb f) : TM2Computable ea eb f

A forgetful map, forgetting the time bound on the number of steps.

Equations

• h.toTM2Computable = { toTM2ComputableAux := h.toTM2ComputableAux, outputsFun := fun (a : α) => (h.outputsFun a).toTM2Outputs }

def Turing.TM2ComputableInPolyTime.toTM2ComputableInTime {α β αΓ βΓ : Type} {ea : α → List αΓ} {eb : β → List βΓ} {f : α → β} (h : TM2ComputableInPolyTime ea eb f) : TM2ComputableInTime ea eb f

A forgetful map, forgetting that the time function is polynomial.

Equations

• h.toTM2ComputableInTime = { toTM2ComputableAux := h.toTM2ComputableAux, time := fun (n : ℕ) => Polynomial.eval n h.time, outputsFun := h.outputsFun }

def Turing.idComputer (αΓ : Type) [Fintype αΓ] : FinTM2

A Turing machine computing the identity on α.

Equations

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

@[implicit_reducible]

instance Turing.inhabitedFinTM2 : Inhabited FinTM2

Equations

• Turing.inhabitedFinTM2 = { default := Turing.idComputer Bool }

noncomputable def Turing.idComputableInPolyTime {α αΓ : Type} [Fintype αΓ] (ea : α → List αΓ) : TM2ComputableInPolyTime ea ea id

A proof that the identity map on α is computable in polytime.

Equations

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

@[implicit_reducible]

noncomputable instance Turing.inhabitedTM2ComputableInPolyTime : Inhabited (TM2ComputableInPolyTime Computability.encodeBool Computability.encodeBool id)

Equations

• Turing.inhabitedTM2ComputableInPolyTime = { default := Turing.idComputableInPolyTime Computability.encodeBool }

@[implicit_reducible]

noncomputable instance Turing.inhabitedTM2OutputsInTime : Inhabited (TM2OutputsInTime (idComputer Bool) (List.map (Equiv.cast ⋯).invFun [false]) (some (List.map (Equiv.cast ⋯).invFun [false])) (Polynomial.eval 1 1))

Equations

• Turing.inhabitedTM2OutputsInTime = { default := (Turing.idComputableInPolyTime Computability.encodeBool).outputsFun false }

@[implicit_reducible]

noncomputable instance Turing.inhabitedTM2Outputs : Inhabited (TM2Outputs (idComputer Bool) (List.map (Equiv.cast ⋯).invFun [false]) (some (List.map (Equiv.cast ⋯).invFun [false])))

Equations

• Turing.inhabitedTM2Outputs = { default := default.toTM2Outputs }

@[implicit_reducible]

instance Turing.inhabitedEvalsToInTime : Inhabited (StateTransition.EvalsToInTime (fun (x : Unit) => some PUnit.unit) PUnit.unit (some PUnit.unit) 0)

Equations

• Turing.inhabitedEvalsToInTime = { default := StateTransition.EvalsToInTime.refl (fun (x : Unit) => some PUnit.unit) PUnit.unit }

@[implicit_reducible]

instance Turing.inhabitedTM2EvalsTo : Inhabited (StateTransition.EvalsTo (fun (x : Unit) => some PUnit.unit) PUnit.unit (some PUnit.unit))

Equations

• Turing.inhabitedTM2EvalsTo = { default := StateTransition.EvalsTo.refl (fun (x : Unit) => some PUnit.unit) PUnit.unit }

noncomputable def Turing.idComputableInTime {α αΓ : Type} [Fintype αΓ] (ea : α → List αΓ) : TM2ComputableInTime ea ea id

A proof that the identity map on α is computable in time.

Equations

• Turing.idComputableInTime ea = (Turing.idComputableInPolyTime ea).toTM2ComputableInTime

@[implicit_reducible]

noncomputable instance Turing.inhabitedTM2ComputableInTime : Inhabited (TM2ComputableInTime Computability.encodeBool Computability.encodeBool id)

Equations

• Turing.inhabitedTM2ComputableInTime = { default := Turing.idComputableInTime Computability.encodeBool }

noncomputable def Turing.idComputable {α αΓ : Type} [Fintype αΓ] (ea : α → List αΓ) : TM2Computable ea ea id

A proof that the identity map on α is computable.

Equations

• Turing.idComputable ea = (Turing.idComputableInTime ea).toTM2Computable

@[implicit_reducible]

noncomputable instance Turing.inhabitedTM2Computable : Inhabited (TM2Computable Computability.encodeBool Computability.encodeBool id)

Equations

• Turing.inhabitedTM2Computable = { default := Turing.idComputable Computability.encodeBool }

@[implicit_reducible]

noncomputable instance Turing.inhabitedTM2ComputableAux : Inhabited (TM2ComputableAux Bool Bool)

Equations

• Turing.inhabitedTM2ComputableAux = { default := default.toTM2ComputableAux }