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.
• finEncodingList : an encoding of List α in the alphabet α.
• finEncodingPair : an encoding of α × β from encodings of α and β.

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

  The alphabet of the encoding

• encode : α → List self.Γ

  The encoding function

• decode : List self.Γ → Option α

  The decoding function

• decode_encode (x : α) : self.decode (self.encode x) = some x

  Decoding and encoding are inverses of each other.

theorem Computability.Encoding.encode_injective {α : Type u} (e : Encoding α) : Function.Injective e.encode

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

An Encoding plus a guarantee of finiteness of the alphabet.

• Γ : Type
• encode : α → List self.Γ
• decode : List self.Γ → Option α
• decode_encode (x : α) : self.decode (self.encode x) = some x
• ΓFin : Fintype self.Γ

  The alphabet of the encoding is finite

@[implicit_reducible]

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

inductive Computability.Γ' : Type

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

• blank : Γ'
• bit (b : Bool) : Γ'
• bra : Γ'
• ket : Γ'
• comma : Γ'

@[implicit_reducible]

instance Computability.instDecidableEqΓ' : DecidableEq Γ'

def Computability.instDecidableEqΓ'.decEq (x✝ x✝¹ : Γ') : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance Computability.instFintypeΓ' : Fintype Γ'

@[implicit_reducible]

instance Computability.inhabitedΓ' : Inhabited Γ'

def Computability.inclusionBoolΓ' : Bool → Γ'

The natural inclusion of Bool in Γ'.

def Computability.sectionΓ'Bool : Γ' → Bool

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

@[simp]

theorem Computability.sectionΓ'Bool_inclusionBoolΓ' {b : Bool} : sectionΓ'Bool (inclusionBoolΓ' b) = b

theorem Computability.inclusionBoolΓ'_injective : Function.Injective inclusionBoolΓ'

def Computability.encodePosNum : PosNum → List Bool

An encoding function of the positive binary numbers in Bool.

def Computability.encodeNum : Num → List Bool

An encoding function of the binary numbers in Bool.

def Computability.encodeNat (n : ℕ) : List Bool

An encoding function of ℕ in Bool.

def Computability.decodePosNum : List Bool → PosNum

A decoding function from List Bool to the positive binary numbers.

def Computability.decodeNum : List Bool → Num

A decoding function from List Bool to the binary numbers.

def Computability.decodeNat : List Bool → ℕ

A decoding function from List Bool to ℕ.

theorem Computability.encodePosNum_nonempty (n : PosNum) : encodePosNum n ≠ []

@[simp]

theorem Computability.decode_encodePosNum (n : PosNum) : decodePosNum (encodePosNum n) = n

@[simp]

theorem Computability.decode_encodeNum (n : Num) : decodeNum (encodeNum n) = n

@[simp]

theorem Computability.decode_encodeNat (n : ℕ) : decodeNat (encodeNat n) = n

def Computability.encodingNatBool : Encoding ℕ

A binary Encoding of ℕ in Bool.

def Computability.finEncodingNatBool : FinEncoding ℕ

A binary encoding of ℕ in Bool, as a FinEncoding.

def Computability.encodingNatΓ' : Encoding ℕ

A binary Encoding of ℕ in Γ'.

def Computability.finEncodingNatΓ' : FinEncoding ℕ

A binary FinEncoding of ℕ in Γ'.

def Computability.unaryEncodeNat : ℕ → List Bool

A unary encoding function of ℕ in Bool.

def Computability.unaryDecodeNat : List Bool → ℕ

A unary decoding function from List Bool to ℕ.

@[simp]

theorem Computability.unary_decode_encode_nat (n : ℕ) : unaryDecodeNat (unaryEncodeNat n) = n

def Computability.unaryFinEncodingNat : FinEncoding ℕ

A unary FinEncoding of ℕ in Bool.

def Computability.encodeBool : Bool → List Bool

An encoding function of Bool in Bool.

def Computability.decodeBool : List Bool → Bool

A decoding function from List Bool to Bool.

@[simp]

theorem Computability.decode_encodeBool (b : Bool) : decodeBool (encodeBool b) = b

def Computability.finEncodingBoolBool : FinEncoding Bool

A FinEncoding of Bool in Bool.

@[implicit_reducible]

instance Computability.inhabitedFinEncoding : Inhabited (FinEncoding Bool)

@[implicit_reducible]

instance Computability.inhabitedEncoding : Inhabited (Encoding Bool)

theorem Computability.Encoding.card_le_card_list {α : Type u} (e : Encoding α) : Cardinal.lift.{v, u} (Cardinal.mk α) ≤ Cardinal.lift.{u, v} (Cardinal.mk (List e.Γ))

theorem Computability.Encoding.card_le_aleph0 {α : Type u} (e : Encoding α) [Countable e.Γ] : Cardinal.mk α ≤ Cardinal.aleph0

theorem Computability.FinEncoding.card_le_aleph0 {α : Type u} (e : FinEncoding α) : Cardinal.mk α ≤ Cardinal.aleph0

def Computability.finEncodingList (α : Type) [Fintype α] : FinEncoding (List α)

A FinEncoding of a List α in (finite) alphabet α, encoded directly.

def Computability.finEncodingPair {α : Type u_1} {β : Type u_2} (ea : FinEncoding α) (eb : FinEncoding β) : FinEncoding (α × β)

Given FinEncoding of α and β, constructs a FinEncoding of α × β by concatenating the encodings, mapping the symbols from the first encoding with Sum.inl and those from the second with Sum.inr.