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.

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

Equations

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

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

Reflexivity of evals_to in 0 steps.

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

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 σ) (a b : σ) (c : option σ) (m₁ m₂ : ) :
turing.evals_to_in_time f a b m₁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) :
list (tm.Γ tm.k₀)option (list (tm.Γ tm.k₁)) → Type

A proof of tm outputting l' when given l.

Equations
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
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 : } :

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} :
computability.fin_encoding αcomputability.fin_encoding β(α → β)Type 1

A Turing machine + a proof it outputs f.

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

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

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

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

Equations

A proof that the identity map on α is computable.

Equations