# 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 #

• finEncodingNatBool : a binary encoding of ℕ in a simple alphabet.
• finEncodingNatΓ' : a binary encoding of ℕ in the alphabet used for TM's.
• unaryFinEncodingNat : a unary encoding of ℕ
• finEncodingBoolBool : an encoding of bool.
structure Computability.Encoding (α : Type u) :
Type (max u (v + 1))
• Γ : Type v
• encode : αList s
• decode : List s
• decode_encode : ∀ (x : α),

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

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

An encoding plus a guarantee of finiteness of the alphabet.

Instances For
instance Computability.Γ.fintype {α : Type u} (e : ) :
Fintype e

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 positive binary numbers in bool.

Equations
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 positive binary numbers.

Equations
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 encoding function of ℕ in bool.

Equations
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