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 β.

source

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.

Instances For

source

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

Function.Injective e.encode

source

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

Instances For

source

@[implicit_reducible]

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

Fintype e.Γ

Equations

Computability.Γ.fintype e = e.ΓFin

source

inductive Computability.Γ' :

Type

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

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

Instances For

source

@[implicit_reducible]

instance Computability.instDecidableEqΓ' :

DecidableEq Γ'

Equations

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

source

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

Decidable (x✝ = x✝¹)

Equations

Instances For

source

@[implicit_reducible]

instance Computability.instFintypeΓ' :

Fintype Γ'

Equations

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

source

@[implicit_reducible]

instance Computability.inhabitedΓ' :

Inhabited Γ'

Equations

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

source

def Computability.inclusionBoolΓ' :

Bool → Γ'

The natural inclusion of Bool in Γ'.

Equations

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

Instances For

source

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

Instances For

source

@[simp]

theorem Computability.sectionΓ'Bool_inclusionBoolΓ' {b : Bool} :

sectionΓ'Bool (inclusionBoolΓ' b) = b

source

theorem Computability.inclusionBoolΓ'_injective :

Function.Injective inclusionBoolΓ'

source

def Computability.encodePosNum :

PosNum → List Bool

An encoding function of the positive binary numbers in Bool.

Equations

Instances For

source

def Computability.encodeNum :

Num → List Bool

An encoding function of the binary numbers in Bool.

Equations

Instances For

source

def Computability.encodeNat (n : ℕ) :

List Bool

An encoding function of ℕ in Bool.

Equations

Computability.encodeNat n = Computability.encodeNum ↑n

Instances For

source

def Computability.decodePosNum :

List Bool → PosNum

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

Equations

Instances For

source

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)

Instances For

source

def Computability.decodeNat :

List Bool → ℕ

A decoding function from List Bool to ℕ.

Equations

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

Instances For

source

theorem Computability.encodePosNum_nonempty (n : PosNum) :

encodePosNum n ≠ []

source

@[simp]

theorem Computability.decode_encodePosNum (n : PosNum) :

decodePosNum (encodePosNum n) = n

source

@[simp]

theorem Computability.decode_encodeNum (n : Num) :

decodeNum (encodeNum n) = n

source

@[simp]

theorem Computability.decode_encodeNat (n : ℕ) :

decodeNat (encodeNat n) = n

source

def Computability.encodingNatBool :

Encoding ℕ

A binary Encoding of ℕ in Bool.

Equations

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

Instances For

source

def Computability.finEncodingNatBool :

FinEncoding ℕ

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

Equations

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

Instances For

source

def Computability.encodingNatΓ' :

Encoding ℕ

A binary Encoding of ℕ in Γ'.

Equations

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

Instances For

source

def Computability.finEncodingNatΓ' :

FinEncoding ℕ

A binary FinEncoding of ℕ in Γ'.

Equations

Computability.finEncodingNatΓ' = { toEncoding := Computability.encodingNatΓ', ΓFin := inferInstanceAs (Fintype Computability.Γ') }

Instances For

source

def Computability.unaryEncodeNat :

ℕ → List Bool

A unary encoding function of ℕ in Bool.

Equations

Instances For

source

def Computability.unaryDecodeNat :

List Bool → ℕ

A unary decoding function from List Bool to ℕ.

Equations

Computability.unaryDecodeNat = List.length

Instances For

source

@[simp]

theorem Computability.unary_decode_encode_nat (n : ℕ) :

unaryDecodeNat (unaryEncodeNat n) = n

source

def Computability.unaryFinEncodingNat :

FinEncoding ℕ

A unary FinEncoding of ℕ in Bool.

Equations

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

Instances For

source

def Computability.encodeBool :

Bool → List Bool

An encoding function of Bool in Bool.

Equations

Computability.encodeBool = pure

Instances For

source

def Computability.decodeBool :

List Bool → Bool

A decoding function from List Bool to Bool.

Equations

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

Instances For

source

@[simp]

theorem Computability.decode_encodeBool (b : Bool) :

decodeBool (encodeBool b) = b

source

def Computability.finEncodingBoolBool :

FinEncoding Bool

A FinEncoding of Bool in Bool.

Equations

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

Instances For

source

@[implicit_reducible]

instance Computability.inhabitedFinEncoding :

Inhabited (FinEncoding Bool)

Equations

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

source

@[implicit_reducible]

instance Computability.inhabitedEncoding :

Inhabited (Encoding Bool)

Equations

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

source

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.Γ))

source

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

Cardinal.mk α ≤ Cardinal.aleph0

source

theorem Computability.FinEncoding.card_le_aleph0 {α : Type u} (e : FinEncoding α) :

Cardinal.mk α ≤ Cardinal.aleph0

source

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

FinEncoding (List α)

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

Equations

Computability.finEncodingList α = { Γ := α, encode := id, decode := some, decode_encode := ⋯, ΓFin := inferInstance }

Instances For

source

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.

Equations

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

Instances For

Documentation

Mathlib.Computability.Encoding

Encodings #

Examples #