Explicit binary codes for finite alphabets

An enumeration assigns index i to the palindromic codeword false, true^i, false. Concatenation encodes words, including the empty word. Decoding rejects missing delimiters and indices outside the enumeration. Reversing an encoding therefore reverses its letters without changing their codes.

structure Complexity.FiniteAlphabetCode (α : Type) : Type

An explicit enumeration of an alphabet, including an empty alphabet.

• size : ℕ

  Number of letters.

• index : α ≃ Fin self.size

  Chosen numbering of the letters.

noncomputable def Complexity.FiniteAlphabetCode.ofFintype (α : Type) [Fintype α] : FiniteAlphabetCode α

Choose a code from a finite-alphabet instance.

Equations

• Complexity.FiniteAlphabetCode.ofFintype α = { size := Fintype.card α, index := Fintype.equivFin α }

def Complexity.FiniteAlphabetCode.symbol {α : Type} (c : FiniteAlphabetCode α) (a : α) : List Bool

A delimited unary symbol code, identical to its reversal.

Equations

• c.symbol a = false :: List.replicate (↑(c.index a)) true ++ [false]

def Complexity.FiniteAlphabetCode.encode {α : Type} (c : FiniteAlphabetCode α) (w : List α) : List Bool

Concatenate the symbol codes of a word.

Equations

• c.encode w = List.flatMap c.symbol w

def Complexity.FiniteAlphabetCode.decodeFrom {α : Type} (c : FiniteAlphabetCode α) : Option ℕ → List Bool → Option (List α)

Decode a suffix while waiting for an opening delimiter or counting an open codeword.

Equations

• c.decodeFrom none [] = some []
• c.decodeFrom (some val) [] = none
• c.decodeFrom none (false :: bs) = c.decodeFrom (some 0) bs
• c.decodeFrom none (true :: tail) = none
• c.decodeFrom (some i) (true :: bs) = if i + 1 < c.size then c.decodeFrom (some (i + 1)) bs else none
• c.decodeFrom (some i) (false :: bs) = if h : i < c.size then Option.map (fun (x : List α) => c.index.symm ⟨i, h⟩ :: x) (c.decodeFrom none bs) else none

def Complexity.FiniteAlphabetCode.decode {α : Type} (c : FiniteAlphabetCode α) (bits : List Bool) : Option (List α)

Decode an entire word, rejecting every malformed code.

Equations

• c.decode bits = c.decodeFrom none bits

def Complexity.FiniteAlphabetCode.map {α β : Type} (input : FiniteAlphabetCode α) (output : FiniteAlphabetCode β) (f : List α → List β) (bits : List Bool) : List Bool

Encode a function's result on valid inputs and return empty output on invalid codes.

Equations

• input.map output f bits = match input.decode bits with | none => [] | some w => output.encode (f w)