# Documentation

Mathlib.Computability.TMComputable

# 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

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

Instances For

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

Instances For

The step function corresponding to this TM.

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

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

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

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

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.

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

Reflexivity of EvalsTo in 0 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.

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

Reflexivity of EvalsToInTime in 0 steps.

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.

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

A proof of tm outputting l' when given l.

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

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

Instances For
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) :

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

Instances For
structure Turing.TM2ComputableAux (Γ₀ : Type) (Γ₁ : Type) :

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

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

A Turing machine + a proof it outputs f.

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.

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

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

Instances For

A Turing machine computing the identity on α.

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

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

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

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

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

A proof that the identity map on α is computable.

Instances For