Turing machine tapes

This file defines the notion of a Turing machine tape, and the operations on it. A tape is a bidirectional infinite sequence of cells, each of which stores an element of a given alphabet Γ. All but finitely many of the cells are required to hold the blank symbol default : Γ.

Main definitions

• ListBlank Γ is the type of one-directional tapes with alphabet Γ. Implemented as a quotient of List Γ by extension by blanks at the end.
• Tape Γ is the type of Turing machine tapes with alphabet Γ. Implemented as two ListBlank Γ instances, one for each direction, as well as a head symbol.

def Turing.BlankExtends {Γ : Type u_1} [Inhabited Γ] (l₁ l₂ : List Γ) : Prop

The BlankExtends partial order holds of l₁ and l₂ if l₂ is obtained by adding blanks (default : Γ) to the end of l₁.

theorem Turing.BlankExtends.refl {Γ : Type u_1} [Inhabited Γ] (l : List Γ) : BlankExtends l l

theorem Turing.BlankExtends.trans {Γ : Type u_1} [Inhabited Γ] {l₁ l₂ l₃ : List Γ} : BlankExtends l₁ l₂ → BlankExtends l₂ l₃ → BlankExtends l₁ l₃

theorem Turing.BlankExtends.below_of_le {Γ : Type u_1} [Inhabited Γ] {l l₁ l₂ : List Γ} : BlankExtends l l₁ → BlankExtends l l₂ → l₁.length ≤ l₂.length → BlankExtends l₁ l₂

def Turing.BlankExtends.above {Γ : Type u_1} [Inhabited Γ] {l l₁ l₂ : List Γ} (h₁ : BlankExtends l l₁) (h₂ : BlankExtends l l₂) : { l' : List Γ // BlankExtends l₁ l' ∧ BlankExtends l₂ l' }

Any two extensions by blank l₁,l₂ of l have a common join (which can be taken to be the longer of l₁ and l₂).

theorem Turing.BlankExtends.above_of_le {Γ : Type u_1} [Inhabited Γ] {l l₁ l₂ : List Γ} : BlankExtends l₁ l → BlankExtends l₂ l → l₁.length ≤ l₂.length → BlankExtends l₁ l₂

def Turing.BlankRel {Γ : Type u_1} [Inhabited Γ] (l₁ l₂ : List Γ) : Prop

BlankRel is the symmetric closure of BlankExtends, turning it into an equivalence relation. Two lists are related by BlankRel if one extends the other by blanks.

theorem Turing.BlankRel.refl {Γ : Type u_1} [Inhabited Γ] (l : List Γ) : BlankRel l l

theorem Turing.BlankRel.symm {Γ : Type u_1} [Inhabited Γ] {l₁ l₂ : List Γ} : BlankRel l₁ l₂ → BlankRel l₂ l₁

theorem Turing.BlankRel.trans {Γ : Type u_1} [Inhabited Γ] {l₁ l₂ l₃ : List Γ} : BlankRel l₁ l₂ → BlankRel l₂ l₃ → BlankRel l₁ l₃

def Turing.BlankRel.above {Γ : Type u_1} [Inhabited Γ] {l₁ l₂ : List Γ} (h : BlankRel l₁ l₂) : { l : List Γ // BlankExtends l₁ l ∧ BlankExtends l₂ l }

Given two BlankRel lists, there exists (constructively) a common join.

def Turing.BlankRel.below {Γ : Type u_1} [Inhabited Γ] {l₁ l₂ : List Γ} (h : BlankRel l₁ l₂) : { l : List Γ // BlankExtends l l₁ ∧ BlankExtends l l₂ }

Given two BlankRel lists, there exists (constructively) a common meet.

theorem Turing.BlankRel.equivalence (Γ : Type u_1) [Inhabited Γ] : Equivalence BlankRel

@[implicit_reducible]

def Turing.BlankRel.setoid (Γ : Type u_1) [Inhabited Γ] : Setoid (List Γ)

Construct a setoid instance for BlankRel.

def Turing.ListBlank (Γ : Type u_1) [Inhabited Γ] : Type u_1

A ListBlank Γ is a quotient of List Γ by extension by blanks at the end. This is used to represent half-tapes of a Turing machine, so that we can pretend that the list continues infinitely with blanks.

@[implicit_reducible]

instance Turing.ListBlank.inhabited {Γ : Type u_1} [Inhabited Γ] : Inhabited (ListBlank Γ)

@[implicit_reducible]

instance Turing.ListBlank.hasEmptyc {Γ : Type u_1} [Inhabited Γ] : EmptyCollection (ListBlank Γ)

@[reducible, inline]

abbrev Turing.ListBlank.liftOn {Γ : Type u_1} [Inhabited Γ] {α : Sort u_2} (l : ListBlank Γ) (f : List Γ → α) (H : ∀ (a b : List Γ), BlankExtends a b → f a = f b) : α

A modified version of Quotient.liftOn' specialized for ListBlank, with the stronger precondition BlankExtends instead of BlankRel.

def Turing.ListBlank.mk {Γ : Type u_1} [Inhabited Γ] : List Γ → ListBlank Γ

The quotient map turning a List into a ListBlank.

theorem Turing.ListBlank.induction_on {Γ : Type u_1} [Inhabited Γ] {p : ListBlank Γ → Prop} (q : ListBlank Γ) (h : ∀ (a : List Γ), p (mk a)) : p q

def Turing.ListBlank.head {Γ : Type u_1} [Inhabited Γ] (l : ListBlank Γ) : Γ

The head of a ListBlank is well defined.

@[simp]

theorem Turing.ListBlank.head_mk {Γ : Type u_1} [Inhabited Γ] (l : List Γ) : (mk l).head = l.headI

def Turing.ListBlank.tail {Γ : Type u_1} [Inhabited Γ] (l : ListBlank Γ) : ListBlank Γ

The tail of a ListBlank is well defined (up to the tail of blanks).

@[simp]

theorem Turing.ListBlank.tail_mk {Γ : Type u_1} [Inhabited Γ] (l : List Γ) : (mk l).tail = mk l.tail

def Turing.ListBlank.cons {Γ : Type u_1} [Inhabited Γ] (a : Γ) (l : ListBlank Γ) : ListBlank Γ

We can cons an element onto a ListBlank.

@[simp]

theorem Turing.ListBlank.cons_mk {Γ : Type u_1} [Inhabited Γ] (a : Γ) (l : List Γ) : cons a (mk l) = mk (a :: l)

@[simp]

theorem Turing.ListBlank.head_cons {Γ : Type u_1} [Inhabited Γ] (a : Γ) (l : ListBlank Γ) : (cons a l).head = a

@[simp]

theorem Turing.ListBlank.tail_cons {Γ : Type u_1} [Inhabited Γ] (a : Γ) (l : ListBlank Γ) : (cons a l).tail = l

@[simp]

theorem Turing.ListBlank.cons_head_tail {Γ : Type u_1} [Inhabited Γ] (l : ListBlank Γ) : cons l.head l.tail = l

The cons and head/tail functions are mutually inverse, unlike in the case of List where this only holds for nonempty lists.

theorem Turing.ListBlank.exists_cons {Γ : Type u_1} [Inhabited Γ] (l : ListBlank Γ) : ∃ (a : Γ) (l' : ListBlank Γ), l = cons a l'

The cons and head/tail functions are mutually inverse, unlike in the case of List where this only holds for nonempty lists.

def Turing.ListBlank.nth {Γ : Type u_1} [Inhabited Γ] (l : ListBlank Γ) (n : ℕ) : Γ

The n-th element of a ListBlank is well defined for all n : ℕ, unlike in a List.

@[simp]

theorem Turing.ListBlank.nth_mk {Γ : Type u_1} [Inhabited Γ] (l : List Γ) (n : ℕ) : (mk l).nth n = l.getI n

@[simp]

theorem Turing.ListBlank.nth_zero {Γ : Type u_1} [Inhabited Γ] (l : ListBlank Γ) : l.nth 0 = l.head

@[simp]

theorem Turing.ListBlank.nth_succ {Γ : Type u_1} [Inhabited Γ] (l : ListBlank Γ) (n : ℕ) : l.nth (n + 1) = l.tail.nth n

theorem Turing.ListBlank.ext {Γ : Type u_1} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} : (∀ (i_1 : ℕ), L₁.nth i_1 = L₂.nth i_1) → L₁ = L₂

theorem Turing.ListBlank.ext_iff {Γ : Type u_1} [i : Inhabited Γ] {L₁ L₂ : ListBlank Γ} : L₁ = L₂ ↔ ∀ (i_1 : ℕ), L₁.nth i_1 = L₂.nth i_1

def Turing.ListBlank.modifyNth {Γ : Type u_1} [Inhabited Γ] (f : Γ → Γ) : ℕ → ListBlank Γ → ListBlank Γ

Apply a function to a value stored at the nth position of the list.

theorem Turing.ListBlank.nth_modifyNth {Γ : Type u_1} [Inhabited Γ] (f : Γ → Γ) (n i : ℕ) (L : ListBlank Γ) : (modifyNth f n L).nth i = if i = n then f (L.nth i) else L.nth i

structure Turing.PointedMap (Γ : Type u) (Γ' : Type v) [Inhabited Γ] [Inhabited Γ'] : Type (max u v)

A pointed map of Inhabited types is a map that sends one default value to the other.

• f : Γ → Γ'

  The map underlying this instance.

• map_pt' : self.f default = default

@[implicit_reducible]

instance Turing.instInhabitedPointedMap {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] : Inhabited (PointedMap Γ Γ')

@[implicit_reducible]

instance Turing.instCoeFunPointedMapForall {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] : CoeFun (PointedMap Γ Γ') fun (x : PointedMap Γ Γ') => Γ → Γ'

theorem Turing.PointedMap.mk_val {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : Γ → Γ') (pt : f default = default) : { f := f, map_pt' := pt }.f = f

@[simp]

theorem Turing.PointedMap.map_pt {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') : f.f default = default

@[simp]

theorem Turing.PointedMap.headI_map {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (l : List Γ) : (List.map f.f l).headI = f.f l.headI

def Turing.ListBlank.map {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (l : ListBlank Γ) : ListBlank Γ'

The map function on lists is well defined on ListBlanks provided that the map is pointed.

@[simp]

theorem Turing.ListBlank.map_mk {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (l : List Γ) : map f (mk l) = mk (List.map f.f l)

@[simp]

theorem Turing.ListBlank.head_map {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (l : ListBlank Γ) : (map f l).head = f.f l.head

@[simp]

theorem Turing.ListBlank.tail_map {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (l : ListBlank Γ) : (map f l).tail = map f l.tail

@[simp]

theorem Turing.ListBlank.map_cons {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (l : ListBlank Γ) (a : Γ) : map f (cons a l) = cons (f.f a) (map f l)

@[simp]

theorem Turing.ListBlank.nth_map {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (l : ListBlank Γ) (n : ℕ) : (map f l).nth n = f.f (l.nth n)

def Turing.proj {ι : Type u_1} {Γ : ι → Type u_2} [(i : ι) → Inhabited (Γ i)] (i : ι) : PointedMap ((i : ι) → Γ i) (Γ i)

The i-th projection as a pointed map.

theorem Turing.proj_map_nth {ι : Type u_1} {Γ : ι → Type u_2} [(i : ι) → Inhabited (Γ i)] (i : ι) (L : ListBlank ((i : ι) → Γ i)) (n : ℕ) : (ListBlank.map (proj i) L).nth n = L.nth n i

theorem Turing.ListBlank.map_modifyNth {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (F : PointedMap Γ Γ') (f : Γ → Γ) (f' : Γ' → Γ') (H : ∀ (x : Γ), F.f (f x) = f' (F.f x)) (n : ℕ) (L : ListBlank Γ) : map F (modifyNth f n L) = modifyNth f' n (map F L)

def Turing.ListBlank.append {Γ : Type u_1} [Inhabited Γ] : List Γ → ListBlank Γ → ListBlank Γ

Append a list on the left side of a ListBlank.

@[simp]

theorem Turing.ListBlank.append_mk {Γ : Type u_1} [Inhabited Γ] (l₁ l₂ : List Γ) : append l₁ (mk l₂) = mk (l₁ ++ l₂)

theorem Turing.ListBlank.append_assoc {Γ : Type u_1} [Inhabited Γ] (l₁ l₂ : List Γ) (l₃ : ListBlank Γ) : append (l₁ ++ l₂) l₃ = append l₁ (append l₂ l₃)

def Turing.ListBlank.flatMap {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (l : ListBlank Γ) (f : Γ → List Γ') (hf : ∃ (n : ℕ), f default = List.replicate n default) : ListBlank Γ'

The flatMap function on lists is well defined on ListBlanks provided that the default element is sent to a sequence of default elements.

@[simp]

theorem Turing.ListBlank.flatMap_mk {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (l : List Γ) (f : Γ → List Γ') (hf : ∃ (n : ℕ), f default = List.replicate n default) : (mk l).flatMap f hf = mk (List.flatMap f l)

@[simp]

theorem Turing.ListBlank.cons_flatMap {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (a : Γ) (l : ListBlank Γ) (f : Γ → List Γ') (hf : ∃ (n : ℕ), f default = List.replicate n default) : (cons a l).flatMap f hf = append (f a) (l.flatMap f hf)

structure Turing.Tape (Γ : Type u_1) [Inhabited Γ] : Type u_1

The tape of a Turing machine is composed of a head element (which we imagine to be the current position of the head), together with two ListBlanks denoting the portions of the tape going off to the left and right. When the Turing machine moves right, an element is pulled from the right side and becomes the new head, while the head element is consed onto the left side.

• head : Γ

  The current position of the head.

• left : ListBlank Γ

  The portion of the tape going off to the left.

• right : ListBlank Γ

  The portion of the tape going off to the right.

@[implicit_reducible]

instance Turing.Tape.inhabited {Γ : Type u_1} [Inhabited Γ] : Inhabited (Tape Γ)

inductive Turing.Dir : Type

A direction for the Turing machine move command, either left or right.

• left : Dir
• right : Dir

@[implicit_reducible]

instance Turing.instDecidableEqDir : DecidableEq Dir

def Turing.instInhabitedDir.default : Dir

@[implicit_reducible]

instance Turing.instInhabitedDir : Inhabited Dir

def Turing.Tape.left₀ {Γ : Type u_1} [Inhabited Γ] (T : Tape Γ) : ListBlank Γ

The "inclusive" left side of the tape, including both left and head.

def Turing.Tape.right₀ {Γ : Type u_1} [Inhabited Γ] (T : Tape Γ) : ListBlank Γ

The "inclusive" right side of the tape, including both right and head.

def Turing.Tape.move {Γ : Type u_1} [Inhabited Γ] : Dir → Tape Γ → Tape Γ

Move the tape in response to a motion of the Turing machine. Note that T.move Dir.left makes T.left smaller; the Turing machine is moving left and the tape is moving right.

@[simp]

theorem Turing.Tape.move_left_right {Γ : Type u_1} [Inhabited Γ] (T : Tape Γ) : move Dir.right (move Dir.left T) = T

@[simp]

theorem Turing.Tape.move_right_left {Γ : Type u_1} [Inhabited Γ] (T : Tape Γ) : move Dir.left (move Dir.right T) = T

def Turing.Tape.mk' {Γ : Type u_1} [Inhabited Γ] (L R : ListBlank Γ) : Tape Γ

Construct a tape from a left side and an inclusive right side.

@[simp]

theorem Turing.Tape.mk'_left {Γ : Type u_1} [Inhabited Γ] (L R : ListBlank Γ) : (mk' L R).left = L

@[simp]

theorem Turing.Tape.mk'_head {Γ : Type u_1} [Inhabited Γ] (L R : ListBlank Γ) : (mk' L R).head = R.head

@[simp]

theorem Turing.Tape.mk'_right {Γ : Type u_1} [Inhabited Γ] (L R : ListBlank Γ) : (mk' L R).right = R.tail

@[simp]

theorem Turing.Tape.mk'_right₀ {Γ : Type u_1} [Inhabited Γ] (L R : ListBlank Γ) : (mk' L R).right₀ = R

@[simp]

theorem Turing.Tape.mk'_left_right₀ {Γ : Type u_1} [Inhabited Γ] (T : Tape Γ) : mk' T.left T.right₀ = T

theorem Turing.Tape.exists_mk' {Γ : Type u_1} [Inhabited Γ] (T : Tape Γ) : ∃ (L : ListBlank Γ) (R : ListBlank Γ), T = mk' L R

@[simp]

theorem Turing.Tape.move_left_mk' {Γ : Type u_1} [Inhabited Γ] (L R : ListBlank Γ) : move Dir.left (mk' L R) = mk' L.tail (ListBlank.cons L.head R)

@[simp]

theorem Turing.Tape.move_right_mk' {Γ : Type u_1} [Inhabited Γ] (L R : ListBlank Γ) : move Dir.right (mk' L R) = mk' (ListBlank.cons R.head L) R.tail

def Turing.Tape.mk₂ {Γ : Type u_1} [Inhabited Γ] (L R : List Γ) : Tape Γ

Construct a tape from a left side and an inclusive right side.

def Turing.Tape.mk₁ {Γ : Type u_1} [Inhabited Γ] (l : List Γ) : Tape Γ

Construct a tape from a list, with the head of the list at the TM head and the rest going to the right.

def Turing.Tape.nth {Γ : Type u_1} [Inhabited Γ] (T : Tape Γ) : ℤ → Γ

The nth function of a tape is integer-valued, with index 0 being the head, negative indexes on the left and positive indexes on the right. (Picture a number line.)

@[simp]

theorem Turing.Tape.nth_zero {Γ : Type u_1} [Inhabited Γ] (T : Tape Γ) : T.nth 0 = T.head

theorem Turing.Tape.right₀_nth {Γ : Type u_1} [Inhabited Γ] (T : Tape Γ) (n : ℕ) : T.right₀.nth n = T.nth ↑n

@[simp]

theorem Turing.Tape.mk'_nth_nat {Γ : Type u_1} [Inhabited Γ] (L R : ListBlank Γ) (n : ℕ) : (mk' L R).nth ↑n = R.nth n

@[simp]

theorem Turing.Tape.move_left_nth {Γ : Type u_1} [Inhabited Γ] (T : Tape Γ) (i : ℤ) : (move Dir.left T).nth i = T.nth (i - 1)

@[simp]

theorem Turing.Tape.move_right_nth {Γ : Type u_1} [Inhabited Γ] (T : Tape Γ) (i : ℤ) : (move Dir.right T).nth i = T.nth (i + 1)

@[simp]

theorem Turing.Tape.move_right_n_head {Γ : Type u_1} [Inhabited Γ] (T : Tape Γ) (i : ℕ) : ((move Dir.right)^[i] T).head = T.nth ↑i

def Turing.Tape.write {Γ : Type u_1} [Inhabited Γ] (b : Γ) (T : Tape Γ) : Tape Γ

Replace the current value of the head on the tape.

@[simp]

theorem Turing.Tape.write_self {Γ : Type u_1} [Inhabited Γ] (T : Tape Γ) : write T.head T = T

@[simp]

theorem Turing.Tape.write_nth {Γ : Type u_1} [Inhabited Γ] (b : Γ) (T : Tape Γ) {i : ℤ} : (write b T).nth i = if i = 0 then b else T.nth i

@[simp]

theorem Turing.Tape.write_mk {Γ : Type u_1} [Inhabited Γ] (a b : Γ) (L R : ListBlank Γ) : write b { head := a, left := L, right := R } = { head := b, left := L, right := R }

@[simp]

theorem Turing.Tape.write_mk' {Γ : Type u_1} [Inhabited Γ] (b : Γ) (L R : ListBlank Γ) : write b (mk' L R) = mk' L (ListBlank.cons b R.tail)

def Turing.Tape.map {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (T : Tape Γ) : Tape Γ'

Apply a pointed map to a tape to change the alphabet.

@[simp]

theorem Turing.Tape.map_fst {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (T : Tape Γ) : (map f T).head = f.f T.head

@[simp]

theorem Turing.Tape.map_write {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (b : Γ) (T : Tape Γ) : map f (write b T) = write (f.f b) (map f T)

@[simp]

theorem Turing.Tape.write_move_right_n {Γ : Type u_1} [Inhabited Γ] (f : Γ → Γ) (L R : ListBlank Γ) (n : ℕ) : write (f (R.nth n)) ((move Dir.right)^[n] (mk' L R)) = (move Dir.right)^[n] (mk' L (ListBlank.modifyNth f n R))

theorem Turing.Tape.map_move {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (T : Tape Γ) (d : Dir) : map f (move d T) = move d (map f T)

theorem Turing.Tape.map_mk' {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (L R : ListBlank Γ) : map f (mk' L R) = mk' (ListBlank.map f L) (ListBlank.map f R)

theorem Turing.Tape.map_mk₂ {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (L R : List Γ) : map f (mk₂ L R) = mk₂ (List.map f.f L) (List.map f.f R)

theorem Turing.Tape.map_mk₁ {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : PointedMap Γ Γ') (l : List Γ) : map f (mk₁ l) = mk₁ (List.map f.f l)