Computable functions

This file contains the definition of a Turing machine with some finiteness conditions (bundling the definition of TM2 in TuringMachine.lean), a definition of when a TM gives a certain output (in a certain time), and the definition of computability (in polytime 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, 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

• K : Type
• kDecidableEq : DecidableEq s.K
• kFin : Fintype s.K
• k₀ : s.K
• k₁ : s.K
• Γ : s.K → Type
• Λ : Type
• main : s.Λ
• ΛFin : Fintype s.Λ
• σ : Type
• initialState : s.σ
• σFin : Fintype s.σ
• Γk₀Fin : Fintype (Turing.FinTM2.Γ s s.k₀)
• m : s.Λ → Turing.TM2.Stmt s.Γ s.Λ s.σ

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

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

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

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

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

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

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

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

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

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

The step function corresponding to this TM.

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

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

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

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

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

• steps : ℕ
• evals_in_steps : (flip bind f)^[s.steps] (some a) = b

A "proof" of the fact that f eventually reaches b when repeatedly evaluated on a, remembering the number of steps it takes.

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

• steps : ℕ
• evals_in_steps : (flip bind f)^[s.steps] (some a) = b
• steps_le_m : s.steps ≤ m

A "proof" of the fact that f eventually reaches b in at most m steps when repeatedly evaluated on a, remembering the number of steps it takes.

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

Reflexivity of EvalsTo in 0 steps.

def Turing.EvalsTo.trans {σ : Type u_1} (f : σ → Option σ) (a : σ) (b : σ) (c : Option σ) (h₁ : Turing.EvalsTo f a (some b)) (h₂ : Turing.EvalsTo f b c) : Turing.EvalsTo f a c

Transitivity of EvalsTo in the sum of the numbers of steps.

def Turing.EvalsToInTime.refl {σ : Type u_1} (f : σ → Option σ) (a : σ) : Turing.EvalsToInTime f a (some a) 0

Reflexivity of EvalsToInTime in 0 steps.

def Turing.EvalsToInTime.trans {σ : Type u_1} (f : σ → Option σ) (m₁ : ℕ) (m₂ : ℕ) (a : σ) (b : σ) (c : Option σ) (h₁ : Turing.EvalsToInTime f a (some b) m₁) (h₂ : Turing.EvalsToInTime f b c m₂) : Turing.EvalsToInTime f a c (m₂ + m₁)

Transitivity of EvalsToInTime in the sum of the numbers of steps.

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

A proof of tm outputting l' when given l.

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

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

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

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

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

• tm : Turing.FinTM2
• inputAlphabet : Turing.FinTM2.Γ s.tm s.tm.k₀ ≃ Γ₀
• outputAlphabet : Turing.FinTM2.Γ s.tm s.tm.k₁ ≃ Γ₁

A Turing machine with input alphabet equivalent to Γ₀ and output alphabet equivalent to Γ₁.

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

• tm : Turing.FinTM2
• inputAlphabet : Turing.FinTM2.Γ s.tm s.tm.k₀ ≃ ea.Γ
• outputAlphabet : Turing.FinTM2.Γ s.tm s.tm.k₁ ≃ eb.Γ
• outputsFun : (a : α) → Turing.TM2Outputs s.tm (List.map s.inputAlphabet.invFun (Computability.Encoding.encode ea.toEncoding a)) (some (List.map s.outputAlphabet.invFun (Computability.Encoding.encode eb.toEncoding (f a))))

A Turing machine + a proof it outputs f.

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

• tm : Turing.FinTM2
• inputAlphabet : Turing.FinTM2.Γ s.tm s.tm.k₀ ≃ ea.Γ
• outputAlphabet : Turing.FinTM2.Γ s.tm s.tm.k₁ ≃ eb.Γ
• time : ℕ → ℕ
• outputsFun : (a : α) → Turing.TM2OutputsInTime s.tm (List.map s.inputAlphabet.invFun (Computability.Encoding.encode ea.toEncoding a)) (some (List.map s.outputAlphabet.invFun (Computability.Encoding.encode eb.toEncoding (f a)))) (Turing.TM2ComputableInTime.time s (List.length (Computability.Encoding.encode ea.toEncoding a)))

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

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

• tm : Turing.FinTM2
• inputAlphabet : Turing.FinTM2.Γ s.tm s.tm.k₀ ≃ ea.Γ
• outputAlphabet : Turing.FinTM2.Γ s.tm s.tm.k₁ ≃ eb.Γ
• time : Polynomial ℕ
• outputsFun : (a : α) → Turing.TM2OutputsInTime s.tm (List.map s.inputAlphabet.invFun (Computability.Encoding.encode ea.toEncoding a)) (some (List.map s.outputAlphabet.invFun (Computability.Encoding.encode eb.toEncoding (f a)))) (Polynomial.eval (List.length (Computability.Encoding.encode ea.toEncoding a)) s.time)

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

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

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

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

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

def Turing.idComputer {α : Type} (ea : Computability.FinEncoding α) : Turing.FinTM2

A Turing machine computing the identity on α.

instance Turing.inhabitedFinTM2 : Inhabited Turing.FinTM2

def Turing.idComputableInPolyTime {α : Type} (ea : Computability.FinEncoding α) : Turing.TM2ComputableInPolyTime ea ea id

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

instance Turing.inhabitedTM2ComputableInPolyTime : Inhabited (Turing.TM2ComputableInPolyTime default default id)

instance Turing.inhabitedTM2OutputsInTime : Inhabited (Turing.TM2OutputsInTime (Turing.idComputer Computability.finEncodingBoolBool) (List.map (Equiv.cast (_ : Turing.FinTM2.Γ (Turing.idComputer Computability.finEncodingBoolBool) (Turing.idComputer Computability.finEncodingBoolBool).k₀ = Turing.FinTM2.Γ (Turing.idComputer Computability.finEncodingBoolBool) (Turing.idComputer Computability.finEncodingBoolBool).k₀)).invFun [false]) (some (List.map (Equiv.cast (_ : Turing.FinTM2.Γ (Turing.idComputer Computability.finEncodingBoolBool) (Turing.idComputer Computability.finEncodingBoolBool).k₁ = Turing.FinTM2.Γ (Turing.idComputer Computability.finEncodingBoolBool) (Turing.idComputer Computability.finEncodingBoolBool).k₁)).invFun [false])) (Polynomial.eval 1 1))

instance Turing.inhabitedTM2Outputs : Inhabited (Turing.TM2Outputs (Turing.idComputer Computability.finEncodingBoolBool) (List.map (Equiv.cast (_ : Turing.FinTM2.Γ (Turing.idComputer Computability.finEncodingBoolBool) (Turing.idComputer Computability.finEncodingBoolBool).k₀ = Turing.FinTM2.Γ (Turing.idComputer Computability.finEncodingBoolBool) (Turing.idComputer Computability.finEncodingBoolBool).k₀)).invFun [false]) (some (List.map (Equiv.cast (_ : Turing.FinTM2.Γ (Turing.idComputer Computability.finEncodingBoolBool) (Turing.idComputer Computability.finEncodingBoolBool).k₁ = Turing.FinTM2.Γ (Turing.idComputer Computability.finEncodingBoolBool) (Turing.idComputer Computability.finEncodingBoolBool).k₁)).invFun [false])))

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

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

def Turing.idComputableInTime {α : Type} (ea : Computability.FinEncoding α) : Turing.TM2ComputableInTime ea ea id

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

instance Turing.inhabitedTM2ComputableInTime : Inhabited (Turing.TM2ComputableInTime Computability.finEncodingBoolBool Computability.finEncodingBoolBool id)

def Turing.idComputable {α : Type} (ea : Computability.FinEncoding α) : Turing.TM2Computable ea ea id

A proof that the identity map on α is computable.

instance Turing.inhabitedTM2Computable : Inhabited (Turing.TM2Computable Computability.finEncodingBoolBool Computability.finEncodingBoolBool id)

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