# mathlibdocumentation

computability.tm_computable

# Computable functions #

This file contains the definition of a Turing machine with some finiteness conditions (bundling the definition of TM2 in turing_machine.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 #

• id_computable_in_poly_time : a TM + a proof it computes the identity on a type in polytime.
• id_computable : 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.fin_tm2  :
Type 1

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

@[protected, instance]
Equations
@[protected, instance]
Equations
def turing.fin_tm2.stmt (tm : turing.fin_tm2) :
Type

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

Equations
@[protected, instance]
def turing.fin_tm2.cfg (tm : turing.fin_tm2) :
Type

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

Equations
@[protected, instance]
Equations
@[simp]
def turing.fin_tm2.step (tm : turing.fin_tm2) :
tm.cfgoption tm.cfg

The step function corresponding to this TM.

Equations
def turing.init_list (tm : turing.fin_tm2) (s : list (tm.Γ tm.k₀)) :
tm.cfg

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

Equations
def turing.halt_list (tm : turing.fin_tm2) (s : list (tm.Γ tm.k₁)) :
tm.cfg

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

Equations
structure turing.evals_to {σ : Type u_1} (f : σ → ) (a : σ) (b : option σ) :
Type

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

structure turing.evals_to_in_time {σ : Type u_1} (f : σ → ) (a : σ) (b : option σ) (m : ) :
Type

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.evals_to.refl {σ : Type u_1} (f : σ → ) (a : σ) :
a

Reflexivity of evals_to in 0 steps.

Equations
def turing.evals_to.trans {σ : Type u_1} (f : σ → ) (a b : σ) (c : option σ) (h₁ : b) (h₂ : c) :
c

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

Equations
def turing.evals_to_in_time.refl {σ : Type u_1} (f : σ → ) (a : σ) :
0

Reflexivity of evals_to_in_time in 0 steps.

Equations
def turing.evals_to_in_time.trans {σ : Type u_1} (f : σ → ) (a b : σ) (c : option σ) (m₁ m₂ : ) (h₁ : m₁) (h₂ : m₂) :
(m₂ + m₁)

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

Equations
def turing.tm2_outputs (tm : turing.fin_tm2) (l : list (tm.Γ tm.k₀)) (l' : option (list (tm.Γ tm.k₁))) :
Type

A proof of tm outputting l' when given l.

Equations
• l' = l) l')
def turing.tm2_outputs_in_time (tm : turing.fin_tm2) (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
• l' m = l) l') m
def turing.tm2_outputs_in_time.to_tm2_outputs {tm : turing.fin_tm2} {l : list (tm.Γ tm.k₀)} {l' : option (list (tm.Γ tm.k₁))} {m : } (h : l' m) :
l'

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

Equations
structure turing.tm2_computable_aux (Γ₀ Γ₁ : Type) :
Type 1

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

structure turing.tm2_computable {α β : Type} (ea : computability.fin_encoding α) (eb : computability.fin_encoding β) (f : α → β) :
Type 1

A Turing machine + a proof it outputs f.

structure turing.tm2_computable_in_time {α β : Type} (ea : computability.fin_encoding α) (eb : computability.fin_encoding β) (f : α → β) :
Type 1

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

structure turing.tm2_computable_in_poly_time {α β : Type} (ea : computability.fin_encoding α) (eb : computability.fin_encoding β) (f : α → β) :
Type 1

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

def turing.tm2_computable_in_time.to_tm2_computable {α β : Type} {ea : computability.fin_encoding α} {eb : computability.fin_encoding β} {f : α → β} (h : f) :
f

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

Equations

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

Equations

A Turing machine computing the identity on α.

Equations
@[protected, instance]
Equations
noncomputable def turing.id_computable_in_poly_time {α : Type} (ea : computability.fin_encoding α) :

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

Equations
@[protected, instance]
Equations
@[protected, instance]
noncomputable def turing.inhabited_tm2_outputs_in_time  :
inhabited (list.map (equiv.cast turing.inhabited_tm2_outputs_in_time._proof_1).inv_fun [ff]) (some (list.map (equiv.cast turing.inhabited_tm2_outputs_in_time._proof_2).inv_fun [ff]))
Equations
@[protected, instance]
noncomputable def turing.inhabited_tm2_outputs  :
inhabited (list.map (equiv.cast turing.inhabited_tm2_outputs._proof_1).inv_fun [ff]) (some (list.map (equiv.cast turing.inhabited_tm2_outputs._proof_2).inv_fun [ff])))
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
noncomputable def turing.id_computable_in_time {α : Type} (ea : computability.fin_encoding α) :

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

Equations
@[protected, instance]
Equations
noncomputable def turing.id_computable {α : Type} (ea : computability.fin_encoding α) :

A proof that the identity map on α is computable.

Equations
@[protected, instance]
Equations
@[protected, instance]
noncomputable def turing.inhabited_tm2_computable_aux  :
Equations