Documentation

Complexity.Computability.Machines.Turing.MultiTape.Encodings.Tape

Encodings of finite tape storage #

The existing stack and bidirectional tapes use the standard list, option and pair encodings. The symbol encoding is a parameter: the operations do not require a finite or inhabited alphabet. If symbol encodings have a uniform length bound, the complete tape encoding is linear in its stored extent, including blank gaps.

Main definitions #

Main results #

References #

Adapts the encodings in Computability/Probabilistic/Tape.lean on the cslib crypto branch at 5ff69ca93402e7c947208dc56396d6d86203ccd8, using Christian Reitwiessner's standard encodings and Bolton Bailey's tape representations.

source
def Turing.MultiTapeTM.encStackTape {Symbol : Type} (enc : Symbol ↪ List Bool) :
Cslib.Turing.StackTape Symbol ↪ List Bool

Encode the finite stored list, retaining interior blank cells.

Instances For
    source
    @[simp]
    theorem Turing.MultiTapeTM.encStackTape_apply {Symbol : Type} (enc : Symbol ↪ List Bool) (tape : Cslib.Turing.StackTape Symbol) :
    (encStackTape enc) tape = (encList (encOption enc)) tape.toList
    source
    def Turing.MultiTapeTM.encBiTape {Symbol : Type} (enc : Symbol ↪ List Bool) :
    Cslib.Turing.BiTape Symbol ↪ List Bool

    Encode the current cell, left side and right side with their standard framing.

    Instances For
      source
      @[simp]
      theorem Turing.MultiTapeTM.encBiTape_apply {Symbol : Type} (enc : Symbol ↪ List Bool) (tape : Cslib.Turing.BiTape Symbol) :
      (encBiTape enc) tape = (encPair (encOption enc) (encPair (encStackTape enc) (encStackTape enc))) (tape.head, tape.left, tape.right)
      source
      theorem Turing.MultiTapeTM.length_encStackTape_le {Symbol : Type} (enc : Symbol ↪ List Bool) (tape : Cslib.Turing.StackTape Symbol) {bound : ℕ} (hbound : ∀ (symbol : Symbol), (enc symbol).length ≤ bound) :
      ((encStackTape enc) tape).length ≤ tape.length * (2 * bound + 3)

      Bounded symbol encodings give a linear bound for the stored stack.

      source
      theorem Turing.MultiTapeTM.length_encBiTape_le {Symbol : Type} (enc : Symbol ↪ List Bool) (tape : Cslib.Turing.BiTape Symbol) {bound : ℕ} (hbound : ∀ (symbol : Symbol), (enc symbol).length ≤ bound) :
      ((encBiTape enc) tape).length ≤ 4 * (bound + 2) * tape.spaceUsed

      The encoding charges all stored cells, including blanks between nonblank cells.