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

@[instance]

Equations
@[instance]

Equations

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

Equations

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

Equations
@[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) :
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) :
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} :
(σ → 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} :
(σ → option σ)σ → → Type
• to_evals_to : b
• steps_le_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.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 σ) :
b 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₂ : ) :
m₁ 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) :
list (tm.Γ tm.k₀)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) :
list (tm.Γ tm.k₀)option (list (tm.Γ tm.k₁)) → 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 : } :
l' m l'

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

Equations
structure turing.tm2_computable_aux  :
Type → Type → Type 1

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

structure turing.tm2_computable {α β : Type} :
(α → β)Type 1
• to_tm2_computable_aux :
• outputs_fun : Π (a : α),

A Turing machine + a proof it outputs f.

structure turing.tm2_computable_in_time {α β : Type} :
(α → β)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} :
(α → β)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 : α → β} :
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
def turing.id_computer {α : Type} :

A Turing machine computing the identity on α.

Equations
@[instance]

Equations

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

Equations
@[instance]

Equations
@[instance]
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
@[instance]
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
@[instance]

Equations

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

Equations
@[instance]

Equations
def turing.id_computable {α : Type} (ea : computability.fin_encoding α) :

A proof that the identity map on α is computable.

Equations
@[instance]

Equations
@[instance]

Equations