Documentation

Mathlib.Computability.TMComputable

Computable functions #

This file contains the definition of a Turing machine with some finiteness conditions (bundling the definition of TM2 in TuringMachine.lean), a definition of when a TM gives a certain output (in a certain time), and the definition of computability (in polynomial time 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, and 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.FinTM2 :

A bundled TM2 (an equivalent of the classical Turing machine, defined starting from the namespace Turing.TM2 in TuringMachine.lean), with an input and output stack, a main function, an initial state and some finiteness guarantees.

  • K : Type

    index type of stacks

  • kDecidableEq : DecidableEq self.K
  • kFin : Fintype self.K

    A TM2 machine has finitely many stacks.

  • k₀ : self.K

    input resp. output stack

  • k₁ : self.K

    input resp. output stack

  • Γ : self.KType

    type of stack elements

  • Λ : Type

    type of function labels

  • main : self

    a main function: the initial function that is executed, given by its label

  • ΛFin : Fintype self

    A TM2 machine has finitely many function labels.

  • σ : Type

    type of states of the machine

  • initialState : self

    the initial state of the machine

  • σFin : Fintype self

    a TM2 machine has finitely many internal states.

  • Γk₀Fin : Fintype (self self.k₀)

    Each internal stack is finite.

  • m : selfTuring.TM2.Stmt self self self

    the program itself, i.e. one function for every function label

Instances For
Equations
  • tm.decidableEqK = tm.kDecidableEq
Equations
  • tm.inhabitedσ = { default := tm.initialState }

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

Equations
Instances For
Equations

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

Equations
Instances For
Equations
def Turing.FinTM2.step (tm : Turing.FinTM2) :
tm.CfgOption tm.Cfg

The step function corresponding to this TM.

Equations
def Turing.initList (tm : Turing.FinTM2) (s : List (tm tm.k₀)) :
tm.Cfg

The initial configuration corresponding to a list in the input alphabet.

Equations
  • Turing.initList tm s = { l := some tm.main, var := tm.initialState, stk := fun (k : tm.K) => if h : k = tm.k₀ then .mpr s else [] }
def Turing.haltList (tm : Turing.FinTM2) (s : List (tm tm.k₁)) :
tm.Cfg

The final configuration corresponding to a list in the output alphabet.

Equations
  • Turing.haltList tm s = { l := none, var := tm.initialState, stk := fun (k : tm.K) => if h : k = tm.k₁ then .mpr s else [] }
structure Turing.EvalsTo {σ : Type u_1} (f : σOption σ) (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.

  • steps :

    number of steps taken

  • evals_in_steps : (flip bind f)^[self.steps] (some a) = b
Instances For
theorem Turing.EvalsTo.evals_in_steps {σ : Type u_1} {f : σOption σ} {a : σ} {b : Option σ} (self : Turing.EvalsTo f a b) :
(flip bind f)^[self.steps] (some a) = b
structure Turing.EvalsToInTime {σ : Type u_1} (f : σOption σ) (a : σ) (b : Option σ) (m : ) extends Turing.EvalsTo :

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.

  • steps :
  • evals_in_steps : (flip bind f)^[self.steps] (some a) = b
  • steps_le_m : self.steps m
Instances For
theorem Turing.EvalsToInTime.steps_le_m {σ : Type u_1} {f : σOption σ} {a : σ} {b : Option σ} {m : } (self : Turing.EvalsToInTime f a b m) :
self.steps m
def Turing.EvalsTo.refl {σ : Type u_1} (f : σOption σ) (a : σ) :

Reflexivity of EvalsTo in 0 steps.

Equations
def Turing.EvalsTo.trans {σ : Type u_1} (f : σOption σ) (a : σ) (b : σ) (c : Option σ) (h₁ : Turing.EvalsTo f a (some b)) (h₂ : Turing.EvalsTo f b c) :

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

Equations
def Turing.EvalsToInTime.refl {σ : Type u_1} (f : σOption σ) (a : σ) :

Reflexivity of EvalsToInTime in 0 steps.

Equations
def Turing.EvalsToInTime.trans {σ : Type u_1} (f : σOption σ) (m₁ : ) (m₂ : ) (a : σ) (b : σ) (c : Option σ) (h₁ : Turing.EvalsToInTime f a (some b) m₁) (h₂ : Turing.EvalsToInTime f b c m₂) :
Turing.EvalsToInTime f a c (m₂ + m₁)

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

Equations
def Turing.TM2Outputs (tm : Turing.FinTM2) (l : List (tm tm.k₀)) (l' : Option (List (tm tm.k₁))) :

A proof of tm outputting l' when given l.

Equations
Instances For
def Turing.TM2OutputsInTime (tm : Turing.FinTM2) (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
Instances For
def Turing.TM2OutputsInTime.toTM2Outputs {tm : Turing.FinTM2} {l : List (tm tm.k₀)} {l' : Option (List (tm tm.k₁))} {m : } (h : Turing.TM2OutputsInTime tm l l' m) :

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

Equations
  • h.toTM2Outputs = h.toEvalsTo
structure Turing.TM2ComputableAux (Γ₀ : Type) (Γ₁ : Type) :

A (bundled TM2) Turing machine with input alphabet equivalent to Γ₀ and output alphabet equivalent to Γ₁.

  • the underlying bundled TM2

  • inputAlphabet : self.tm self.tm.k₀ Γ₀

    the input alphabet is equivalent to Γ₀

  • outputAlphabet : self.tm self.tm.k₁ Γ₁

    the output alphabet is equivalent to Γ₁

Instances For
structure Turing.TM2Computable {α : Type} {β : Type} (ea : Computability.FinEncoding α) (eb : Computability.FinEncoding β) (f : αβ) extends Turing.TM2ComputableAux :

A Turing machine + a proof it outputs f.

  • inputAlphabet : self.tm self.tm.k₀ ea
  • outputAlphabet : self.tm self.tm.k₁ eb
  • outputsFun : (a : α) → Turing.TM2Outputs self.tm (List.map self.inputAlphabet.invFun (ea.encode a)) (some (List.map self.outputAlphabet.invFun (eb.encode (f a))))

    a proof this machine outputs f

Instances For
structure Turing.TM2ComputableInTime {α : Type} {β : Type} (ea : Computability.FinEncoding α) (eb : Computability.FinEncoding β) (f : αβ) extends Turing.TM2ComputableAux :

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

  • inputAlphabet : self.tm self.tm.k₀ ea
  • outputAlphabet : self.tm self.tm.k₁ eb
  • time :

    a time function

  • outputsFun : (a : α) → Turing.TM2OutputsInTime self.tm (List.map self.inputAlphabet.invFun (ea.encode a)) (some (List.map self.outputAlphabet.invFun (eb.encode (f a)))) (self.time (ea.encode a).length)

    proof this machine outputs f in at most time(input.length) steps

Instances For
structure Turing.TM2ComputableInPolyTime {α : Type} {β : Type} (ea : Computability.FinEncoding α) (eb : Computability.FinEncoding β) (f : αβ) extends Turing.TM2ComputableAux :

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

  • inputAlphabet : self.tm self.tm.k₀ ea
  • outputAlphabet : self.tm self.tm.k₁ eb
  • a polynomial time function

  • outputsFun : (a : α) → Turing.TM2OutputsInTime self.tm (List.map self.inputAlphabet.invFun (ea.encode a)) (some (List.map self.outputAlphabet.invFun (eb.encode (f a)))) (Polynomial.eval (ea.encode a).length self.time)

    proof that this machine outputs f in at most time(input.length) steps

Instances For

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

Equations
  • h.toTM2Computable = { toTM2ComputableAux := h.toTM2ComputableAux, outputsFun := fun (a : α) => (h.outputsFun a).toTM2Outputs }

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

Equations
  • h.toTM2ComputableInTime = { toTM2ComputableAux := h.toTM2ComputableAux, time := fun (n : ) => Polynomial.eval n h.time, outputsFun := h.outputsFun }

A Turing machine computing the identity on α.

Equations

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

Equations
  • One or more equations did not get rendered due to their size.

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

Equations

A proof that the identity map on α is computable.

Equations