StackTape: Infinite, eventually-none lists of Options

This file defines StackTape, a stack-like data structure of Option values, where the tape is considered to be infinite and eventually all nones. This is useful as a data structure with a simple API for manipulation by Turing machines.

Design

StackTape is represented as a list of Option values where the list cannot end with none. The end of the list is then treated as the start of an infinite sequence of none values by the low-level API. This design makes it convenient to express the length of the tape in terms of the list length.

An alternative design would be to represent the tape as a Stream' (Option Symbol), with additional fields tracking the length and the fact that the stream eventually becomes none. This design might complicate reasoning about the length of the tape, but could make other operations more straightforward.

Future design work might explore this alternative representation and compare its advantages and disadvantages.

TODO

• Make a ::-like notation.

structure Turing.StackTape (Symbol : Type) : Type

An infinite tape representation using a list of Option values, where the list is eventually none.

Represented as a List (Option Symbol) that does not end with none.

• toList : List (Option Symbol)

  The underlying list representation

• toList_getLast?_ne_some_none : self.toList.getLast? ≠ some none

  The list can be empty (i.e. none), but if it is not empty, the last element is not (some) none

def Turing.StackTape.nil {Symbol : Type} : StackTape Symbol

The empty StackTape

Equations

• Turing.StackTape.nil = { toList := [], toList_getLast?_ne_some_none := ⋯ }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[simp]

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

@[simp]

theorem Turing.StackTape.nil_toList {Symbol : Type} : nil.toList = []

def Turing.StackTape.cons {Symbol : Type} (x : Option Symbol) (xs : StackTape Symbol) : StackTape Symbol

Prepend an Option to the StackTape

Equations

• Turing.StackTape.cons none { toList := [], toList_getLast?_ne_some_none := toList_getLast?_ne_some_none } = { toList := [], toList_getLast?_ne_some_none := ⋯ }
• Turing.StackTape.cons none { toList := hd :: tl, toList_getLast?_ne_some_none := hl } = { toList := none :: hd :: tl, toList_getLast?_ne_some_none := ⋯ }
• Turing.StackTape.cons (some a) { toList := l, toList_getLast?_ne_some_none := hl } = { toList := some a :: l, toList_getLast?_ne_some_none := ⋯ }

@[simp]

theorem Turing.StackTape.cons_none_nil_toList {Symbol : Type} : (cons none nil).toList = []

@[simp]

theorem Turing.StackTape.cons_some_toList {Symbol : Type} (a : Symbol) (l : StackTape Symbol) : (cons (some a) l).toList = some a :: l.toList

def Turing.StackTape.tail {Symbol : Type} (l : StackTape Symbol) : StackTape Symbol

Remove the first element of the StackTape, returning the rest

Equations

• l.tail = match hl : l.toList with | [] => Turing.StackTape.nil | hd :: t => { toList := t, toList_getLast?_ne_some_none := ⋯ }

def Turing.StackTape.head {Symbol : Type} (l : StackTape Symbol) : Option Symbol

Get the first element of the StackTape.

Equations

• l.head = match l.toList with | [] => none | h :: tail => h

theorem Turing.StackTape.eq_iff {Symbol : Type} (l1 l2 : StackTape Symbol) : l1 = l2 ↔ l1.head = l2.head ∧ l1.tail = l2.tail

@[simp]

theorem Turing.StackTape.head_cons {Symbol : Type} (o : Option Symbol) (l : StackTape Symbol) : (cons o l).head = o

@[simp]

theorem Turing.StackTape.tail_cons {Symbol : Type} (o : Option Symbol) (l : StackTape Symbol) : (cons o l).tail = l

@[simp]

theorem Turing.StackTape.cons_head_tail {Symbol : Type} (l : StackTape Symbol) : cons l.head l.tail = l

def Turing.StackTape.map_some {Symbol : Type} (l : List Symbol) : StackTape Symbol

Create a StackTape from a list by mapping all elements to some

Equations

• Turing.StackTape.map_some l = { toList := List.map some l, toList_getLast?_ne_some_none := ⋯ }

def Turing.StackTape.length {Symbol : Type} (l : StackTape Symbol) : ℕ

The length of the StackTape is the number of elements up to the last non-none element

Equations

• l.length = l.toList.length

theorem Turing.StackTape.length_tail_le {Symbol : Type} (l : StackTape Symbol) : l.tail.length ≤ l.length

theorem Turing.StackTape.length_cons_none {Symbol : Type} (l : StackTape Symbol) : (cons none l).length = l.length + if l.length = 0 then 0 else 1

theorem Turing.StackTape.length_cons_some {Symbol : Type} (a : Symbol) (l : StackTape Symbol) : (cons (some a) l).length = l.length + 1

theorem Turing.StackTape.length_cons_le {Symbol : Type} (o : Option Symbol) (l : StackTape Symbol) : (cons o l).length ≤ l.length + 1

@[simp]

theorem Turing.StackTape.length_map_some {Symbol : Type} (l : List Symbol) : (map_some l).length = l.length

@[simp]

theorem Turing.StackTape.length_nil {Symbol : Type} : nil.length = 0