Total decoders

A decoder for an encoding enc : α ↪ List Bool (Turing.MultiTapeTM.Decoder) is a function on all words that inverts enc on its image and is tidily computable within bounds of fixed degrees. On a malformed word it still returns a value, whose encoding has polynomial length.

Decoders are built along the structure of an encoding: unary numbers by their length, binary numbers by reading their digits up to the last true (Turing.MultiTapeTM.ofBits), Booleans by their first symbol, options by testing for the empty word, pairs by reading the framed first component (Turing.MultiTapeTM.unframe) and what follows it (Turing.MultiTapeTM.dropFrame), and lists by splitting a word into framed words (Turing.MultiTapeTM.frames) and decoding each. The splitting is done by a finite-state transducer that closes a final incomplete frame, so that every word yields a valid encoded list, and the framed words of an encoded list are its encoded elements.

Main definitions

• Turing.MultiTapeTM.frames: the framed words one after another in a word.
• Turing.MultiTapeTM.ofBits: binary digits, least significant first, read as a number.
• Turing.MultiTapeTM.Decoder: total decoders with tidy certificates of fixed degrees.
• Turing.MultiTapeTM.Decoder.bits, .unary, .nat, .bool, .option, .pair, .list, .map: decoders of bit strings, unary and binary numbers, Booleans, options, pairs and lists, and transport along an equivalence of encodings.

Main results

• Turing.MultiTapeTM.frames_encList: the framed words of an encoded list are its encoded elements.
• Turing.MultiTapeTM.computableTidilyInDegree_frames: splitting into framed words is linear.
• Turing.MultiTapeTM.bits_ofBits: the binary digits of a word read as a number are the word up to its last true.

Framed words one after another

theorem Turing.MultiTapeTM.length_dropFrame_le (w : List Bool) : (dropFrame w).length ≤ w.length

Dropping a frame does not lengthen a word.

theorem Turing.MultiTapeTM.length_dropFrame_lt {w : List Bool} : w ≠ [] → (dropFrame w).length < w.length

Dropping a frame shortens a nonempty word.

@[irreducible]

def Turing.MultiTapeTM.frames (w : List Bool) : List (List Bool)

The words framed one after another in w. A final incomplete frame is closed.

@[simp]

theorem Turing.MultiTapeTM.frames_nil : frames [] = []

theorem Turing.MultiTapeTM.frames_of_ne_nil {w : List Bool} (h : w ≠ []) : frames w = unframe w :: frames (dropFrame w)

theorem Turing.MultiTapeTM.frames_frame_append (u v : List Bool) : frames (frame u ++ v) = u :: frames v

A framed word followed by another word.

theorem Turing.MultiTapeTM.frames_encList {α : Type u_1} (enc : α ↪ List Bool) (l : List α) : frames ((encList enc) l) = List.map (⇑enc) l

The framed words of an encoded list are its encoded elements.

inductive Turing.MultiTapeTM.FramesState : Type

The states of the transducer splitting a word into framed words: between frames, inside a frame after a marker, and inside a frame after a symbol.

• between : FramesState
• marker : FramesState
• symbol : FramesState

@[instance_reducible]

instance Turing.MultiTapeTM.instDecidableEqFramesState : DecidableEq FramesState

instance Turing.MultiTapeTM.instFiniteFramesState : Finite FramesState

def Turing.MultiTapeTM.framesT : Transducer Bool FramesState

Splits a word into framed words, closing a final incomplete frame.

@[simp]

theorem Turing.MultiTapeTM.framesT_step (x✝ : FramesState) (x✝¹ : Bool) : framesT.step x✝ x✝¹ = match x✝, x✝¹ with | FramesState.between, true => (FramesState.marker, []) | FramesState.between, false => (FramesState.between, [false]) | FramesState.marker, b => (FramesState.symbol, [true, b]) | FramesState.symbol, true => (FramesState.marker, []) | FramesState.symbol, false => (FramesState.between, [false])

@[simp]

theorem Turing.MultiTapeTM.framesT_q₀ : framesT.q₀ = FramesState.between

@[simp]

theorem Turing.MultiTapeTM.framesT_final (x✝ : FramesState) : framesT.final x✝ = match x✝ with | FramesState.between => [] | x => [false]

theorem Turing.MultiTapeTM.framesT_run_symbol (v : List Bool) : framesT.run FramesState.symbol v = frame (unframe v) ++ framesT.run FramesState.between (dropFrame v)

Inside a frame, the transducer completes the frame at the start of its input and continues with what follows.

theorem Turing.MultiTapeTM.framesT_run (w : List Bool) : framesT.run FramesState.between w = (encList encBits) (frames w)

The transducer emits the encoded list of framed words.

theorem Turing.MultiTapeTM.computableTidilyInDegree_frames : ComputableTidilyInDegree frames encBits (encList encBits) 1 1

Splitting a word into framed words is linear.

Binary digits

def Turing.MultiTapeTM.ofBits (w : List Bool) : ℕ

Binary digits, least significant first, read as a number.

theorem Turing.MultiTapeTM.bits_ofBits (w : List Bool) : (ofBits w).bits = List.rdropWhile (fun (x : Bool) => !x) w

The binary digits of a word read as a number are the word up to its last true.

def Turing.MultiTapeTM.dropFalsesT : Transducer Bool Bool

Drops the falses at the start of a word.

theorem Turing.MultiTapeTM.dropFalsesT_run_true (w : List Bool) : dropFalsesT.run true w = w

theorem Turing.MultiTapeTM.dropFalsesT_run (w : List Bool) : dropFalsesT.run false w = List.dropWhile (fun (x : Bool) => !x) w

Decoders

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

A total decoder for the encoding enc: a function on all words that inverts enc and is tidily computable within time, space and output length of fixed degrees in the length of the 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 : ℕ), ComputableTidilyInDegree self.decode encBits enc d e

  Decoding is tidily computable within bounds of fixed degrees.

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

Every total decoder has a native 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.nat : Decoder encNat

Binary numbers are decoded from their digits up to the last true.

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.list {α : Type} {enc : α ↪ List Bool} (D : Decoder enc) : Decoder (encList enc)

Lists are decoded element by element from the framed words of a word.

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 to an encoding enc' agreeing with enc along f, where g is a right inverse of f.