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₁.

Equations

• Turing.BlankExtends l₁ l₂ = ∃ (n : ℕ), l₂ = l₁ ++ List.replicate n default

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

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

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

def Turing.BlankExtends.above {Γ : Type u_1} [Inhabited Γ] {l l₁ l₂ : List Γ} (h₁ : Turing.BlankExtends l l₁) (h₂ : Turing.BlankExtends l l₂) : { l' : List Γ // Turing.BlankExtends l₁ l' ∧ Turing.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₂).

Equations

• h₁.above h₂ = if h : l₁.length ≤ l₂.length then ⟨l₂, ⋯⟩ else ⟨l₁, ⋯⟩

theorem Turing.BlankExtends.above_of_le {Γ : Type u_1} [Inhabited Γ] {l l₁ l₂ : List Γ} : Turing.BlankExtends l₁ l → Turing.BlankExtends l₂ l → l₁.length ≤ l₂.length → Turing.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.

Equations

• Turing.BlankRel l₁ l₂ = (Turing.BlankExtends l₁ l₂ ∨ Turing.BlankExtends l₂ l₁)

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

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

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

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

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

Equations

• h.above = if hl : l₁.length ≤ l₂.length then ⟨l₂, ⋯⟩ else ⟨l₁, ⋯⟩

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

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

Equations

• h.below = if hl : l₁.length ≤ l₂.length then ⟨l₁, ⋯⟩ else ⟨l₂, ⋯⟩

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

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

Construct a setoid instance for BlankRel.

Equations

• Turing.BlankRel.setoid Γ = { r := Turing.BlankRel, iseqv := ⋯ }

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.

Equations

• Turing.ListBlank Γ = Quotient (Turing.BlankRel.setoid Γ)

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

Equations

• Turing.ListBlank.inhabited = { default := Quotient.mk'' [] }

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

Equations

• Turing.ListBlank.hasEmptyc = { emptyCollection := Quotient.mk'' [] }

@[reducible, inline]

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

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

Equations

• l.liftOn f H = Quotient.liftOn' l f ⋯

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

The quotient map turning a List into a ListBlank.

Equations

• Turing.ListBlank.mk = Quotient.mk''

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

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

The head of a ListBlank is well defined.

Equations

• l.head = l.liftOn List.headI ⋯

@[simp]

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

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

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

Equations

• l.tail = l.liftOn (fun (l : List Γ) => Turing.ListBlank.mk l.tail) ⋯

@[simp]

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

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

We can cons an element onto a ListBlank.

Equations

• Turing.ListBlank.cons a l = l.liftOn (fun (l : List Γ) => Turing.ListBlank.mk (a :: l)) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Turing.ListBlank.cons_head_tail {Γ : Type u_1} [Inhabited Γ] (l : Turing.ListBlank Γ) : Turing.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 : Turing.ListBlank Γ) : ∃ (a : Γ) (l' : Turing.ListBlank Γ), l = Turing.ListBlank.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 : Turing.ListBlank Γ) (n : ℕ) : Γ

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

Equations

• l.nth n = l.liftOn (fun (l : List Γ) => l.getI n) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

Equations

• Turing.ListBlank.modifyNth f 0 x✝ = Turing.ListBlank.cons (f x✝.head) x✝.tail
• Turing.ListBlank.modifyNth f n.succ x✝ = Turing.ListBlank.cons x✝.head (Turing.ListBlank.modifyNth f n x✝.tail)

theorem Turing.ListBlank.nth_modifyNth {Γ : Type u_1} [Inhabited Γ] (f : Γ → Γ) (n i : ℕ) (L : Turing.ListBlank Γ) : (Turing.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

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

Equations

• Turing.instInhabitedPointedMap = { default := { f := default, map_pt' := ⋯ } }

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

Equations

• Turing.instCoeFunPointedMapForall = { coe := Turing.PointedMap.f }

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 : Turing.PointedMap Γ Γ') : f.f default = default

@[simp]

theorem Turing.PointedMap.headI_map {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : Turing.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 : Turing.PointedMap Γ Γ') (l : Turing.ListBlank Γ) : Turing.ListBlank Γ'

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

Equations

• Turing.ListBlank.map f l = l.liftOn (fun (l : List Γ) => Turing.ListBlank.mk (List.map f.f l)) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The i-th projection as a pointed map.

Equations

• Turing.proj i = { f := fun (a : (i : ι) → Γ i) => a i, map_pt' := ⋯ }

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

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

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

Append a list on the left side of a ListBlank.

Equations

• Turing.ListBlank.append [] x✝ = x✝
• Turing.ListBlank.append (a :: l) x✝ = Turing.ListBlank.cons a (Turing.ListBlank.append l x✝)

@[simp]

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

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

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

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

Equations

• l.flatMap f hf = l.liftOn (fun (l : List Γ) => Turing.ListBlank.mk (l.flatMap f)) ⋯

@[deprecated Turing.ListBlank.flatMap (since := "2024-10-16")]

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

Alias of Turing.ListBlank.flatMap.

---

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

Equations

• @Turing.ListBlank.bind = @Turing.ListBlank.flatMap

@[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) : (Turing.ListBlank.mk l).flatMap f hf = Turing.ListBlank.mk (l.flatMap f)

@[deprecated Turing.ListBlank.flatMap_mk (since := "2024-10-16")]

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

Alias of Turing.ListBlank.flatMap_mk.

@[simp]

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

@[deprecated Turing.ListBlank.cons_flatMap (since := "2024-10-16")]

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

Alias of Turing.ListBlank.cons_flatMap.

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 : Turing.ListBlank Γ

  The portion of the tape going off to the left.

• right : Turing.ListBlank Γ

  The portion of the tape going off to the right.

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

Equations

• Turing.Tape.inhabited = { default := { head := default, left := default, right := default } }

inductive Turing.Dir : Type

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

• left : Turing.Dir
• right : Turing.Dir

instance Turing.instDecidableEqDir : DecidableEq Turing.Dir

Equations

• Turing.instDecidableEqDir x✝ y✝ = if h : x✝.toCtorIdx = y✝.toCtorIdx then isTrue ⋯ else isFalse ⋯

instance Turing.instInhabitedDir : Inhabited Turing.Dir

Equations

• Turing.instInhabitedDir = { default := Turing.Dir.left }

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

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

Equations

• T.left₀ = Turing.ListBlank.cons T.head T.left

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

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

Equations

• T.right₀ = Turing.ListBlank.cons T.head T.right

def Turing.Tape.move {Γ : Type u_1} [Inhabited Γ] : Turing.Dir → Turing.Tape Γ → Turing.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.

Equations

• Turing.Tape.move Turing.Dir.left { head := a, left := L, right := R } = { head := L.head, left := L.tail, right := Turing.ListBlank.cons a R }
• Turing.Tape.move Turing.Dir.right { head := a, left := L, right := R } = { head := R.head, left := Turing.ListBlank.cons a L, right := R.tail }

@[simp]

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

@[simp]

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

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

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

Equations

• Turing.Tape.mk' L R = { head := R.head, left := L, right := R.tail }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

Equations

• Turing.Tape.mk₂ L R = Turing.Tape.mk' (Turing.ListBlank.mk L) (Turing.ListBlank.mk R)

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

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

Equations

• Turing.Tape.mk₁ l = Turing.Tape.mk₂ [] l

def Turing.Tape.nth {Γ : Type u_1} [Inhabited Γ] (T : Turing.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.)

Equations

• T.nth 0 = T.head
• T.nth (Int.ofNat n.succ) = T.right.nth n
• T.nth (Int.negSucc n) = T.left.nth n

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Replace the current value of the head on the tape.

Equations

• Turing.Tape.write b T = { head := b, left := T.left, right := T.right }

@[simp]

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

@[simp]

theorem Turing.Tape.write_nth {Γ : Type u_1} [Inhabited Γ] (b : Γ) (T : Turing.Tape Γ) {i : ℤ} : (Turing.Tape.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 : Turing.ListBlank Γ) : Turing.Tape.write b (Turing.Tape.mk' L (Turing.ListBlank.cons a R)) = Turing.Tape.mk' L (Turing.ListBlank.cons b R)

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

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

Equations

• Turing.Tape.map f T = { head := f.f T.head, left := Turing.ListBlank.map f T.left, right := Turing.ListBlank.map f T.right }

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem Turing.Tape.map_mk₂ {Γ : Type u_1} {Γ' : Type u_2} [Inhabited Γ] [Inhabited Γ'] (f : Turing.PointedMap Γ Γ') (L R : List Γ) : Turing.Tape.map f (Turing.Tape.mk₂ L R) = Turing.Tape.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 : Turing.PointedMap Γ Γ') (l : List Γ) : Turing.Tape.map f (Turing.Tape.mk₁ l) = Turing.Tape.mk₁ (List.map f.f l)