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 computable within independent 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 plain certificates of independent 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.computableInDegree_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.computableInDegree_frames : ComputableInDegree frames encBits (encList encBits) 1 1

Splitting a word into framed words is linear.

Decoders

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.