mathlib3documentation

computability.tm_computable

Computable functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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  :

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

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

Equations
Instances for turing.fin_tm2.stmt
@[protected, instance]

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

Equations
Instances for turing.fin_tm2.cfg
@[protected, instance]
Equations
@[simp]

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 σ) :

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 : σ ) (a : σ) (b : option σ) (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.

Instances for turing.evals_to_in_time
@[refl]
def turing.evals_to.refl {σ : Type u_1} (f : σ ) (a : σ) :
a

Reflexivity of evals_to in 0 steps.

Equations
@[trans]
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
@[refl]
def turing.evals_to_in_time.refl {σ : Type u_1} (f : σ ) (a : σ) :
0

Reflexivity of evals_to_in_time in 0 steps.

Equations
@[trans]
def turing.evals_to_in_time.trans {σ : Type u_1} (f : σ ) (m₁ m₂ : ) (a b : σ) (c : option σ) (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₁))) :

A proof of tm outputting l' when given l.

Equations
• l' = l) l')
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 : ) :

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

Equations
• l' m = l) l') m
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 : l' m) :
l'

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

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

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 : α β) :

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 : α β) :

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

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
@[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 [bool.ff]) (option.some (list.map (equiv.cast turing.inhabited_tm2_outputs_in_time._proof_2).inv_fun [bool.ff]))
Equations
@[protected, instance]
noncomputable def turing.inhabited_tm2_outputs  :
inhabited (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
@[protected, instance]
def turing.inhabited_evals_to_in_time  :
inhabited (turing.evals_to_in_time (λ (_x : unit), option.some punit.star) punit.star (option.some punit.star) 0)
Equations
@[protected, instance]
def turing.inhabited_tm2_evals_to  :
inhabited (turing.evals_to (λ (_x : unit), option.some punit.star) punit.star (option.some punit.star))
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