# 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 :

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.

Instances For
Equations
• = tm.kDecidableEq
Equations
• = { default := tm.initialState }

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

Equations
Instances For

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

Equations
Instances For
Equations

The step function corresponding to this TM.

Equations
Instances For
def Turing.initList (tm : Turing.FinTM2) (s : List (tm tm.k₀)) :

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

Equations
• = { l := some tm.main, var := tm.initialState, stk := fun (k : tm.K) => if h : k = tm.k₀ then Eq.mpr s else [] }
Instances For
def Turing.haltList (tm : Turing.FinTM2) (s : List (tm tm.k₁)) :

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

Equations
• = { l := none, var := tm.initialState, stk := fun (k : tm.K) => if h : k = tm.k₁ then Eq.mpr s else [] }
Instances For
structure Turing.EvalsTo {σ : Type u_1} (f : σ) (a : σ) (b : ) :

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

Instances For
structure Turing.EvalsToInTime {σ : Type u_1} (f : σ) (a : σ) (b : ) (m : ) extends :

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.

• steps :
• evals_in_steps : (flip bind f)^[self.steps] (some a) = b
• steps_le_m : self.steps m
Instances For
def Turing.EvalsTo.refl {σ : Type u_1} (f : σ) (a : σ) :

Reflexivity of EvalsTo in 0 steps.

Equations
• = { steps := 0, evals_in_steps := }
Instances For
def Turing.EvalsTo.trans {σ : Type u_1} (f : σ) (a : σ) (b : σ) (c : ) (h₁ : Turing.EvalsTo f a (some b)) (h₂ : ) :

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

Equations
Instances For
def Turing.EvalsToInTime.refl {σ : Type u_1} (f : σ) (a : σ) :

Reflexivity of EvalsToInTime in 0 steps.

Equations
Instances For
def Turing.EvalsToInTime.trans {σ : Type u_1} (f : σ) (m₁ : ) (m₂ : ) (a : σ) (b : σ) (c : ) (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.

Equations
Instances For
def Turing.TM2Outputs (tm : Turing.FinTM2) (l : List (tm tm.k₀)) (l' : Option (List (tm tm.k₁))) :

A proof of tm outputting l' when given l.

Equations
Instances For
def Turing.TM2OutputsInTime (tm : Turing.FinTM2) (l : List (tm tm.k₀)) (l' : Option (List (tm tm.k₁))) (m : ) :

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

Equations
Instances For
def Turing.TM2OutputsInTime.toTM2Outputs {tm : Turing.FinTM2} {l : List (tm tm.k₀)} {l' : Option (List (tm tm.k₁))} {m : } (h : Turing.TM2OutputsInTime tm l l' m) :

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

Equations
• = h.toEvalsTo
Instances For
structure Turing.TM2ComputableAux (Γ₀ : Type) (Γ₁ : Type) :

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

• inputAlphabet : self.tm self.tm.k₀ Γ₀
• outputAlphabet : self.tm self.tm.k₁ Γ₁
Instances For
structure Turing.TM2Computable {α : Type} {β : Type} (ea : ) (eb : ) (f : αβ) extends :

A Turing machine + a proof it outputs f.

• inputAlphabet : self.tm self.tm.k₀ ea
• outputAlphabet : self.tm self.tm.k₁ eb
• outputsFun : (a : α) → Turing.TM2Outputs self.tm (List.map self.inputAlphabet.invFun (ea.encode a)) (some (List.map self.outputAlphabet.invFun (eb.encode (f a))))
Instances For
structure Turing.TM2ComputableInTime {α : Type} {β : Type} (ea : ) (eb : ) (f : αβ) extends :

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

Instances For
structure Turing.TM2ComputableInPolyTime {α : Type} {β : Type} (ea : ) (eb : ) (f : αβ) extends :

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

Instances For
def Turing.TM2ComputableInTime.toTM2Computable {α : Type} {β : Type} {ea : } {eb : } {f : αβ} (h : ) :

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

Equations
Instances For
def Turing.TM2ComputableInPolyTime.toTM2ComputableInTime {α : Type} {β : Type} {ea : } {eb : } {f : αβ} (h : ) :

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

Equations
• = { toTM2ComputableAux := h.toTM2ComputableAux, time := fun (n : ) => Polynomial.eval n h.time, outputsFun := h.outputsFun }
Instances For

A Turing machine computing the identity on α.

Equations
Instances For
Equations
def Turing.idComputableInPolyTime {α : Type} (ea : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Turing.idComputableInTime {α : Type} (ea : ) :

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

Equations
Instances For
def Turing.idComputable {α : Type} (ea : ) :

A proof that the identity map on α is computable.

Equations
Instances For
Equations