Polynomial-time operations on finite tape storage

The operations of cslib's existing tapes are certified in plain polynomial time (Turing.MultiTapeTM.ComputableInPolyTime) by composition of list, option and pair operations. They charge the complete stored tapes and accept any symbol encoding, including infinite or empty alphabets. Finite-control interpreters can use these rules without building new tape machines.

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.stackTape_cons: prepend a computed cell, retaining the stack's omission of trailing blanks.
• Turing.MultiTapeTM.ComputableInPolyTime.biTape_moveLeft, .biTape_moveRight, .biTape_write, .biTape_step: native tape operations with fun_prop certificates.
• Turing.MultiTapeTM.ComputableInPolyTime.biTape_mk₁: load a computed list.

References

Adapts Computability/Probabilistic/Tape.lean from the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8 to plain polynomial time, using arbitrary symbol encodings instead of fixed finite tags.

theorem Turing.MultiTapeTM.ComputableInPolyTime.stackTape_toList {Symbol : Type} (enc : Symbol ↪ List Bool) : ComputableInPolyTime Cslib.Turing.StackTape.toList (encStackTape enc) (encList (encOption enc))

Reading the stored list is a change of view of the same encoded bits.

theorem Turing.MultiTapeTM.ComputableInPolyTime.stackTape_head {Symbol : Type} (enc : Symbol ↪ List Bool) : ComputableInPolyTime Cslib.Turing.StackTape.head (encStackTape enc) (encOption enc)

Reading a stack head decodes the first cell, with a blank default.

theorem Turing.MultiTapeTM.ComputableInPolyTime.stackTape_tail {Symbol : Type} (enc : Symbol ↪ List Bool) : ComputableInPolyTime Cslib.Turing.StackTape.tail (encStackTape enc) (encStackTape enc)

Removing a stack head is the list-tail operation.

theorem Turing.MultiTapeTM.ComputableInPolyTime.stackTape_cons {Symbol α : Type} {input : α ↪ List Bool} {enc : Symbol ↪ List Bool} {symbol : α → Option Symbol} {tape : α → Cslib.Turing.StackTape Symbol} (hsymbol : ComputableInPolyTime symbol input (encOption enc)) (htape : ComputableInPolyTime tape input (encStackTape enc)) : ComputableInPolyTime (fun (a : α) => Cslib.Turing.StackTape.cons (symbol a) (tape a)) input (encStackTape enc)

Prepend a cell without requiring a default symbol or case analysis over the alphabet.

theorem Turing.MultiTapeTM.ComputableInPolyTime.stackTape_mapSome {Symbol : Type} (enc : Symbol ↪ List Bool) : ComputableInPolyTime Cslib.Turing.StackTape.mapSome (encList enc) (encStackTape enc)

Map symbols to occupied cells with the list map.

theorem Turing.MultiTapeTM.ComputableInPolyTime.biTape_mk {Symbol α : Type} {input : α ↪ List Bool} {enc : Symbol ↪ List Bool} {head : α → Option Symbol} {left right : α → Cslib.Turing.StackTape Symbol} (hhead : ComputableInPolyTime head input (encOption enc)) (hleft : ComputableInPolyTime left input (encStackTape enc)) (hright : ComputableInPolyTime right input (encStackTape enc)) : ComputableInPolyTime (fun (a : α) => { head := head a, left := left a, right := right a }) input (encBiTape enc)

Assemble a tape from its computed head and two sides.

theorem Turing.MultiTapeTM.ComputableInPolyTime.biTape_head {Symbol : Type} (enc : Symbol ↪ List Bool) : ComputableInPolyTime Cslib.Turing.BiTape.head (encBiTape enc) (encOption enc)

Read the current cell of a computed tape.

theorem Turing.MultiTapeTM.ComputableInPolyTime.biTape_left {Symbol : Type} (enc : Symbol ↪ List Bool) : ComputableInPolyTime Cslib.Turing.BiTape.left (encBiTape enc) (encStackTape enc)

Extract the stored left side.

theorem Turing.MultiTapeTM.ComputableInPolyTime.biTape_right {Symbol : Type} (enc : Symbol ↪ List Bool) : ComputableInPolyTime Cslib.Turing.BiTape.right (encBiTape enc) (encStackTape enc)

Extract the stored right side.

theorem Turing.MultiTapeTM.ComputableInPolyTime.biTape_moveLeft {Symbol : Type} (enc : Symbol ↪ List Bool) : ComputableInPolyTime Cslib.Turing.BiTape.moveLeft (encBiTape enc) (encBiTape enc)

Move left by the stack operations.

theorem Turing.MultiTapeTM.ComputableInPolyTime.biTape_moveRight {Symbol : Type} (enc : Symbol ↪ List Bool) : ComputableInPolyTime Cslib.Turing.BiTape.moveRight (encBiTape enc) (encBiTape enc)

Move right by the stack operations.

theorem Turing.MultiTapeTM.ComputableInPolyTime.biTape_write {Symbol α : Type} {input : α ↪ List Bool} {enc : Symbol ↪ List Bool} {tape : α → Cslib.Turing.BiTape Symbol} {symbol : α → Option Symbol} (htape : ComputableInPolyTime tape input (encBiTape enc)) (hsymbol : ComputableInPolyTime symbol input (encOption enc)) : ComputableInPolyTime (fun (a : α) => (tape a).write (symbol a)) input (encBiTape enc)

Write a computed optional symbol, including blank erasure.

theorem Turing.MultiTapeTM.ComputableInPolyTime.biTape_step {Symbol α : Type} {input : α ↪ List Bool} {enc : Symbol ↪ List Bool} (action : Option (Option Symbol) × SignType) {tape : α → Cslib.Turing.BiTape Symbol} (htape : ComputableInPolyTime tape input (encBiTape enc)) : ComputableInPolyTime (fun (a : α) => (tape a).step action) input (encBiTape enc)

Execute a fixed native action, charging the full encoded tape.

theorem Turing.MultiTapeTM.ComputableInPolyTime.biTape_mk₁ {Symbol : Type} (enc : Symbol ↪ List Bool) : ComputableInPolyTime Cslib.Turing.BiTape.mk₁ (encList enc) (encBiTape enc)

Loading a list constructs a head and two stacks with no default symbol.