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

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

K : Type
K_decidable_eq : decidable_eq c.K
K_fin : fintype c.K
k₀ : c.K
k₁ : c.K
Γ : c.K → Type
Λ : Type
main : c.Λ
Λ_fin : fintype c.Λ
σ : Type
initial_state : c.σ
σ_fin : fintype c.σ
Γk₀_fin : fintype (c.Γ c.k₀)
M : c.Λ → turing.TM2.stmt c.Γ c.Λ c.σ

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]

def turing.fin_tm2.decidable_eq (tm : turing.fin_tm2) :

decidable_eq tm.K

Equations

tm.decidable_eq = tm.K_decidable_eq

@[instance]

def turing.fin_tm2.inhabited (tm : turing.fin_tm2) :

inhabited tm.σ

Equations

tm.inhabited = {default := tm.initial_state}

def turing.fin_tm2.stmt (tm : turing.fin_tm2) :

Type

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

Equations

tm.stmt = turing.TM2.stmt tm.Γ tm.Λ tm.σ

@[instance]

def turing.fin_tm2.stmt.inhabited (tm : turing.fin_tm2) :

inhabited tm.stmt

def turing.fin_tm2.cfg (tm : turing.fin_tm2) :

Type

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

Equations

tm.cfg = turing.TM2.cfg tm.Γ tm.Λ tm.σ

@[instance]

def turing.fin_tm2.inhabited_cfg (tm : turing.fin_tm2) :

inhabited tm.cfg

Equations

tm.inhabited_cfg = turing.TM2.cfg.inhabited tm.Γ tm.Λ tm.σ

@[simp]

def turing.fin_tm2.step (tm : turing.fin_tm2) (a : tm.cfg) :

The step function corresponding to this TM.

Equations

tm.step = turing.TM2.step tm.M

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

turing.init_list tm s = {l := some tm.main, var := tm.initial_state, stk := λ (k : tm.K), dite (k = tm.k₀) (λ (h : k = tm.k₀), _.mpr s) (λ (_x : ¬k = tm.k₀), list.nil)}

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

turing.halt_list tm s = {l := none tm.Λ, var := tm.initial_state, stk := λ (k : tm.K), dite (k = tm.k₁) (λ (h : k = tm.k₁), _.mpr s) (λ (_x : ¬k = tm.k₁), list.nil)}

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

Type

steps : ℕ
evals_in_steps : flip bind f^[c.steps ] ↑a = b

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

Type

to_evals_to : turing.evals_to f a b
steps_le_m : c.to_evals_to.steps ≤ 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 : σ → option σ) (a : σ) :

turing.evals_to f a ↑a

Reflexivity of evals_to in 0 steps.

Equations

turing.evals_to.refl f a = {steps := 0, evals_in_steps := _}

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

turing.evals_to f a c

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

Equations

turing.evals_to.trans f a b c h₁ h₂ = {steps := h₂.steps + h₁.steps, evals_in_steps := _}

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

turing.evals_to_in_time f a ↑a 0

Reflexivity of evals_to_in_time in 0 steps.

Equations

turing.evals_to_in_time.refl f a = {to_evals_to := turing.evals_to.refl f a, steps_le_m := _}

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

turing.evals_to_in_time.trans f a b c m₁ m₂ h₁ h₂ = {to_evals_to := turing.evals_to.trans f a b c h₁.to_evals_to h₂.to_evals_to, steps_le_m := _}

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

turing.tm2_outputs tm l l' = turing.evals_to tm.step (turing.init_list tm l) (option.map (turing.halt_list tm) 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

turing.tm2_outputs_in_time tm l l' m = turing.evals_to_in_time tm.step (turing.init_list tm l) (option.map (turing.halt_list tm) 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 : turing.tm2_outputs_in_time tm l l' m) :

turing.tm2_outputs tm l l'

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

Equations

h.to_tm2_outputs = h.to_evals_to

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

Type 1

tm : turing.fin_tm2
input_alphabet : c.tm.Γ c.tm.k₀ ≃ Γ₀
output_alphabet : c.tm.Γ c.tm.k₁ ≃ Γ₁

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

to_tm2_computable_aux : turing.tm2_computable_aux ea.to_encoding.Γ eb.to_encoding.Γ
outputs_fun : Π (a : α), turing.tm2_outputs c.to_tm2_computable_aux.tm (list.map c.to_tm2_computable_aux.input_alphabet.inv_fun (ea.to_encoding.encode a)) (some (list.map c.to_tm2_computable_aux.output_alphabet.inv_fun (eb.to_encoding.encode (f a))))

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

to_tm2_computable_aux : turing.tm2_computable_aux ea.to_encoding.Γ eb.to_encoding.Γ
time : ℕ → ℕ
outputs_fun : Π (a : α), turing.tm2_outputs_in_time c.to_tm2_computable_aux.tm (list.map c.to_tm2_computable_aux.input_alphabet.inv_fun (ea.to_encoding.encode a)) (some (list.map c.to_tm2_computable_aux.output_alphabet.inv_fun (eb.to_encoding.encode (f a)))) (c.time (ea.to_encoding.encode a).length)

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

to_tm2_computable_aux : turing.tm2_computable_aux ea.to_encoding.Γ eb.to_encoding.Γ
time : polynomial ℕ
outputs_fun : Π (a : α), turing.tm2_outputs_in_time c.to_tm2_computable_aux.tm (list.map c.to_tm2_computable_aux.input_alphabet.inv_fun (ea.to_encoding.encode a)) (some (list.map c.to_tm2_computable_aux.output_alphabet.inv_fun (eb.to_encoding.encode (f a)))) (polynomial.eval (ea.to_encoding.encode a).length c.time)

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 : turing.tm2_computable_in_time ea eb f) :

turing.tm2_computable ea eb f

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

Equations

h.to_tm2_computable = {to_tm2_computable_aux := h.to_tm2_computable_aux, outputs_fun := λ (a : α), (h.outputs_fun a).to_tm2_outputs}

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

turing.tm2_computable_in_time ea eb f

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

Equations

h.to_tm2_computable_in_time = {to_tm2_computable_aux := h.to_tm2_computable_aux, time := λ (n : ℕ), polynomial.eval n h.time, outputs_fun := h.outputs_fun}

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

A Turing machine computing the identity on α.

Equations

turing.id_computer ea = {K := unit, K_decidable_eq := λ (a b : unit), punit.decidable_eq a b, K_fin := punit.fintype, k₀ := punit.star, k₁ := punit.star, Γ := λ (_x : unit), ea.to_encoding.Γ, Λ := unit, main := punit.star, Λ_fin := punit.fintype, σ := unit, initial_state := punit.star, σ_fin := punit.fintype, Γk₀_fin := ea.Γ_fin, M := λ (_x : unit), turing.TM2.stmt.halt}

@[instance]

def turing.inhabited_fin_tm2 :

inhabited turing.fin_tm2

Equations

turing.inhabited_fin_tm2 = {default := turing.id_computer (default (computability.fin_encoding bool))}

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

turing.tm2_computable_in_poly_time ea ea id

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

Equations

turing.id_computable_in_poly_time ea = {to_tm2_computable_aux := {tm := turing.id_computer ea, input_alphabet := equiv.cast _, output_alphabet := equiv.cast _}, time := 1, outputs_fun := λ (_x : α), {to_evals_to := {steps := 1, evals_in_steps := _}, steps_le_m := _}}

@[instance]

def turing.inhabited_tm2_computable_in_poly_time :

inhabited (turing.tm2_computable_in_poly_time (default (computability.fin_encoding bool)) (default (computability.fin_encoding bool)) id)

Equations

turing.inhabited_tm2_computable_in_poly_time = {default := turing.id_computable_in_poly_time (default (computability.fin_encoding bool))}

@[instance]

def turing.inhabited_tm2_outputs_in_time :

inhabited (turing.tm2_outputs_in_time (turing.id_computer computability.fin_encoding_bool_bool) (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])) (polynomial.eval (computability.fin_encoding_bool_bool.to_encoding.encode ff).length (turing.id_computable_in_poly_time computability.fin_encoding_bool_bool).time))

Equations

turing.inhabited_tm2_outputs_in_time = {default := (turing.id_computable_in_poly_time computability.fin_encoding_bool_bool).outputs_fun ff}

@[instance]

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 [ff]) (some (list.map (equiv.cast turing.inhabited_tm2_outputs._proof_2).inv_fun [ff])))

Equations

turing.inhabited_tm2_outputs = {default := (default (turing.tm2_outputs_in_time (turing.id_computer computability.fin_encoding_bool_bool) (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])) (polynomial.eval (computability.fin_encoding_bool_bool.to_encoding.encode ff).length (turing.id_computable_in_poly_time computability.fin_encoding_bool_bool).time))).to_tm2_outputs}

@[instance]

def turing.inhabited_evals_to_in_time :

inhabited (turing.evals_to_in_time (λ (_x : unit), some punit.star) punit.star (some punit.star) 0)

Equations

turing.inhabited_evals_to_in_time = {default := turing.evals_to_in_time.refl (λ (_x : unit), some punit.star) punit.star}

@[instance]

def turing.inhabited_tm2_evals_to :

inhabited (turing.evals_to (λ (_x : unit), some punit.star) punit.star (some punit.star))

Equations

turing.inhabited_tm2_evals_to = {default := turing.evals_to.refl (λ (_x : unit), some punit.star) punit.star}

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

turing.tm2_computable_in_time ea ea id

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

Equations

turing.id_computable_in_time ea = (turing.id_computable_in_poly_time ea).to_tm2_computable_in_time

@[instance]

def turing.inhabited_tm2_computable_in_time :

inhabited (turing.tm2_computable_in_time computability.fin_encoding_bool_bool computability.fin_encoding_bool_bool id)

Equations

turing.inhabited_tm2_computable_in_time = {default := turing.id_computable_in_time (default (computability.fin_encoding bool))}

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

turing.tm2_computable ea ea id

A proof that the identity map on α is computable.

Equations

turing.id_computable ea = (turing.id_computable_in_time ea).to_tm2_computable

@[instance]

def turing.inhabited_tm2_computable :

inhabited (turing.tm2_computable computability.fin_encoding_bool_bool computability.fin_encoding_bool_bool id)

Equations

turing.inhabited_tm2_computable = {default := turing.id_computable (default (computability.fin_encoding bool))}

@[instance]

def turing.inhabited_tm2_computable_aux :

inhabited (turing.tm2_computable_aux bool bool)

Equations

turing.inhabited_tm2_computable_aux = {default := (default (turing.tm2_computable computability.fin_encoding_bool_bool computability.fin_encoding_bool_bool id)).to_tm2_computable_aux}