BiTape: Bidirectionally infinite TM tape representation using StackTape

This file defines BiTape, a tape representation for Turing machines in the form of an List of Option values, with the additional property that the list cannot end with none.

Design

Note that Mathlib has a Tape type, but it requires the alphabet type to be inhabited, and considers the ends of the tape to be filled with default values.

This design requires the tape elements to be Option values, and ensures that Lists of the base alphabet, rendered directly onto the tape by mapping over some, will not collide.

Main definitions

• BiTape: A tape with a head symbol and left/right contents stored as StackTape
• BiTape.move: Move the tape head left or right
• BiTape.write: Write a symbol at the current head position
• BiTape.spaceUsed: The space used by the tape

structure Cslib.Turing.BiTape (Symbol : Type u_1) : Type u_1

A structure for bidirectionally-infinite Turing machine tapes that eventually take on blank none values

• head : Option Symbol

  The symbol currently under the tape head

• left : StackTape Symbol

  The contents to the left of the head

• right : StackTape Symbol

  The contents to the right of the head

def Cslib.Turing.BiTape.nil {Symbol : Type u_1} : BiTape Symbol

The empty BiTape

Equations

• Cslib.Turing.BiTape.nil = { head := none, left := ∅, right := ∅ }

@[instance_reducible]

instance Cslib.Turing.BiTape.instInhabited {Symbol : Type u_1} : Inhabited (BiTape Symbol)

Equations

• Cslib.Turing.BiTape.instInhabited = { default := Cslib.Turing.BiTape.nil }

@[instance_reducible]

instance Cslib.Turing.BiTape.instEmptyCollection {Symbol : Type u_1} : EmptyCollection (BiTape Symbol)

Equations

• Cslib.Turing.BiTape.instEmptyCollection = { emptyCollection := Cslib.Turing.BiTape.nil }

@[simp]

theorem Cslib.Turing.BiTape.empty_eq_nil {Symbol : Type u_1} : ∅ = nil

def Cslib.Turing.BiTape.mk₁ {Symbol : Type u_1} (l : List Symbol) : BiTape Symbol

Given a List of Symbols, construct a BiTape by mapping the list to some elements and laying them out to the right side, with the head under the first element of the list if it exists.

Equations

• Cslib.Turing.BiTape.mk₁ [] = ∅
• Cslib.Turing.BiTape.mk₁ (h :: t) = { head := some h, left := ∅, right := Cslib.Turing.StackTape.mapSome t }

def Cslib.Turing.BiTape.moveLeft {Symbol : Type u_1} (t : BiTape Symbol) : BiTape Symbol

Move the head left by shifting the left StackTape under the head.

Equations

• t.moveLeft = { head := t.left.head, left := t.left.tail, right := Cslib.Turing.StackTape.cons t.head t.right }

def Cslib.Turing.BiTape.moveRight {Symbol : Type u_1} (t : BiTape Symbol) : BiTape Symbol

Move the head right by shifting the right StackTape under the head.

Equations

• t.moveRight = { head := t.right.head, left := Cslib.Turing.StackTape.cons t.head t.left, right := t.right.tail }

def Cslib.Turing.BiTape.move {Symbol : Type u_1} (t : BiTape Symbol) : Turing.Dir → BiTape Symbol

Move the head to the left or right, shifting the tape underneath it.

Equations

• t.move Turing.Dir.left = t.moveLeft
• t.move Turing.Dir.right = t.moveRight

def Cslib.Turing.BiTape.optionMove {Symbol : Type u_1} : BiTape Symbol → Option Turing.Dir → BiTape Symbol

Optionally perform a move, or do nothing if none.

Equations

• x✝.optionMove none = x✝
• x✝.optionMove (some d) = x✝.move d

@[simp]

theorem Cslib.Turing.BiTape.moveLeft_moveRight {Symbol : Type u_1} (t : BiTape Symbol) : t.moveLeft.moveRight = t

@[simp]

theorem Cslib.Turing.BiTape.moveRight_moveLeft {Symbol : Type u_1} (t : BiTape Symbol) : t.moveRight.moveLeft = t

def Cslib.Turing.BiTape.write {Symbol : Type u_1} (t : BiTape Symbol) (a : Option Symbol) : BiTape Symbol

Write a value under the head of the BiTape.

Equations

• t.write a = { head := a, left := t.left, right := t.right }

def Cslib.Turing.BiTape.spaceUsed {Symbol : Type u_1} (t : BiTape Symbol) : ℕ

The space used by a BiTape is the number of symbols between and including the head, and leftmost and rightmost non-blank symbols on the BiTape.

Equations

• t.spaceUsed = 1 + t.left.length + t.right.length

@[simp]

theorem Cslib.Turing.BiTape.spaceUsed_write {Symbol : Type u_1} (t : BiTape Symbol) (a : Option Symbol) : (t.write a).spaceUsed = t.spaceUsed

theorem Cslib.Turing.BiTape.spaceUsed_mk₁ {Symbol : Type u_1} (l : List Symbol) : (mk₁ l).spaceUsed = max 1 l.length

theorem Cslib.Turing.BiTape.spaceUsed_move {Symbol : Type u_1} (t : BiTape Symbol) (d : Turing.Dir) : (t.move d).spaceUsed ≤ t.spaceUsed + 1