Documentation

Mathlib.Computability.Encoding

Encodings #

This file contains the definition of a (finite) encoding, a map from a type to strings in an alphabet, used in defining computability by Turing machines. It also contains several examples:

Examples #

structure Computability.Encoding (α : Type u) :
Type (max u (v + 1))

An encoding of a type in a certain alphabet, together with a decoding.

  • Γ : Type v
  • encode : αList self
  • decode : List selfOption α
  • decode_encode : ∀ (x : α), self.decode (self.encode x) = some x
Instances For
    structure Computability.FinEncoding (α : Type u) extends Computability.Encoding :
    Type (max 1 u)

    An encoding plus a guarantee of finiteness of the alphabet.

    • Γ : Type
    • encode : αList self
    • decode : List selfOption α
    • decode_encode : ∀ (x : α), self.toEncoding.decode (self.toEncoding.encode x) = some x
    • ΓFin : Fintype self
    Instances For

      A standard Turing machine alphabet, consisting of blank,bit0,bit1,bra,ket,comma.

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

        An arbitrary section of the natural inclusion of bool in Γ'.

        Equations
        Instances For

          An encoding function of the binary numbers in bool.

          Equations
          Instances For

            An encoding function of ℕ in bool.

            Equations
            Instances For

              A decoding function from List Bool to the binary numbers.

              Equations
              Instances For

                A decoding function from List Bool to ℕ.

                Equations
                Instances For

                  A binary encoding of ℕ in bool.

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

                    A binary fin_encoding of ℕ in bool.

                    Equations
                    Instances For

                      A binary encoding of ℕ in Γ'.

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

                        A unary decoding function from List Bool to ℕ.

                        Equations
                        Instances For

                          A unary fin_encoding of ℕ.

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

                            An encoding function of bool in bool.

                            Equations
                            Instances For

                              A decoding function from List Bool to bool.

                              Equations
                              Instances For

                                A fin_encoding of bool in bool.

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