Decoding finite configurations in polynomial time

Turing.MultiTapeTM.decodeFiniteCfg reads a finite configuration from any word, inverting Turing.MultiTapeTM.encFiniteCfg, in polynomial time; a malformed word decodes to some configuration. The fields are read off the frames of the encoding by unframe and dropFrame, counts are clamped into range, and the cells of a stack tape are read by a finite transducer and folded into a canonical tape by StackTape.cons, last cell first.

Main definitions

• Turing.MultiTapeTM.decodeStackTape, Turing.MultiTapeTM.decodeBiTape: decoders of tapes.
• Turing.MultiTapeTM.decodeTapes: the decoder of a fixed finite family of tapes.
• Turing.MultiTapeTM.decodeFiniteCfg: the decoder of finite configurations.

Main results

• Turing.MultiTapeTM.decodeFiniteCfg_encFiniteCfg: decoding inverts the encoding.
• Turing.MultiTapeTM.ComputableInPolyTime.decodeTapes: decoding a fixed finite family of tapes is polynomial-time.
• Turing.MultiTapeTM.ComputableInPolyTime.decodeFiniteCfg: decoding is polynomial-time.

Implementation notes

Only unframe, dropFrame, list folds and finite transducers from the main development are used. The cell transducer Turing.MultiTapeTM.cellsTransducer splits a framed list of cells, a special case of splitting a word into its framed words; a general splitter with list decoders, once available, could replace it, and Turing.MultiTapeTM.decodeState is a decoder of a finite encoding from its length.

Cells

def Turing.MultiTapeTM.cellBits (cell : Option Bool) : List Bool

The bits of a cell: whether it is occupied, then its symbol, false when it is blank.

def Turing.MultiTapeTM.contentBits : Option (Option Bool) → List Bool

The bits of a framed cell, from a summary of its framed word: blank while the word is empty, otherwise occupied, with the second bit of the word as its symbol.

@[simp]

theorem Turing.MultiTapeTM.length_contentBits (content : Option (Option Bool)) : (contentBits content).length = 2

def Turing.MultiTapeTM.pushContent : Option (Option Bool) → Bool → Option (Option Bool)

Record a bit of a framed word in its summary: only the first two bits matter.

def Turing.MultiTapeTM.cellsTransducer : Transducer Bool (Option (Option Bool) × Bool)

The transducer emitting the bits of every framed cell. Its state is the summary of the framed word read so far, and whether a bit of that word is expected next.

theorem Turing.MultiTapeTM.cellsTransducer_run_frame (cell : Option Bool) (rest : List Bool) : cellsTransducer.run (none, false) (frame ((encOption encBool) cell) ++ rest) = cellBits cell ++ cellsTransducer.run (none, false) rest

The transducer emits the bits of a framed cell and continues after its frame.

theorem Turing.MultiTapeTM.cellsTransducer_run_encList (cells : List (Option Bool)) : cellsTransducer.run cellsTransducer.q₀ ((encList (encOption encBool)) cells) = List.flatMap cellBits cells

On an encoded list of cells, the transducer emits the bits of every cell.

Stack tapes

def Turing.MultiTapeTM.stackStep : Option Bool × Cslib.Turing.StackTape Bool → Bool → Option Bool × Cslib.Turing.StackTape Bool

Read the reversed bits of cells into a tape, last cell first: a symbol bit is held until the occupancy bit before it.

def Turing.MultiTapeTM.decodeStackTape (word : List Bool) : Cslib.Turing.StackTape Bool

Decode a stack tape from any word, inverting encStackTape encBool.

theorem Turing.MultiTapeTM.foldl_stackStep (cells : List (Option Bool)) (tape : Cslib.Turing.StackTape Bool) : List.foldl stackStep (none, tape) (List.flatMap cellBits cells).reverse = (none, List.foldr Cslib.Turing.StackTape.cons tape cells)

The fold over the reversed bits of cells prepends the cells, last first.

theorem Cslib.Turing.StackTape.foldr_cons_toList {Symbol : Type u_1} (tape : StackTape Symbol) : List.foldr cons nil tape.toList = tape

Prepending the stored cells of a stack tape to the empty tape rebuilds it.

theorem Turing.MultiTapeTM.decodeStackTape_encList (cells : List (Option Bool)) : decodeStackTape ((encList (encOption encBool)) cells) = List.foldr Cslib.Turing.StackTape.cons Cslib.Turing.StackTape.nil cells

A word encoding a list of cells decodes to the tape of the cells, without the blank cells at its end.

theorem Turing.MultiTapeTM.decodeStackTape_encStackTape (tape : Cslib.Turing.StackTape Bool) : decodeStackTape ((encStackTape encBool) tape) = tape

Decoding inverts the encoding of stack tapes.

theorem Turing.MultiTapeTM.length_stackStep_le (state : Option Bool × Cslib.Turing.StackTape Bool) (bit : Bool) : ((encPair (encOption encBool) (encStackTape encBool)) (stackStep state bit)).length ≤ ((encPair (encOption encBool) (encStackTape encBool)) state).length + 4

A step of Turing.MultiTapeTM.stackStep lengthens the encoded state by at most four bits.

Two-sided tapes and configurations

def Turing.MultiTapeTM.decodeCell (word : List Bool) : Option Bool

Decode a cell encoded by encOption encBool.

@[simp]

theorem Turing.MultiTapeTM.decodeCell_encOption (cell : Option Bool) : decodeCell ((encOption encBool) cell) = cell

Decoding inverts the encoding of cells.

def Turing.MultiTapeTM.decodeBiTape (word : List Bool) : Cslib.Turing.BiTape Bool

Decode a two-sided tape from any word, inverting encBiTape encBool.

theorem Turing.MultiTapeTM.decodeBiTape_encBiTape (tape : Cslib.Turing.BiTape Bool) : decodeBiTape ((encBiTape encBool) tape) = tape

Decoding inverts the encoding of two-sided tapes.

theorem Turing.MultiTapeTM.dropFrame_iterate_encList {α : Type u_1} (enc : α ↪ List Bool) (values : List α) (n : ℕ) : dropFrame^[n] ((encList enc) values) = (encList enc) (List.drop n values)

Dropping n frames from an encoded list drops its first n elements.

noncomputable def Turing.MultiTapeTM.decodeTapes (k : ℕ) (word : List Bool) : Fin k → Cslib.Turing.BiTape Bool

Decode a family of k tapes from any word, inverting encPi (encBiTape encBool).

theorem Turing.MultiTapeTM.decodeTapes_encPi {k : ℕ} (tapes : Fin k → Cslib.Turing.BiTape Bool) : decodeTapes k ((encPi (encBiTape encBool)) tapes) = tapes

Decoding inverts the encoding of families of tapes.

noncomputable def Turing.MultiTapeTM.decodeState {State : Type} [Finite State] (n : ℕ) : Option State

Decode a control state from the length of its encoding by encFinite, clamped into range.

theorem Turing.MultiTapeTM.encFinite_decodeState {State : Type} [Finite State] (n : ℕ) : (encFinite (Option State)) (decodeState n) = encUnary (min n (Nat.card (Option State) - 1))

A decoded control state is encoded by the clamped count.

@[simp]

theorem Turing.MultiTapeTM.decodeState_length_encFinite {State : Type} [Finite State] (state : Option State) : decodeState ((encFinite (Option State)) state).length = state

Decoding inverts the encoding of control states.

noncomputable def Turing.MultiTapeTM.decodeFiniteCfg {k : ℕ} {State : Type} [Finite State] (word : List Bool) : FiniteCfg k Bool State

Decode a finite configuration from any word, inverting encFiniteCfg.

theorem Turing.MultiTapeTM.decodeFiniteCfg_encFiniteCfg {k : ℕ} {State : Type} [Finite State] (finite : FiniteCfg k Bool State) : decodeFiniteCfg (encFiniteCfg finite) = finite

Decoding inverts the encoding of finite configurations.

Decoding in polynomial time

theorem Turing.MultiTapeTM.ComputableInPolyTime.decodeStackTape : ComputableInPolyTime MultiTapeTM.decodeStackTape encBits (encStackTape encBool)

Decoding a stack tape is polynomial-time.

theorem Turing.MultiTapeTM.ComputableInPolyTime.decodeBiTape : ComputableInPolyTime MultiTapeTM.decodeBiTape encBits (encBiTape encBool)

Decoding a two-sided tape is polynomial-time.

theorem Turing.MultiTapeTM.ComputableInPolyTime.decodeTapes (k : ℕ) : ComputableInPolyTime (MultiTapeTM.decodeTapes k) encBits (encPi (encBiTape encBool))

Decoding a fixed finite family of tapes is polynomial-time.

theorem Turing.MultiTapeTM.ComputableInPolyTime.decodeFiniteCfg {k : ℕ} {State : Type} [Finite State] : ComputableInPolyTime MultiTapeTM.decodeFiniteCfg encBits encFiniteCfg

Decoding a finite configuration is polynomial-time.