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.
An encoding plus a guarantee of finiteness of the alphabet.
Instances For
Equations
- Computability.Γ.fintype e = e.ΓFin
A standard Turing machine alphabet, consisting of blank,bit0,bit1,bra,ket,comma.
- blank: Computability.Γ'
- bit: Bool → Computability.Γ'
- bra: Computability.Γ'
- ket: Computability.Γ'
- comma: Computability.Γ'
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- Computability.inhabitedΓ' = { default := Computability.Γ'.blank }
The natural inclusion of bool in Γ'.
Instances For
An arbitrary section of the natural inclusion of bool in Γ'.
Equations
- Computability.sectionΓ'Bool x = match x with | Computability.Γ'.bit b => b | x => default
Instances For
An encoding function of the positive binary numbers in bool.
Equations
Instances For
An encoding function of the binary numbers in bool.
Equations
- Computability.encodeNum x = match x with | Num.zero => [] | Num.pos n => Computability.encodePosNum n
Instances For
An encoding function of ℕ in bool.
Equations
Instances For
A decoding function from List Bool
to the positive binary numbers.
Equations
- Computability.decodePosNum (false :: l) = PosNum.bit0 (Computability.decodePosNum l)
- Computability.decodePosNum (true :: l) = if l = [] then PosNum.one else PosNum.bit1 (Computability.decodePosNum l)
- Computability.decodePosNum x = PosNum.one
Instances For
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
A binary encoding of ℕ in bool.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A binary fin_encoding of ℕ in bool.
Equations
- Computability.finEncodingNatBool = { toEncoding := Computability.encodingNatBool, ΓFin := Bool.fintype }
Instances For
A binary encoding of ℕ in Γ'.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A binary fin_encoding of ℕ in Γ'.
Equations
- Computability.finEncodingNatΓ' = { toEncoding := Computability.encodingNatΓ', ΓFin := Computability.Γ'.fintype }
Instances For
A unary encoding function of ℕ in bool.
Equations
Instances For
A unary decoding function from List Bool
to ℕ.
Equations
- Computability.unaryDecodeNat = List.length
Instances For
A unary fin_encoding of ℕ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A decoding function from List Bool
to bool.
Equations
- Computability.decodeBool x = match x with | b :: tail => b | x => default
Instances For
A fin_encoding of bool in bool.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Computability.inhabitedFinEncoding = { default := Computability.finEncodingBoolBool }
Equations
- Computability.inhabitedEncoding = { default := Computability.finEncodingBoolBool.toEncoding }