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 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.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.

Instances For

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

    Instances For

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

      Instances For

        The step function corresponding to this TM.

        Instances For

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

          Instances For

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

            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.

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

                Instances For
                  def Turing.EvalsTo.refl {σ : Type u_1} (f : σOption σ) (a : σ) :

                  Reflexivity of EvalsTo in 0 steps.

                  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.

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

                      Reflexivity of EvalsToInTime in 0 steps.

                      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.

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

                          A proof of tm outputting l' when given l.

                          Instances For
                            def Turing.TM2OutputsInTime (tm : Turing.FinTM2) (l : List (Turing.FinTM2.Γ tm tm.k₀)) (l' : Option (List (Turing.FinTM2.Γ tm tm.k₁))) (m : ) :

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

                            Instances For
                              def Turing.TM2OutputsInTime.toTM2Outputs {tm : Turing.FinTM2} {l : List (Turing.FinTM2.Γ tm tm.k₀)} {l' : Option (List (Turing.FinTM2.Γ tm tm.k₁))} {m : } (h : Turing.TM2OutputsInTime tm l l' m) :

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

                              Instances For
                                structure Turing.TM2ComputableAux (Γ₀ : Type) (Γ₁ : Type) :

                                A Turing machine with input alphabet equivalent to Γ₀ and output alphabet 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.

                                  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(len(input)) 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(len(input)) steps.

                                      Instances For

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

                                        Instances For

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

                                          Instances For

                                            A Turing machine computing the identity on α.

                                            Instances For

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

                                              Instances For

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

                                                Instances For

                                                  A proof that the identity map on α is computable.

                                                  Instances For