Raw two-stack work tapes

A work tape is stored as its current cell and two lists, nearest cell first. Blanks are retained: moving beyond the stored interval extends it by one blank cell. Thus storage records the interval visited by the head, independently of the number of times the machine revisits cells. The relative read and representation proofs adapt the BiTape API of Bolton Bailey and Samuel Schlesinger to raw lists.

Main definitions

• Turing.MultiTapeTM.ToTM2.RawTape: the current cell and the raw left and right stacks.
• Turing.MultiTapeTM.ToTM2.RawTape.step: native optional writing followed by head movement.
• Turing.MultiTapeTM.ToTM2.RawTape.Represents: correspondence with an integer-indexed native tape.

Main results

• Turing.MultiTapeTM.ToTM2.RawTape.Represents.step: preservation of native tape semantics.

structure Turing.MultiTapeTM.ToTM2.RawTape (Symbol : Type u_1) : Type u_1

A work tape with raw stacks, ordered from the head outwards. Trailing blanks are retained.

• head : Option Symbol

  The cell under the head.

• left : List (Option Symbol)

  Cells strictly to the left, nearest first.

• right : List (Option Symbol)

  Cells strictly to the right, nearest first.

theorem Turing.MultiTapeTM.ToTM2.RawTape.ext {Symbol : Type u_1} {x y : RawTape Symbol} (head : x.head = y.head) (left : x.left = y.left) (right : x.right = y.right) : x = y

theorem Turing.MultiTapeTM.ToTM2.RawTape.ext_iff {Symbol : Type u_1} {x y : RawTape Symbol} : x = y ↔ x.head = y.head ∧ x.left = y.left ∧ x.right = y.right

@[instance_reducible]

instance Turing.MultiTapeTM.ToTM2.instDecidableEqRawTape {Symbol✝ : Type u_1} [DecidableEq Symbol✝] : DecidableEq (RawTape Symbol✝)

def Turing.MultiTapeTM.ToTM2.instDecidableEqRawTape.decEq {Symbol✝ : Type u_1} [DecidableEq Symbol✝] (x✝ x✝¹ : RawTape Symbol✝) : Decidable (x✝ = x✝¹)

def Turing.MultiTapeTM.ToTM2.RawTape.init {Symbol : Type u_1} : RawTape Symbol

A blank tape, initially storing just the cell at its head.

@[instance_reducible]

instance Turing.MultiTapeTM.ToTM2.RawTape.instInhabited {Symbol : Type u_1} : Inhabited (RawTape Symbol)

def Turing.MultiTapeTM.ToTM2.RawTape.write {Symbol : Type u_1} (t : RawTape Symbol) (w : Option (Option Symbol)) : RawTape Symbol

Perform an optional native write: none preserves the cell and some none erases it.

@[simp]

theorem Turing.MultiTapeTM.ToTM2.RawTape.write_none {Symbol : Type u_1} (t : RawTape Symbol) : t.write none = t

@[simp]

theorem Turing.MultiTapeTM.ToTM2.RawTape.head_write {Symbol : Type u_1} (t : RawTape Symbol) (w : Option (Option Symbol)) : (t.write w).head = w.getD t.head

def Turing.MultiTapeTM.ToTM2.RawTape.moveLeft {Symbol : Type u_1} (t : RawTape Symbol) : RawTape Symbol

Move left, extending the stored interval by a blank when the left stack is empty.

def Turing.MultiTapeTM.ToTM2.RawTape.moveRight {Symbol : Type u_1} (t : RawTape Symbol) : RawTape Symbol

Move right, extending the stored interval by a blank when the right stack is empty.

def Turing.MultiTapeTM.ToTM2.RawTape.step {Symbol : Type u_1} (t : RawTape Symbol) (a : Option (Option Symbol) × SignType) : RawTape Symbol

Apply a native work-tape action, writing before moving.

def Turing.MultiTapeTM.ToTM2.RawTape.read {Symbol : Type u_1} (t : RawTape Symbol) : ℤ → Option Symbol

Read at an integer offset relative to the head; unstored cells are blank.

def Turing.MultiTapeTM.ToTM2.RawTape.Represents {Symbol : Type u_1} (t : RawTape Symbol) (native : ℤ → Option Symbol) (pos : ℤ) : Prop

The raw tape agrees with a native tape whose head is at pos.

@[simp]

theorem Turing.MultiTapeTM.ToTM2.RawTape.read_zero {Symbol : Type u_1} (t : RawTape Symbol) : t.read 0 = t.head

@[simp]

theorem Turing.MultiTapeTM.ToTM2.RawTape.read_init {Symbol : Type u_1} (z : ℤ) : init.read z = none

theorem Turing.MultiTapeTM.ToTM2.RawTape.read_write {Symbol : Type u_1} (t : RawTape Symbol) (w : Option (Option Symbol)) (z : ℤ) : (t.write w).read z = if z = 0 then w.getD t.head else t.read z

theorem Turing.MultiTapeTM.ToTM2.RawTape.read_moveLeft {Symbol : Type u_1} (t : RawTape Symbol) (z : ℤ) : t.moveLeft.read z = t.read (z - 1)

theorem Turing.MultiTapeTM.ToTM2.RawTape.read_moveRight {Symbol : Type u_1} (t : RawTape Symbol) (z : ℤ) : t.moveRight.read z = t.read (z + 1)

theorem Turing.MultiTapeTM.ToTM2.RawTape.Represents.head {Symbol : Type u_1} {t : RawTape Symbol} {native : ℤ → Option Symbol} {pos : ℤ} (h : t.Represents native pos) : t.head = native pos

theorem Turing.MultiTapeTM.ToTM2.RawTape.Represents.init {Symbol : Type u_1} : RawTape.init.Represents (fun (x : ℤ) => none) 0

theorem Turing.MultiTapeTM.ToTM2.RawTape.Represents.write {Symbol : Type u_1} {t : RawTape Symbol} {native : ℤ → Option Symbol} {pos : ℤ} (h : t.Represents native pos) (w : Option (Option Symbol)) : (t.write w).Represents (match (motive := Option (Option Symbol) → ℤ → Option Symbol) w with | none => native | some s => Function.update native pos s) pos

theorem Turing.MultiTapeTM.ToTM2.RawTape.Represents.moveLeft {Symbol : Type u_1} {t : RawTape Symbol} {native : ℤ → Option Symbol} {pos : ℤ} (h : t.Represents native pos) : t.moveLeft.Represents native (pos - 1)

theorem Turing.MultiTapeTM.ToTM2.RawTape.Represents.moveRight {Symbol : Type u_1} {t : RawTape Symbol} {native : ℤ → Option Symbol} {pos : ℤ} (h : t.Represents native pos) : t.moveRight.Represents native (pos + 1)

theorem Turing.MultiTapeTM.ToTM2.RawTape.Represents.step {Symbol : Type u_1} {t : RawTape Symbol} {native : ℤ → Option Symbol} {pos : ℤ} (h : t.Represents native pos) (a : Option (Option Symbol) × SignType) : (t.step a).Represents (match (motive := Option (Option Symbol) → ℤ → Option Symbol) a.1 with | none => native | some s => Function.update native pos s) (pos + ↑a.2)

Raw execution preserves a native optional-write-and-move action, including erasing cells.

@[simp]

theorem Turing.MultiTapeTM.ToTM2.RawTape.left_write {Symbol : Type u_1} (t : RawTape Symbol) (w : Option (Option Symbol)) : (t.write w).left = t.left

@[simp]

theorem Turing.MultiTapeTM.ToTM2.RawTape.right_write {Symbol : Type u_1} (t : RawTape Symbol) (w : Option (Option Symbol)) : (t.write w).right = t.right

@[simp]

theorem Turing.MultiTapeTM.ToTM2.RawTape.length_left_moveLeft {Symbol : Type u_1} (t : RawTape Symbol) : t.moveLeft.left.length = t.left.length - 1

@[simp]

theorem Turing.MultiTapeTM.ToTM2.RawTape.length_right_moveLeft {Symbol : Type u_1} (t : RawTape Symbol) : t.moveLeft.right.length = t.right.length + 1

@[simp]

theorem Turing.MultiTapeTM.ToTM2.RawTape.length_left_moveRight {Symbol : Type u_1} (t : RawTape Symbol) : t.moveRight.left.length = t.left.length + 1

@[simp]

theorem Turing.MultiTapeTM.ToTM2.RawTape.length_right_moveRight {Symbol : Type u_1} (t : RawTape Symbol) : t.moveRight.right.length = t.right.length - 1

theorem Turing.MultiTapeTM.ToTM2.RawTape.length_left_step {Symbol : Type u_1} (t : RawTape Symbol) (a : Option (Option Symbol) × SignType) : (t.step a).left.length = match a.2 with | SignType.neg => t.left.length - 1 | SignType.zero => t.left.length | SignType.pos => t.left.length + 1

The exact left-stack length after an action.

theorem Turing.MultiTapeTM.ToTM2.RawTape.length_right_step {Symbol : Type u_1} (t : RawTape Symbol) (a : Option (Option Symbol) × SignType) : (t.step a).right.length = match a.2 with | SignType.neg => t.right.length + 1 | SignType.zero => t.right.length | SignType.pos => t.right.length - 1

The exact right-stack length after an action.

def Turing.MultiTapeTM.ToTM2.RawTape.span {Symbol : Type u_1} (t : RawTape Symbol) : ℕ

The number of stored cells, including the current cell and stored blanks.

@[simp]

theorem Turing.MultiTapeTM.ToTM2.RawTape.span_init {Symbol : Type u_1} : init.span = 1

@[simp]

theorem Turing.MultiTapeTM.ToTM2.RawTape.span_write {Symbol : Type u_1} (t : RawTape Symbol) (w : Option (Option Symbol)) : (t.write w).span = t.span

theorem Turing.MultiTapeTM.ToTM2.RawTape.span_step {Symbol : Type u_1} (t : RawTape Symbol) (a : Option (Option Symbol) × SignType) : (t.step a).span = t.span + if a.2 = SignType.neg ∧ t.left = [] ∨ a.2 = SignType.pos ∧ t.right = [] then 1 else 0

Storage grows only when the head moves beyond the previously stored interval.

theorem Turing.MultiTapeTM.ToTM2.RawTape.span_step_le {Symbol : Type u_1} (t : RawTape Symbol) (a : Option (Option Symbol) × SignType) : (t.step a).span ≤ t.span + 1