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.space_used: The space used by the tape

structure Turing.BiTape (Symbol : Type) : Type

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 Turing.BiTape.nil {Symbol : Type} : BiTape Symbol

The empty BiTape

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[simp]

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

def Turing.BiTape.mk₁ {Symbol : Type} (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

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

def Turing.BiTape.move_left {Symbol : Type} (t : BiTape Symbol) : BiTape Symbol

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

Equations

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

def Turing.BiTape.move_right {Symbol : Type} (t : BiTape Symbol) : BiTape Symbol

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

Equations

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

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

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

Equations

• t.move Turing.Dir.left = t.move_left
• t.move Turing.Dir.right = t.move_right

def Turing.BiTape.optionMove {Symbol : Type} : BiTape Symbol → Option 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 Turing.BiTape.move_left_move_right {Symbol : Type} (t : BiTape Symbol) : t.move_left.move_right = t

@[simp]

theorem Turing.BiTape.move_right_move_left {Symbol : Type} (t : BiTape Symbol) : t.move_right.move_left = t

def Turing.BiTape.write {Symbol : Type} (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 Turing.BiTape.space_used {Symbol : Type} (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.space_used = 1 + t.left.length + t.right.length

@[simp]

theorem Turing.BiTape.space_used_write {Symbol : Type} (t : BiTape Symbol) (a : Option Symbol) : (t.write a).space_used = t.space_used

theorem Turing.BiTape.space_used_mk₁ {Symbol : Type} (l : List Symbol) : (mk₁ l).space_used = max 1 l.length

theorem Turing.BiTape.space_used_move {Symbol : Type} (t : BiTape Symbol) (d : Dir) : (t.move d).space_used ≤ t.space_used + 1