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.Γ → Option α
• decode_encode : ∀ (x : α), self.decode (self.encode x) = some x

theorem Computability.Encoding.decode_encode {α : Type u} (self : Computability.Encoding α) (x : α) : self.decode (self.encode x) = some x

theorem Computability.Encoding.encode_injective {α : Type u} (e : Computability.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.Γ

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

Equations

• Computability.Γ.fintype e = e.ΓFin

inductive Computability.Γ' : Type

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

• blank: Computability.Γ'
• bit: Bool → Computability.Γ'
• bra: Computability.Γ'
• ket: Computability.Γ'
• comma: Computability.Γ'

instance Computability.instDecidableEqΓ' : DecidableEq Computability.Γ'

Equations

• Computability.instDecidableEqΓ' = Computability.decEqΓ'✝

instance Computability.Γ'.fintype : Fintype Computability.Γ'

Equations

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

instance Computability.inhabitedΓ' : Inhabited Computability.Γ'

Equations

• Computability.inhabitedΓ' = { default := Computability.Γ'.blank }

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

The natural inclusion of bool in Γ'.

Equations

• Computability.inclusionBoolΓ' = Computability.Γ'.bit

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

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

Equations

• Computability.sectionΓ'Bool (Computability.Γ'.bit b) = b
• Computability.sectionΓ'Bool x = default

theorem Computability.leftInverse_section_inclusion : Function.LeftInverse Computability.sectionΓ'Bool Computability.inclusionBoolΓ'

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

def Computability.encodePosNum : PosNum → List Bool

An encoding function of the positive binary numbers in bool.

Equations

• Computability.encodePosNum PosNum.one = [true]
• Computability.encodePosNum n.bit0 = false :: Computability.encodePosNum n
• Computability.encodePosNum n.bit1 = true :: Computability.encodePosNum n

def Computability.encodeNum : Num → List Bool

An encoding function of the binary numbers in bool.

Equations

• Computability.encodeNum Num.zero = []
• Computability.encodeNum (Num.pos n) = Computability.encodePosNum n

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

An encoding function of ℕ in bool.

Equations

• Computability.encodeNat n = Computability.encodeNum ↑n

def Computability.decodePosNum : List Bool → PosNum

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

Equations

• Computability.decodePosNum (false :: l) = (Computability.decodePosNum l).bit0
• Computability.decodePosNum (true :: l) = if l = [] then PosNum.one else (Computability.decodePosNum l).bit1
• Computability.decodePosNum x = PosNum.one

def Computability.decodeNum : List Bool → Num

A decoding function from List Bool to the binary numbers.

Equations

• Computability.decodeNum l = if l = [] then Num.zero else ↑(Computability.decodePosNum l)

def Computability.decodeNat : List Bool → ℕ

A decoding function from List Bool to ℕ.

Equations

• Computability.decodeNat l = ↑(Computability.decodeNum l)

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

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

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

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

def Computability.encodingNatBool : Computability.Encoding ℕ

A binary encoding of ℕ in bool.

Equations

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

def Computability.finEncodingNatBool : Computability.FinEncoding ℕ

A binary fin_encoding of ℕ in bool.

Equations

• Computability.finEncodingNatBool = { toEncoding := Computability.encodingNatBool, ΓFin := Bool.fintype }

def Computability.encodingNatΓ' : Computability.Encoding ℕ

A binary encoding of ℕ in Γ'.

Equations

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

def Computability.finEncodingNatΓ' : Computability.FinEncoding ℕ

A binary fin_encoding of ℕ in Γ'.

Equations

• Computability.finEncodingNatΓ' = { toEncoding := Computability.encodingNatΓ', ΓFin := Computability.Γ'.fintype }

def Computability.unaryEncodeNat : ℕ → List Bool

A unary encoding function of ℕ in bool.

Equations

• Computability.unaryEncodeNat 0 = []
• Computability.unaryEncodeNat n.succ = true :: Computability.unaryEncodeNat n

def Computability.unaryDecodeNat : List Bool → ℕ

A unary decoding function from List Bool to ℕ.

Equations

• Computability.unaryDecodeNat = List.length

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

def Computability.unaryFinEncodingNat : Computability.FinEncoding ℕ

A unary fin_encoding of ℕ.

Equations

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

def Computability.encodeBool : Bool → List Bool

An encoding function of bool in bool.

Equations

• Computability.encodeBool = pure

def Computability.decodeBool : List Bool → Bool

A decoding function from List Bool to bool.

Equations

• Computability.decodeBool (b :: tail) = b
• Computability.decodeBool x = default

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

def Computability.finEncodingBoolBool : Computability.FinEncoding Bool

A fin_encoding of bool in bool.

Equations

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

instance Computability.inhabitedFinEncoding : Inhabited (Computability.FinEncoding Bool)

Equations

• Computability.inhabitedFinEncoding = { default := Computability.finEncodingBoolBool }

instance Computability.inhabitedEncoding : Inhabited (Computability.Encoding Bool)

Equations

• Computability.inhabitedEncoding = { default := Computability.finEncodingBoolBool.toEncoding }

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

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

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