Documentation

CslibFrontier.Computability.Machines.Turing.MultiTape.Universal.PolyTime

Universal input coding and polynomial-time simulation #

The universal function Turing.MultiTapeTM.Universal.universal runs a described machine on an input for a given number of steps. Its time and space are polynomial in the length of the description, of the input and of the number of steps written in unary (Turing.MultiTapeTM.Universal.universal_bounds_unary), so it is tidily computable in polynomial time when the number of steps is written in unary (Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_universal). Written in binary, the number of steps would be exponential in its length.

The input-coding API translates bits to unary symbols (false ↦ 0, true ↦ 1) in linear time and output size. It also certifies polynomial-time decoding of descriptions and coding of a single bit, independently of hierarchy theorems and Ladner's language.

Main definitions #

Main results #

References #

The symbols of the input #

source
def Turing.MultiTapeTM.Universal.trueDoubled (b : Bool) :
List Bool

The code of a bit list with every true doubled: false ↦ [false], true ↦ [true, true].

Instances For
    source
    def Turing.MultiTapeTM.Universal.encTrueDoubled :
    List Bool ↪ List Bool

    Bit lists with every true doubled.

    Instances For
      source
      def Turing.MultiTapeTM.Universal.trueDoubleT :
      Transducer Bool Unit

      Doubles every true.

      Instances For
        source
        def Turing.MultiTapeTM.Universal.symbolsT :
        Transducer Bool Bool

        Reads a doubled word as the framed unary symbols 0 for false and 1 for true.

        Instances For
          source
          theorem Turing.MultiTapeTM.Universal.trueDoubleT_run (x : List Bool) :
          trueDoubleT.run () x = encTrueDoubled x
          source
          theorem Turing.MultiTapeTM.Universal.symbolsT_run (x : List Bool) :
          symbolsT.run false (encTrueDoubled x) = (encList encUnary) (List.map (⇑eBit) x)
          source
          theorem Turing.MultiTapeTM.Universal.computableTidilyInDegree_map_eBit :
          ComputableTidilyInDegree (fun (x : List Bool) => List.map (⇑eBit) x) encBits (encList encUnary) 1 1

          The input as symbols, in linear time and space.

          source
          theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_map_eBit :
          ComputableTidilyInPolyTime (fun (w : List Bool) => List.map (⇑eBit) w) encBits (encList encUnary)

          The input of a machine as symbols is linear.

          source
          theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_eBit :
          ComputableTidilyInPolyTime (fun (b : Bool) => eBit b) encBool encUnary

          The coding of bits as symbols is a finite computation.

          Simulation with a unary clock #

          source
          @[reducible, inline]
          abbrev Turing.MultiTapeTM.Universal.eInUnary :
          Desc × List ℕ × ℕ ↪ List Bool

          The encoding of inputs of the universal function with the number of steps in unary: the framed description, then the framed list of unary input symbols, then the step count in unary. It differs from eIn only in its last component, which eIn writes in binary.

          Instances For
            source
            theorem Turing.MultiTapeTM.Universal.universal_bounds_unary (i : Desc × List ℕ × ℕ) :
            (i.2.2 + 1) * (stepBound (descLen i.1) ((encList encUnary) i.2.1).length i.2.2 + runBound (descLen i.1) ((encList encUnary) i.2.1).length i.2.2 + ((encNat i.2.2).length + 1) ^ 2) + ((eIn i).length + 1) ^ 2 ≤ 100025 * ((eInUnary i).length + 1) ^ 6 ∧ runBound (descLen i.1) ((encList encUnary) i.2.1).length i.2.2 + (eIn i).length ≤ 205 * ((eInUnary i).length + 1) ^ 3

            The time and space of the universal function, polynomially in the length of its input with the number of steps in unary.

            source
            theorem Turing.MultiTapeTM.Universal.computableTidilyInPolyTime_universal :
            ComputableTidilyInPolyTime universal eInUnary eOut

            The universal function with a unary clock is polynomial-time: written in unary, the number of steps counts towards the length of the input.

            Plain ComputableInPolyTime wrappers for the universal simulator #

            source
            theorem Turing.MultiTapeTM.Universal.computableInPolyTime_decodeDesc :
            ComputableInPolyTime decodeDesc encBits eDesc

            Plain polynomial-time certificate for decodeDesc.

            source
            theorem Turing.MultiTapeTM.Universal.computableInO_map_eBit :
            ComputableInO (fun (w : List Bool) => List.map (⇑eBit) w) encBits (encList encUnary) (fun (w : List Bool) => (encBits w).length) fun (w : List Bool) => (encBits w).length

            Plain linear certificate for coding a bit string as unary symbol numbers.

            source
            theorem Turing.MultiTapeTM.Universal.computableInPolyTime_map_eBit :
            ComputableInPolyTime (fun (w : List Bool) => List.map (⇑eBit) w) encBits (encList encUnary)

            Plain polynomial-time certificate for coding a bit string as unary symbol numbers.

            source
            theorem Turing.MultiTapeTM.Universal.computableInPolyTime_eBit :
            ComputableInPolyTime (fun (b : Bool) => eBit b) encBool encUnary

            Plain polynomial-time certificate for coding a single bit as a unary symbol number.

            source
            theorem Turing.MultiTapeTM.Universal.computableInPolyTime_map_ne_zero :
            ComputableInPolyTime (fun (l : List ℕ) => List.map (fun (x : ℕ) => x != 0) l) (encList encUnary) encBits

            Decoding a list of unary symbol numbers to bits via (· != 0) is computable in polynomial time.

            source
            theorem Turing.MultiTapeTM.Universal.computableInPolyTime_universal :
            ComputableInPolyTime universal eInUnary eOut

            Plain polynomial-time certificate for the universal simulator with a unary step budget.