Encodings

This file contains the definition of an encoding, a map from a type to strings in an alphabet, used in defining computability by Turing machines. It also contains several examples:

Examples

• encodingNatBool : a binary encoding of ℕ in a simple alphabet.
• encodingNatΓ' : a binary encoding of ℕ in the alphabet used for TM's.
• unaryEncodingNat : a unary encoding of ℕ
• encodingBoolBool : an encoding of Bool.
• encodingList : an encoding of List α in the alphabet α.
• encodingProd : an encoding of α × β from encodings of α and β.

structure Computability.Encoding (α : Type u) (Γ : Type v) : Type (max u v)

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

• encode : α → List Γ

  The encoding function

• decode : List Γ → 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_1} {Γ : Type u_2} (e : Encoding α Γ) : Function.Injective e.encode

inductive Computability.Γ' : Type

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

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

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

Equations

• Computability.instDecidableEqΓ'.decEq Computability.Γ'.blank Computability.Γ'.blank = isTrue ⋯
• Computability.instDecidableEqΓ'.decEq Computability.Γ'.blank (Computability.Γ'.bit b) = isFalse ⋯
• Computability.instDecidableEqΓ'.decEq Computability.Γ'.blank Computability.Γ'.bra = isFalse Computability.instDecidableEqΓ'.decEq._proof_4
• Computability.instDecidableEqΓ'.decEq Computability.Γ'.blank Computability.Γ'.ket = isFalse Computability.instDecidableEqΓ'.decEq._proof_5
• Computability.instDecidableEqΓ'.decEq Computability.Γ'.blank Computability.Γ'.comma = isFalse Computability.instDecidableEqΓ'.decEq._proof_6
• Computability.instDecidableEqΓ'.decEq (Computability.Γ'.bit b) Computability.Γ'.blank = isFalse ⋯
• Computability.instDecidableEqΓ'.decEq (Computability.Γ'.bit a) (Computability.Γ'.bit b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Computability.instDecidableEqΓ'.decEq (Computability.Γ'.bit b) Computability.Γ'.bra = isFalse ⋯
• Computability.instDecidableEqΓ'.decEq (Computability.Γ'.bit b) Computability.Γ'.ket = isFalse ⋯
• Computability.instDecidableEqΓ'.decEq (Computability.Γ'.bit b) Computability.Γ'.comma = isFalse ⋯
• Computability.instDecidableEqΓ'.decEq Computability.Γ'.bra Computability.Γ'.blank = isFalse Computability.instDecidableEqΓ'.decEq._proof_12
• Computability.instDecidableEqΓ'.decEq Computability.Γ'.bra (Computability.Γ'.bit b) = isFalse ⋯
• Computability.instDecidableEqΓ'.decEq Computability.Γ'.bra Computability.Γ'.bra = isTrue ⋯
• Computability.instDecidableEqΓ'.decEq Computability.Γ'.bra Computability.Γ'.ket = isFalse Computability.instDecidableEqΓ'.decEq._proof_14
• Computability.instDecidableEqΓ'.decEq Computability.Γ'.bra Computability.Γ'.comma = isFalse Computability.instDecidableEqΓ'.decEq._proof_15
• Computability.instDecidableEqΓ'.decEq Computability.Γ'.ket Computability.Γ'.blank = isFalse Computability.instDecidableEqΓ'.decEq._proof_16
• Computability.instDecidableEqΓ'.decEq Computability.Γ'.ket (Computability.Γ'.bit b) = isFalse ⋯
• Computability.instDecidableEqΓ'.decEq Computability.Γ'.ket Computability.Γ'.bra = isFalse Computability.instDecidableEqΓ'.decEq._proof_18
• Computability.instDecidableEqΓ'.decEq Computability.Γ'.ket Computability.Γ'.ket = isTrue ⋯
• Computability.instDecidableEqΓ'.decEq Computability.Γ'.ket Computability.Γ'.comma = isFalse Computability.instDecidableEqΓ'.decEq._proof_19
• Computability.instDecidableEqΓ'.decEq Computability.Γ'.comma Computability.Γ'.blank = isFalse Computability.instDecidableEqΓ'.decEq._proof_20
• Computability.instDecidableEqΓ'.decEq Computability.Γ'.comma (Computability.Γ'.bit b) = isFalse ⋯
• Computability.instDecidableEqΓ'.decEq Computability.Γ'.comma Computability.Γ'.bra = isFalse Computability.instDecidableEqΓ'.decEq._proof_22
• Computability.instDecidableEqΓ'.decEq Computability.Γ'.comma Computability.Γ'.ket = isFalse Computability.instDecidableEqΓ'.decEq._proof_23
• Computability.instDecidableEqΓ'.decEq Computability.Γ'.comma Computability.Γ'.comma = isTrue ⋯

@[instance_reducible]

instance Computability.instDecidableEqΓ' : DecidableEq Γ'

Equations

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

@[instance_reducible]

instance Computability.instFintypeΓ' : Fintype Γ'

Equations

• Computability.instFintypeΓ' = Fintype.ofEquiv (Unit ⊕ Bool ⊕ Unit ⊕ Unit ⊕ Unit) Computability.Γ'.proxyTypeEquiv

@[instance_reducible]

instance Computability.inhabitedΓ' : Inhabited Γ'

Equations

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

def Computability.inclusionBoolΓ' : Bool → Γ'

The natural inclusion of Bool in Γ'.

Equations

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

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

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

Equations

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

@[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.

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) : 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 ℕ Bool

A binary Encoding of ℕ in Bool.

Equations

• Computability.encodingNatBool = { encode := Computability.encodeNat, decode := fun (n : List Bool) => some (Computability.decodeNat n), decode_encode := Computability.encodingNatBool._proof_1 }

def Computability.encodingNatΓ' : Encoding ℕ Γ'

A binary Encoding of ℕ in Γ'.

Equations

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

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

@[simp]

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

def Computability.unaryEncodingNat : Encoding ℕ Bool

A unary Encoding of ℕ in Bool.

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

@[simp]

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

def Computability.encodingBoolBool : Encoding Bool Bool

An Encoding of Bool in Bool.

Equations

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

@[instance_reducible]

instance Computability.inhabitedEncoding : Inhabited (Encoding Bool Bool)

Equations

• Computability.inhabitedEncoding = { default := Computability.encodingBoolBool }

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

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

def Computability.encodingList (α : Type) : Encoding (List α) α

An Encoding of a List α in alphabet α, encoded directly.

Equations

• Computability.encodingList α = { encode := id, decode := some, decode_encode := ⋯ }

def Computability.encodingProd {α : Type u_1} {β : Type u_2} {Γ₁ : Type u_3} {Γ₂ : Type u_4} (ea : Encoding α Γ₁) (eb : Encoding β Γ₂) : Encoding (α × β) (Γ₁ ⊕ Γ₂)

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

Equations

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

Deprecated aliases for FinEncoding and unbundled Γ

@[reducible, deprecated "Use `Encoding α Γ` along with `[Fintype Γ]` instead" (since := "2026-05-07")]

def Computability.FinEncoding (α : Type u) {Γ : Type v} [Fintype Γ] : Type (max u v)

Deprecated: Use Encoding α Γ along with [Fintype Γ] instead.

Equations

• Computability.FinEncoding α = Computability.Encoding α Γ

@[reducible, deprecated "Γ is now an explicit parameter of `Encoding`" (since := "2026-05-07")]

def Computability.Encoding.Γ {α : Type u} {Γ : Type v} : Encoding α Γ → Type v

Deprecated: Γ is now an explicit parameter of Encoding.

Equations

• x✝.Γ = Γ

@[reducible, deprecated "Use `inferInstanceAs (Fintype Γ)` instead" (since := "2026-05-07")]

def Computability.FinEncoding.ΓFin {α : Type u} {Γ : Type v} [h : Fintype Γ] : Encoding α Γ → Fintype Γ

Deprecated: Use inferInstanceAs (Fintype Γ) instead.

Equations

• Computability.FinEncoding.ΓFin x✝ = h

@[reducible, deprecated "Use the encoding directly" (since := "2026-05-07")]

def Computability.FinEncoding.toEncoding {α : Type u} {Γ : Type v} [Fintype Γ] (e : Encoding α Γ) : Encoding α Γ

Deprecated: Use the encoding directly.

Equations

• Computability.FinEncoding.toEncoding e = e

@[reducible, inline, deprecated Computability.encodingNatBool (since := "2026-05-07")]

abbrev Computability.finEncodingNatBool : Encoding ℕ Bool

Deprecated alias for encodingNatBool.

Equations

• Computability.finEncodingNatBool = Computability.encodingNatBool

@[reducible, inline, deprecated Computability.encodingNatΓ' (since := "2026-05-07")]

abbrev Computability.finEncodingNatΓ' : Encoding ℕ Γ'

Deprecated alias for encodingNatΓ'.

Equations

• Computability.finEncodingNatΓ' = Computability.encodingNatΓ'

@[reducible, inline, deprecated Computability.unaryEncodingNat (since := "2026-05-07")]

abbrev Computability.unaryFinEncodingNat : Encoding ℕ Bool

Deprecated alias for unaryEncodingNat.

Equations

• Computability.unaryFinEncodingNat = Computability.unaryEncodingNat

@[reducible, inline, deprecated Computability.encodingBoolBool (since := "2026-05-07")]

abbrev Computability.finEncodingBoolBool : Encoding Bool Bool

Deprecated alias for encodingBoolBool.

Equations

• Computability.finEncodingBoolBool = Computability.encodingBoolBool

@[reducible, deprecated Computability.encodingList (since := "2026-05-07")]

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

Deprecated alias for encodingList.

Equations

• Computability.finEncodingList α = Computability.encodingList α

@[reducible, deprecated Computability.encodingProd (since := "2026-05-07")]

def Computability.finEncodingPair {α : Type u_1} {β : Type u_2} {Γ₁ : Type u_3} {Γ₂ : Type u_4} [Fintype Γ₁] [Fintype Γ₂] (ea : Encoding α Γ₁) (eb : Encoding β Γ₂) : Encoding (α × β) (Γ₁ ⊕ Γ₂)

Deprecated alias for encodingProd.

Equations

• Computability.finEncodingPair ea eb = Computability.encodingProd ea eb

@[deprecated Computability.Encoding.card_le_aleph0 (since := "2026-05-07")]

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

Deprecated alias for Encoding.card_le_aleph0.