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

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

• Γ : Type v
• encode : αList self
• decode : List self
• decode_encode : ∀ (x : α), self.decode (self.encode x) = some x
Instances For
theorem Computability.Encoding.decode_encode {α : Type u} (self : ) (x : α) :
self.decode (self.encode x) = some x
structure Computability.FinEncoding (α : Type u) extends :
Type (max 1 u)

An encoding plus a guarantee of finiteness of the alphabet.

• Γ : Type
• encode : αList self
• decode : List self
• decode_encode : ∀ (x : α), self.decode (self.encode x) = some x
• ΓFin : Fintype self
Instances For
instance Computability.Γ.fintype {α : Type u} (e : ) :
Fintype e
Equations
• = e.ΓFin

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

Instances For
Equations
• One or more equations did not get rendered due to their size.

The natural inclusion of bool in Γ'.

Equations
Instances For

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

Equations
• = match x with | => b | x => default
Instances For

An encoding function of the positive binary numbers in bool.

Equations
Instances For

An encoding function of the binary numbers in bool.

Equations
Instances For

An encoding function of ℕ in bool.

Equations
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.

Equations
Instances For

A decoding function from List Bool to ℕ.

Equations
Instances For

A binary encoding of ℕ in bool.

Equations
• One or more equations did not get rendered due to their size.
Instances For

A binary fin_encoding of ℕ in bool.

Equations
Instances For

A binary encoding of ℕ in Γ'.

Equations
• One or more equations did not get rendered due to their size.
Instances For

A binary fin_encoding of ℕ in Γ'.

Equations
Instances For

A unary encoding function of ℕ in bool.

Equations
Instances For

A unary decoding function from List Bool to ℕ.

Equations
Instances For

A unary fin_encoding of ℕ.

Equations
• One or more equations did not get rendered due to their size.
Instances For

An encoding function of bool in bool.

Equations
Instances For

A decoding function from List Bool to bool.

Equations
• = match x with | b :: tail => b | x => default
Instances For

A fin_encoding of bool in bool.

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations