mathlib3 documentation

computability.encoding

Encodings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 computability.encoding
structure computability.fin_encoding (α : Type u) :
Type (max 1 u)

An encoding plus a guarantee of finiteness of the alphabet.

Instances for computability.fin_encoding
@[protected, instance]
Equations
inductive computability.Γ'  :

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

Instances for computability.Γ'

An encoding function of ℕ in bool.

Equations

A decoding function from list bool to the binary numbers.

Equations

A decoding function from list bool to ℕ.

Equations

A binary encoding of ℕ in bool.

Equations

A unary decoding function from list bool to ℕ.

Equations

An encoding function of bool in bool.

Equations