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.

source

structure computability.encoding (α : Type) :

Type 1

Γ : Type
encode : α → list c.Γ
decode : list c.Γ → option α
decode_encode : ∀ (x : α), c.decode (c.encode x) = some x

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

source

structure computability.fin_encoding (α : Type) :

Type 1

to_encoding : computability.encoding α
Γ_fin : fintype c.to_encoding.Γ

An encoding plus a guarantee of finiteness of the alphabet.

source

@[instance]

def computability.Γ'.fintype :

fintype computability.Γ'

source

inductive computability.Γ' :

Type

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

source

@[instance]

def computability.Γ'.decidable_eq :

decidable_eq computability.Γ'

source

@[instance]

def computability.inhabited_Γ' :

inhabited computability.Γ'

Equations

computability.inhabited_Γ' = {default := computability.Γ'.blank}

source

def computability.inclusion_bool_Γ' (a : bool) :

computability.Γ'

The natural inclusion of bool in Γ'.

Equations

computability.inclusion_bool_Γ' = computability.Γ'.bit

source

def computability.section_Γ'_bool (a : computability.Γ') :

bool

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

Equations

source

theorem computability.left_inverse_section_inclusion :

function.left_inverse computability.section_Γ'_bool computability.inclusion_bool_Γ'

source

theorem computability.inclusion_bool_Γ'_injective :

function.injective computability.inclusion_bool_Γ'

source

def computability.encode_pos_num (a : pos_num) :

list bool

An encoding function of the positive binary numbers in bool.

Equations

source

def computability.encode_num (a : num) :

list bool

An encoding function of the binary numbers in bool.

Equations

source

def computability.encode_nat (n : ℕ) :

list bool

An encoding function of ℕ in bool.

Equations

computability.encode_nat n = computability.encode_num ↑n

source

def computability.decode_pos_num (a : list bool) :

pos_num

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

Equations

source

def computability.decode_num (a : list bool) :

num

A decoding function from list bool to the binary numbers.

Equations

computability.decode_num = λ (l : list bool), ite (l = list.nil) num.zero ↑(computability.decode_pos_num l)

source

def computability.decode_nat (a : list bool) :

ℕ

A decoding function from list bool to ℕ.

Equations

computability.decode_nat = λ (l : list bool), ↑(computability.decode_num l)

source

theorem computability.encode_pos_num_nonempty (n : pos_num) :

computability.encode_pos_num n ≠ list.nil

source

theorem computability.decode_encode_pos_num (n : pos_num) :

computability.decode_pos_num (computability.encode_pos_num n) = n

source

theorem computability.decode_encode_num (n : num) :

computability.decode_num (computability.encode_num n) = n

source

theorem computability.decode_encode_nat (n : ℕ) :

computability.decode_nat (computability.encode_nat n) = n

source

def computability.encoding_nat_bool :

computability.encoding ℕ

A binary encoding of ℕ in bool.

Equations

computability.encoding_nat_bool = {Γ := bool, encode := computability.encode_nat, decode := λ (n : list bool), some (computability.decode_nat n), decode_encode := computability.encoding_nat_bool._proof_1}

source

def computability.fin_encoding_nat_bool :

computability.fin_encoding ℕ

A binary fin_encoding of ℕ in bool.

Equations

computability.fin_encoding_nat_bool = {to_encoding := computability.encoding_nat_bool, Γ_fin := bool.fintype}

source

def computability.encoding_nat_Γ' :

computability.encoding ℕ

A binary encoding of ℕ in Γ'.

Equations

computability.encoding_nat_Γ' = {Γ := computability.Γ', encode := λ (x : ℕ), list.map computability.inclusion_bool_Γ' (computability.encode_nat x), decode := λ (x : list computability.Γ'), some (computability.decode_nat (list.map computability.section_Γ'_bool x)), decode_encode := computability.encoding_nat_Γ'._proof_1}

source

def computability.fin_encoding_nat_Γ' :

computability.fin_encoding ℕ

A binary fin_encoding of ℕ in Γ'.

Equations

computability.fin_encoding_nat_Γ' = {to_encoding := computability.encoding_nat_Γ', Γ_fin := computability.Γ'.fintype}

source

def computability.unary_encode_nat (a : ℕ) :

list bool

A unary encoding function of ℕ in bool.

Equations

computability.unary_encode_nat (n + 1) = tt :: computability.unary_encode_nat n
computability.unary_encode_nat 0 = list.nil

source

def computability.unary_decode_nat (a : list bool) :

ℕ

A unary decoding function from list bool to ℕ.

Equations

computability.unary_decode_nat = list.length

source

theorem computability.unary_decode_encode_nat (n : ℕ) :

computability.unary_decode_nat (computability.unary_encode_nat n) = n

source

def computability.unary_fin_encoding_nat :

computability.fin_encoding ℕ

A unary fin_encoding of ℕ.

Equations

computability.unary_fin_encoding_nat = {to_encoding := {Γ := bool, encode := computability.unary_encode_nat, decode := λ (n : list bool), some (computability.unary_decode_nat n), decode_encode := computability.unary_fin_encoding_nat._proof_1}, Γ_fin := bool.fintype}

source

def computability.encode_bool (a : bool) :

list bool

An encoding function of bool in bool.

Equations

computability.encode_bool = list.ret

source

def computability.decode_bool (a : list bool) :

bool

A decoding function from list bool to bool.

Equations

computability.decode_bool (b :: _x) = b
computability.decode_bool list.nil = arbitrary bool

source

theorem computability.decode_encode_bool (b : bool) :

computability.decode_bool (computability.encode_bool b) = b

source

def computability.fin_encoding_bool_bool :

computability.fin_encoding bool

A fin_encoding of bool in bool.

Equations

computability.fin_encoding_bool_bool = {to_encoding := {Γ := bool, encode := computability.encode_bool, decode := λ (x : list bool), some (computability.decode_bool x), decode_encode := computability.fin_encoding_bool_bool._proof_1}, Γ_fin := bool.fintype}

source

@[instance]

def computability.inhabited_fin_encoding :

inhabited (computability.fin_encoding bool)

Equations

computability.inhabited_fin_encoding = {default := computability.fin_encoding_bool_bool}

source

@[instance]

def computability.inhabited_encoding :

inhabited (computability.encoding bool)

Equations

computability.inhabited_encoding = {default := computability.fin_encoding_bool_bool.to_encoding}