mathlib documentation

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 #

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.

Instances for turing.fin_tm2
def turing.fin_tm2.stmt (tm : turing.fin_tm2) :
Type

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

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

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

Equations
Instances for turing.fin_tm2.cfg
@[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 : σ → option σ) (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.

Instances for turing.evals_to
structure turing.evals_to_in_time {σ : Type u_1} (f : σ → option σ) (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.

Instances for turing.evals_to_in_time
def turing.evals_to.refl {σ : Type u_1} (f : σ → option σ) (a : σ) :

Reflexivity of evals_to in 0 steps.

Equations
def turing.evals_to.trans {σ : Type u_1} (f : σ → option σ) (a b : σ) (c : option σ) (h₁ : turing.evals_to f a b) (h₂ : turing.evals_to f b 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 : σ → option σ) (a : σ) :

Reflexivity of evals_to_in_time in 0 steps.

Equations
def turing.evals_to_in_time.trans {σ : Type u_1} (f : σ → option σ) (m₁ m₂ : ) (a b : σ) (c : option σ) (h₁ : turing.evals_to_in_time f a b m₁) (h₂ : turing.evals_to_in_time f b c m₂) :
turing.evals_to_in_time f a c (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
Instances for turing.tm2_outputs
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
Instances for turing.tm2_outputs_in_time
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 : turing.tm2_outputs_in_time tm l l' m) :

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 Γ₁.

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

A Turing machine + a proof it outputs f.

Instances for turing.tm2_computable
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.

Instances for turing.tm2_computable_in_time
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.

Instances for turing.tm2_computable_in_poly_time

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

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

Equations
@[protected, instance]
noncomputable def turing.inhabited_tm2_outputs  :
inhabited (turing.tm2_outputs (turing.id_computer computability.fin_encoding_bool_bool) (list.map (equiv.cast turing.inhabited_tm2_outputs._proof_1).inv_fun [bool.ff]) (option.some (list.map (equiv.cast turing.inhabited_tm2_outputs._proof_2).inv_fun [bool.ff])))
Equations

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

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

A proof that the identity map on α is computable.

Equations