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
        Instances For
          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 [] }
          Instances For
            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 [] }
            Instances For
              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
                  Instances For
                    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
                    Instances For
                      def Turing.EvalsToInTime.refl {σ : Type u_1} (f : σOption σ) (a : σ) :

                      Reflexivity of EvalsToInTime in 0 steps.

                      Equations
                      Instances For
                        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
                        Instances For
                          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
                              Instances For
                                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 }
                                        Instances For

                                          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 }
                                          Instances For

                                            A Turing machine computing the identity on α.

                                            Equations
                                            Instances For

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

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

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

                                                Equations
                                                Instances For

                                                  A proof that the identity map on α is computable.

                                                  Equations
                                                  Instances For