# mathlibdocumentation

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 #

• fin_encoding_nat_bool : a binary encoding of ℕ in a simple alphabet.
• fin_encoding_nat_Γ' : a binary encoding of ℕ in the alphabet used for TM's.
• unary_fin_encoding_nat : a unary encoding of ℕ
• fin_encoding_bool_bool : an encoding of bool.
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.

@[instance]
inductive computability.Γ'  :
Type

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

@[instance]
@[instance]
Equations

The natural inclusion of bool in Γ'.

Equations

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

Equations

An encoding function of the positive binary numbers in bool.

Equations

An encoding function of the binary numbers in bool.

Equations

An encoding function of ℕ in bool.

Equations

A decoding function from list bool to the positive binary numbers.

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 binary fin_encoding of ℕ in bool.

Equations

A binary encoding of ℕ in Γ'.

Equations

A binary fin_encoding of ℕ in Γ'.

Equations

A unary encoding function of ℕ in bool.

Equations

A unary decoding function from list bool to ℕ.

Equations

A unary fin_encoding of ℕ.

Equations

An encoding function of bool in bool.

Equations

A decoding function from list bool to bool.

Equations

A fin_encoding of bool in bool.

Equations
@[instance]
Equations
@[instance]
Equations