Documentation

Complexity.Computability.Machines.Turing.MultiTape.Universal.Decode

Decoding descriptions of machines #

Every word decodes to a description of a machine (Turing.MultiTapeTM.Universal.descDecoder): the decoder inverts the encoding Turing.MultiTapeTM.Universal.eDesc of descriptions, returns a description of polynomial encoded length on every other word, and is tidily computable within bounds of fixed degrees. It is assembled from the generic decoders of Complexity.Computability.Machines.Turing.MultiTape.Encodings.Decoder along the fields of a description, its transitions, their keys and their actions.

A description framed at the start of a word is recovered whatever follows it (Turing.MultiTapeTM.Universal.decodeDesc_unframe_frame_append), so a description can be padded to any length.

Main definitions #

Main results #

source
def Turing.MultiTapeTM.Universal.signOf (q : Bool × Bool) :
SignType

The sign read from a word: zero if it is empty (q.1), and otherwise positive or negative as its head (q.2) is true or false.

Instances For
    source
    def Turing.MultiTapeTM.Universal.signDecoder :
    Decoder encSign

    Moves are decoded from the head of the word.

    Instances For
      source
      def Turing.MultiTapeTM.Universal.symDecoder :
      Decoder eSym

      Symbols and blanks.

      Instances For
        source
        def Turing.MultiTapeTM.Universal.keyDecoder :
        Decoder eKey

        Keys of transitions, from their fields.

        Instances For
          source
          def Turing.MultiTapeTM.Universal.tapeActDecoder :
          Decoder eTA

          Actions on a work tape.

          Instances For
            source
            def Turing.MultiTapeTM.Universal.actDecoder :
            Decoder eAct

            Actions, from their fields.

            Instances For
              source
              def Turing.MultiTapeTM.Universal.descDecoder :
              Decoder eDesc

              The decoder of descriptions.

              Instances For
                source
                def Turing.MultiTapeTM.Universal.decodeDesc (w : List Bool) :
                Desc

                The description decoded from a word.

                Instances For
                  source
                  theorem Turing.MultiTapeTM.Universal.decodeDesc_eDesc (d : Desc) :
                  decodeDesc (eDesc d) = d

                  Decoding inverts the encoding of descriptions.

                  source
                  theorem Turing.MultiTapeTM.Universal.decodeDesc_unframe_frame_append (d : Desc) (pad : List Bool) :
                  decodeDesc (unframe (frame (eDesc d) ++ pad)) = d

                  Padded descriptions. A description framed at the start of a word is decoded from the framed word, whatever follows it.

                  source
                  theorem Turing.MultiTapeTM.Universal.exists_computableTidilyInDegree_decodeDesc :
                  ∃ (d : ℕ) (e : ℕ), ComputableTidilyInDegree decodeDesc encBits eDesc d e

                  Decoding is efficient. It is tidily computable, and the decoded descriptions have encoded length polynomial in the length of the word, within bounds of fixed degrees.