Total decoders with plain degree certificates

A decoder is total on every word, inverts its encoding, and carries independent cost and encoded output degrees. The basic constructors preserve totality and the round-trip law.

Main definitions

• Turing.MultiTapeTM.Decoder: total decoding with independent cost and output degrees.
• Turing.MultiTapeTM.Decoder.computableInPolyTime: the ordinary polynomial-time certificate.
• Turing.MultiTapeTM.Decoder.bits, .unary, .bool, .option, .pair, .map: basic decoders.

structure Turing.MultiTapeTM.Decoder {α : Type} (enc : α ↪ List Bool) : Type

A total decoder with polynomial cost and encoded-output growth on every input word.

• decode : List Bool → α

  The decoded value of any word.

• decode_enc (a : α) : self.decode (enc a) = a

  Decoding inverts the encoding.

• computable : ∃ (d : ℕ) (e : ℕ), ComputableInDegree self.decode encBits enc d e

  Decoding has independent cost and encoded-output degrees, including zero.

theorem Turing.MultiTapeTM.Decoder.computableInPolyTime {α : Type} {enc : α ↪ List Bool} (D : Decoder enc) : ComputableInPolyTime D.decode encBits enc

Every total decoder has a plain polynomial-time certificate.

def Turing.MultiTapeTM.Decoder.bits : Decoder encBits

Bit strings are their own encoding.

def Turing.MultiTapeTM.Decoder.unary : Decoder encUnary

Unary numbers are decoded by the length of the word.

def Turing.MultiTapeTM.Decoder.bool : Decoder encBool

Booleans are decoded from the first symbol.

def Turing.MultiTapeTM.Decoder.option {α : Type} {enc : α ↪ List Bool} (D : Decoder enc) : Decoder (encOption enc)

Options are decoded as none from the empty word, and otherwise from the tail.

def Turing.MultiTapeTM.Decoder.pair {β₁ β₂ : Type} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} (D₁ : Decoder enc₁) (D₂ : Decoder enc₂) : Decoder (encPair enc₁ enc₂)

Pairs are decoded from the framed first component and what follows it.

def Turing.MultiTapeTM.Decoder.map {α β : Type} {enc : α ↪ List Bool} {enc' : β ↪ List Bool} (D : Decoder enc) (f : α → β) (g : β → α) (hfg : ∀ (b : β), f (g b) = b) (henc : ∀ (a : α), enc' (f a) = enc a) : Decoder enc'

Transport a decoder along an encoding equality and a right inverse.