Documentation

Mathlib.Computability.Encoding

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 #

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 selfOption α
  • decode_encode : ∀ (x : α), self.decode (self.encode x) = some x
Instances For
theorem Computability.Encoding.decode_encode {α : Type u} (self : Computability.Encoding α) (x : α) :
self.decode (self.encode x) = some x
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 selfOption α
  • decode_encode : ∀ (x : α), self.decode (self.encode x) = some x
  • ΓFin : Fintype self
Instances For

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

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

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

Equations

An encoding function of the binary numbers in bool.

Equations

An encoding function of ℕ in bool.

Equations

A decoding function from List Bool to the binary numbers.

Equations

A decoding function from List Bool to ℕ.

Equations

A binary encoding of ℕ in bool.

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

A binary encoding of ℕ in Γ'.

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

A unary decoding function from List Bool to ℕ.

Equations

A unary fin_encoding of ℕ.

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

An encoding function of bool in bool.

Equations

A decoding function from List Bool to bool.

Equations

A fin_encoding of bool in bool.

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