mathlib documentation

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 → Type 1

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

structure computability.fin_encoding  :
Type → Type 1

An encoding plus a guarantee of finiteness of the alphabet.

inductive computability.Γ'  :
Type

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

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