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.

Instances For
    structure Computability.FinEncoding (α : Type u) extends Computability.Encoding :
    Type (max 1 u)

    An encoding plus a guarantee of finiteness of the alphabet.

    Instances For

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

      Instances For

        The natural inclusion of bool in Γ'.

        Instances For

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

          Instances For

            An encoding function of the binary numbers in bool.

            Instances For

              An encoding function of ℕ in bool.

              Instances For

                A decoding function from List Bool to the binary numbers.

                Instances For

                  A decoding function from List Bool to ℕ.

                  Instances For

                    A binary encoding of ℕ in bool.

                    Instances For

                      A binary fin_encoding of ℕ in bool.

                      Instances For

                        A binary encoding of ℕ in Γ'.

                        Instances For

                          A binary fin_encoding of ℕ in Γ'.

                          Instances For

                            A unary decoding function from List Bool to ℕ.

                            Instances For

                              A unary fin_encoding of ℕ.

                              Instances For

                                An encoding function of bool in bool.

                                Instances For

                                  A decoding function from List Bool to bool.

                                  Instances For

                                    A fin_encoding of bool in bool.

                                    Instances For