Encodings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 u) :

Type (max u (v+1))

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

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

Instances for computability.encoding

computability.encoding.has_sizeof_inst
computability.inhabited_encoding

source

theorem computability.encoding.encode_injective {α : Type u} (e : computability.encoding α) :

function.injective e.encode

source

structure computability.fin_encoding (α : Type u) :

Type (max 1 u)

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

An encoding plus a guarantee of finiteness of the alphabet.

Instances for computability.fin_encoding

computability.fin_encoding.has_sizeof_inst
computability.inhabited_fin_encoding

source

@[protected, instance]

def computability.Γ.fintype {α : Type u} (e : computability.fin_encoding α) :

fintype e.to_encoding.Γ

Equations

computability.Γ.fintype e = e.Γ_fin

source

@[protected, instance]

def computability.Γ'.fintype :

fintype computability.Γ'

source

inductive computability.Γ' :

Type

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

Instances for computability.Γ'

computability.Γ'.has_sizeof_inst
computability.Γ'.fintype
computability.inhabited_Γ'

source

@[protected, instance]

def computability.Γ'.decidable_eq :

decidable_eq computability.Γ'

source

@[protected, instance]

def computability.inhabited_Γ' :

inhabited computability.Γ'

Equations

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

source

def computability.inclusion_bool_Γ' :

bool → computability.Γ'

The natural inclusion of bool in Γ'.

Equations

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

source

def computability.section_Γ'_bool :

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 :

pos_num → list bool

An encoding function of the positive binary numbers in bool.

Equations

source

def computability.encode_num :

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 :

list bool → pos_num

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

Equations

source

def computability.decode_num :

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 :

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), option.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.Γ'), option.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 :

ℕ → list bool

A unary encoding function of ℕ in bool.

Equations

source

def computability.unary_decode_nat :

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), option.some (computability.unary_decode_nat n), decode_encode := computability.unary_fin_encoding_nat._proof_1}, Γ_fin := bool.fintype}

source

def computability.encode_bool :

bool → list bool

An encoding function of bool in bool.

Equations

computability.encode_bool = list.ret

source

def computability.decode_bool :

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), option.some (computability.decode_bool x), decode_encode := computability.fin_encoding_bool_bool._proof_1}, Γ_fin := bool.fintype}

source

@[protected, instance]

def computability.inhabited_fin_encoding :

inhabited (computability.fin_encoding bool)

Equations

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

source

@[protected, instance]

def computability.inhabited_encoding :

inhabited (computability.encoding bool)

Equations

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

source

theorem computability.encoding.card_le_card_list {α : Type u} (e : computability.encoding α) :

(cardinal.mk α).lift ≤ (cardinal.mk (list e.Γ)).lift

source

theorem computability.encoding.card_le_aleph_0 {α : Type u} (e : computability.encoding α) [encodable e.Γ] :

cardinal.mk α ≤ cardinal.aleph_0

source

theorem computability.fin_encoding.card_le_aleph_0 {α : Type u} (e : computability.fin_encoding α) :

cardinal.mk α ≤ cardinal.aleph_0