Equivalent tape representations

DefinitionHalf-tape view of a stack tape#✓fully proved

A stack tape \(s\) over an alphabet \(\Gamma\) is a finite list of cells, each a symbol of \(\Gamma\) or the blank cell, that does not end in a blank cell. Its half-tape view is the half-tape of cells (a sequence of cells taken up to trailing blanks, the blank cell being the default) whose cells are those of \(s\) in order, followed by blank cells.

def toListBlank (s : StackTape Γ) : ListBlank (Option Γ) :=
  ListBlank.mk s.toList
Used by 18
Used byFirst symbol of a half-tape read from non-blank cells · First cell of the half-tape view of a stack tape · Left half of the view of a two-way tape · Cells of the half-tape view of a stack tape · The cells of the view · Right half of the tape view · Dropping the first cell of a stack tape of non-blank symbols · Tail of the half-tape view of a stack tape · Half-tape of a stack tape of non-blank symbols · Pushing a cell onto a stack tape of non-blank symbols · Pushing a cell onto a stack tape · Distinct stack tapes of non-blank symbols read as distinct half-tapes · The half-tape view of stack tapes is injective · Half-tape view of a word · Half-tape view of the empty stack tape · Cell view of a two-way tape · The tape view is injective · The cell view commutes with head moves

TheoremHalf-tape view of the empty stack tape#✓fully proved

The half-tape view of the empty stack tape over \(\Gamma\) is the half-tape all of whose cells are blank.

@[simp]
theorem toListBlank_nil : (nil : StackTape Γ).toListBlank = ListBlank.mk []
Uses 1
Statement usesHalf-tape view of a stack tape

TheoremPushing a cell onto a stack tape#✓fully proved

For every cell \(c\) (a symbol of \(\Gamma\) or the blank cell) and every stack tape \(s\) over \(\Gamma\), the half-tape view of the stack tape obtained by pushing \(c\) onto \(s\) is the half-tape view of \(s\) with \(c\) pushed onto its front.

For the blank cell this holds because the half-tape is blank beyond its end.

@[simp]
theorem toListBlank_cons (o : Option Γ) (s : StackTape Γ) :
    (cons o s).toListBlank = s.toListBlank.cons o
Uses 1 · Used by 2
Statement usesHalf-tape view of a stack tape
Used byPushing a cell onto a stack tape of non-blank symbols · The cell view commutes with head moves

TheoremFirst cell of the half-tape view of a stack tape#✓fully proved

For every stack tape \(s\) over \(\Gamma\) (a finite list of cells, each a symbol of \(\Gamma\) or the blank, that does not end in a blank), the first cell of the half-tape view of \(s\) (its cells followed by infinitely many blanks) is the first cell of \(s\), which is the blank if \(s\) is empty.

@[simp]
theorem head_toListBlank (s : StackTape Γ) : s.toListBlank.head = s.head
Uses 1 · Used by 2
Statement usesHalf-tape view of a stack tape
Used byFirst symbol of a half-tape read from non-blank cells · The cell view commutes with head moves

TheoremTail of the half-tape view of a stack tape#✓fully proved

For every stack tape \(s\) over \(\Gamma\) (a list of cells, each a symbol of \(\Gamma\) or the blank cell, not ending in a blank cell), the tail of the half-tape view of \(s\) is the half-tape view of the tail of \(s\): dropping the first cell of \(s\) drops the first cell of its half-tape.

@[simp]
theorem tail_toListBlank (s : StackTape Γ) : s.toListBlank.tail = s.tail.toListBlank
Uses 1 · Used by 2
Statement usesHalf-tape view of a stack tape
Used byDropping the first cell of a stack tape of non-blank symbols · The cell view commutes with head moves

TheoremCells of the half-tape view of a stack tape#✓fully proved

For every stack tape \(s\) over \(\Gamma\) (a finite list of cells, each a symbol of \(\Gamma\) or the blank, that does not end in a blank) and every \(n \in \mathbb{N}\), the cell at position \(n\) of the half-tape view of \(s\) (its cells followed by infinitely many blanks) is the \(n\)-th cell of \(s\), counting from \(0\), if \(n\) is less than the length of \(s\), and the blank otherwise.

theorem nth_toListBlank (s : StackTape Γ) (n : ℕ) :
    s.toListBlank.nth n = (s.toList[n]?).getD none
Uses 1 · Used by 1
Statement usesHalf-tape view of a stack tape
Used byThe cells of the view

TheoremHalf-tape view of a word#✓fully proved

For every word \(a_1 \cdots a_n\) over \(\Gamma\), the half-tape view of the stack tape whose cells are the non-blank cells \(a_1, \dots, a_n\) is the half-tape whose first \(n\) cells are \(a_1, \dots, a_n\) and whose later cells are blank.

@[simp]
theorem toListBlank_mapSome (l : List Γ) :
    (mapSome l).toListBlank = ListBlank.mk (l.map some)
Uses 1
Statement usesHalf-tape view of a stack tape

TheoremThe half-tape view of stack tapes is injective#✓fully proved

If two stack tapes over \(\Gamma\) have the same half-tape view, then they are equal.

This holds because a stack tape does not end in a blank cell, so trailing blanks of a half-tape do not come from cells.

theorem toListBlank_injective : Function.Injective (toListBlank (Γ := Γ))
Uses 1 · Used by 2
Statement usesHalf-tape view of a stack tape
Used byDistinct stack tapes of non-blank symbols read as distinct half-tapes · The tape view is injective

DefinitionCell view of a two-way tape#✓fully proved

A CSLib tape \(t\) over an alphabet \(\Gamma\) has a head cell and two halves, each a finite list of cells not ending in a blank, where a cell is a symbol of \(\Gamma\) or the blank. Its cell view is the Mathlib tape over cells, with the blank as default symbol, whose head is the head cell of \(t\) and whose left and right halves are the halves of \(t\), blank past their ends. So the cell at position \(i \in \mathbb{Z}\) of the view is the cell \(i\) places to the right of the head of \(t\) (to the left when \(i < 0\)).

def toTape (t : BiTape Γ) : Tape (Option Γ) :=
  ⟨t.head, t.left.toListBlank, t.right.toListBlank⟩
Uses 1 · Used by 20
Statement usesHalf-tape view of a stack tape
Used byHead cell of the view of a two-way tape · Left half of the view of a two-way tape · The cells of the view · Cells of an input tape · Cells after \(n\) moves to the right · Cells after an optional move · Cells after a write · Cells after a write and an optional move · Right half of the tape view · Post–Turing reading of a tape over the non-blank symbols · Distinct tapes of non-blank symbols read as distinct TM0 tapes · The tape view is injective · The Post–Turing reading of an input tape · The cell view of an input tape · Head moves commute with the Post–Turing reading of a tape · The cell view commutes with head moves · The cell view commutes with optional head moves · Writing commutes with the Post–Turing reading of a tape · The cell view commutes with writing · The fenced machine halts on some padding of a word iff the machine halts on it

TheoremHead cell of the view of a two-way tape#✓fully proved

For every two-way tape \(t\) over \(\Gamma\) (a head cell with a left and a right stack tape), the head cell of the view of \(t\) as a tape of cells is the head cell of \(t\).

@[simp]
theorem head_toTape (t : BiTape Γ) : t.toTape.head = t.head
Uses 1
Statement usesCell view of a two-way tape

TheoremLeft half of the view of a two-way tape#✓fully proved

For every two-way tape \(t\) over \(\Gamma\) (a head cell with a left and a right stack tape), the left half of the view of \(t\) as a tape of cells is the half-tape view of the left stack tape of \(t\).

@[simp]
theorem left_toTape (t : BiTape Γ) : t.toTape.left = t.left.toListBlank
Uses 2
Statement usesCell view of a two-way tape · Half-tape view of a stack tape

TheoremRight half of the tape view#✓fully proved

For every two-sided tape \(t\) over \(\Gamma\) (a head cell together with a left and a right stack tape), the right half of the tape view of \(t\) is the half-tape view of the right half of \(t\).

@[simp]
theorem right_toTape (t : BiTape Γ) : t.toTape.right = t.right.toListBlank
Uses 2
Statement usesCell view of a two-way tape · Half-tape view of a stack tape

TheoremThe cells of the view#✓fully proved

Let \(t\) be a two-way tape over \(\Gamma\) with head cell \(h\), left stack tape \((\ell_0, \dots, \ell_{p-1})\) and right stack tape \((r_0, \dots, r_{q-1})\). For every integer \(i\), the cell at position \(i\) of the view of \(t\) as a tape of cells is \(h\) if \(i = 0\), \(r_{i-1}\) if \(0 < i \le q\), \(\ell_{-i-1}\) if \(-p \le i < 0\), and the blank otherwise.

theorem nth_toTape (t : BiTape Γ) (i : ℤ) :
    t.toTape.nth i =
      if i = 0 then t.head
      else if 0 < i then (t.right.toList[(i - 1).toNat]?).getD none
      else (t.left.toList[(-i - 1).toNat]?).getD none
Uses 3
Statement usesCell view of a two-way tape
Proof usesCells of the half-tape view of a stack tape · Half-tape view of a stack tape

TheoremThe cell view commutes with writing#✓fully proved

For every tape \(t\) and every cell \(a\) (a symbol or the blank), the cell view of the tape obtained from \(t\) by writing \(a\) under the head equals the tape obtained from the cell view of \(t\) by writing \(a\) under its head.

@[simp]
theorem toTape_write (t : BiTape Γ) (a : Option Γ) : (t.write a).toTape = t.toTape.write a
Uses 1 · Used by 2
Statement usesCell view of a two-way tape
Used byCells after a write · Writing commutes with the Post–Turing reading of a tape

TheoremThe cell view commutes with head moves#✓fully proved

For every tape \(t\) and each direction \(d\) (left or right), the cell view of the tape obtained from \(t\) by moving the head one cell in direction \(d\) equals the tape obtained from the cell view of \(t\) by moving its head one cell in direction \(d\).

@[simp]
theorem toTape_move (t : BiTape Γ) (d : Dir) : (t.move d).toTape = t.toTape.move d
Uses 5 · Used by 3
Statement usesCell view of a two-way tape
Proof usesFirst cell of the half-tape view of a stack tape · Tail of the half-tape view of a stack tape · Half-tape view of a stack tape · Pushing a cell onto a stack tape
Used byCells after \(n\) moves to the right · Head moves commute with the Post–Turing reading of a tape · The cell view commutes with optional head moves

TheoremThe cell view commutes with optional head moves#✓fully proved

For every two-way tape \(t\) over \(\Gamma\) and every optional head move \(d\), which is either no move or a move one cell in a direction, the cell view of the tape obtained from \(t\) by the optional move \(d\) is the cell view of \(t\) when \(d\) is no move, and the cell view of \(t\) with its head moved one cell in direction \(d\) when \(d\) is a direction.

theorem toTape_optionMove (t : BiTape Γ) (d : Option Dir) :
    (t.optionMove d).toTape = d.elim t.toTape fun d ↦ t.toTape.move d
Uses 2 · Used by 1
Statement usesCell view of a two-way tape
Proof usesThe cell view commutes with head moves
Used byCells after an optional move

DefinitionOffset of an optional head move#✓fully proved

The offset of an optional head move \(d\) is \(0\) if \(d\) is no move, \(-1\) if \(d\) is a move to the left and \(1\) if \(d\) is a move to the right.

After the move \(d\), the cell at position \(i\) relative to the head is the cell that was at position \(i\) plus the offset of \(d\).

def optionMoveOffset : Option Dir → ℤ
  | none => 0
  | some .left => -1
  | some .right => 1
Used by 4
Used byCells after an optional move · Cells after a write and an optional move · The offset of an optional move is at most one · The fenced machine halts on some padding of a word iff the machine halts on it

TheoremThe offset of an optional move is at most one#✓fully proved

For every optional head move \(d\) (no move, a move to the left, or a move to the right), the offset of \(d\) lies between \(-1\) and \(1\), that is, \(-1 \le \mathrm{offset}(d) \le 1\).

theorem optionMoveOffset_bound (d : Option Dir) :
    -1 ≤ optionMoveOffset d ∧ optionMoveOffset d ≤ 1
Uses 1 · Used by 1
Statement usesOffset of an optional head move
Used byThe fenced machine halts on some padding of a word iff the machine halts on it

TheoremCells after a write#✓fully proved

For every two-way tape \(t\) over \(\Gamma\), every cell \(a\) (a symbol of \(\Gamma\) or the blank) and every integer \(i\), the cell at position \(i\) of the view of the tape obtained from \(t\) by writing \(a\) under the head is \(a\) if \(i = 0\), and the cell at position \(i\) of the view of \(t\) otherwise.

theorem nth_toTape_write (t : BiTape Γ) (a : Option Γ) (i : ℤ) :
    (t.write a).toTape.nth i = if i = 0 then a else t.toTape.nth i
Uses 2 · Used by 1
Statement usesCell view of a two-way tape
Proof usesThe cell view commutes with writing
Used byCells after a write and an optional move

TheoremCells after an optional move#✓fully proved

For an optional direction \(d\), let \(\delta(d)\) be \(0\) if \(d\) is no move, \(-1\) if \(d\) is a move to the left and \(1\) if \(d\) is a move to the right. For every two-way tape \(t\) over \(\Gamma\) and every integer \(i\), the cell at position \(i\) of the view of the tape obtained from \(t\) by the optional move \(d\) is the cell at position \(i + \delta(d)\) of the view of \(t\).

theorem nth_toTape_optionMove (t : BiTape Γ) (d : Option Dir) (i : ℤ) :
    (t.optionMove d).toTape.nth i = t.toTape.nth (i + optionMoveOffset d)
Uses 3 · Used by 1
Statement usesOffset of an optional head move · Cell view of a two-way tape
Proof usesThe cell view commutes with optional head moves
Used byCells after a write and an optional move

TheoremCells after a write and an optional move#✓fully proved

For an optional direction \(d\), let \(\delta(d)\) be \(0\) if \(d\) is no move, \(-1\) if \(d\) is a move to the left and \(1\) if \(d\) is a move to the right. For every two-way tape \(t\) over \(\Gamma\), every cell \(a\) (a symbol of \(\Gamma\) or the blank) and every integer \(i\), the cell at position \(i\) of the view of the tape obtained from \(t\) by writing \(a\) under the head and then performing the optional move \(d\) is \(a\) if \(i + \delta(d) = 0\), and the cell at position \(i + \delta(d)\) of the view of \(t\) otherwise.

theorem nth_toTape_write_optionMove (t : BiTape Γ) (a : Option Γ) (d : Option Dir) (i : ℤ) :
    ((t.write a).optionMove d).toTape.nth i =
      if i + optionMoveOffset d = 0 then a else t.toTape.nth (i + optionMoveOffset d)
Uses 4 · Used by 1
Statement usesOffset of an optional head move · Cell view of a two-way tape
Proof usesCells after an optional move · Cells after a write
Used byThe fenced machine halts on some padding of a word iff the machine halts on it

TheoremCells after \(n\) moves to the right#✓fully proved

For every two-way tape \(t\) over \(\Gamma\), every \(n \in \mathbb{N}\) and every integer \(i\), the cell at position \(i\) of the view of the tape obtained from \(t\) by moving the head \(n\) times to the right is the cell at position \(i + n\) of the view of \(t\).

theorem nth_toTape_moveRight_iterate (t : BiTape Γ) (n : ℕ) (i : ℤ) :
    (moveRight^[n] t).toTape.nth i = t.toTape.nth (i + n)
Uses 2 · Used by 1
Statement usesCell view of a two-way tape
Proof usesThe cell view commutes with head moves
Used byThe fenced machine halts on some padding of a word iff the machine halts on it

TheoremThe cell view of an input tape#✓fully proved

For every word \(w = w_0 w_1 \cdots w_{n-1}\) over \(\Gamma\), the cell view of the input tape of \(w\) is the Mathlib input tape of the list of non-blank cells \(w_0, \dots, w_{n-1}\): the head is on \(w_0\), the letters \(w_1, \dots, w_{n-1}\) lie to its right in order, and every other cell is blank (for the empty word, every cell is blank).

@[simp]
theorem toTape_mk₁ (l : List Γ) : (mk₁ l).toTape = Tape.mk₁ (l.map some)
Uses 1 · Used by 1
Statement usesCell view of a two-way tape
Used byThe Post–Turing reading of an input tape

TheoremCells of an input tape#✓fully proved

For every word \(w = w_0 \cdots w_{m-1}\) over \(\Gamma\) and every integer \(i\), the cell at position \(i\) of the view of the input tape of \(w\) is \(w_i\) if \(0 \le i < m\), and the blank otherwise.

theorem nth_toTape_mk₁ (l : List Γ) (i : ℤ) :
    (mk₁ l).toTape.nth i = if 0 ≤ i then l[i.toNat]? else none
Uses 1 · Used by 1
Statement usesCell view of a two-way tape
Used byThe fenced machine halts on some padding of a word iff the machine halts on it

TheoremThe tape view is injective#✓fully proved

If two two-sided tapes \(t\) and \(t'\) over \(\Gamma\) (each a head cell together with a left and a right stack tape) have the same tape view as a tape of cells, then \(t = t'\).

theorem toTape_injective : Function.Injective (toTape (Γ := Γ))
Uses 3 · Used by 1
Statement usesCell view of a two-way tape
Proof usesHalf-tape view of a stack tape · The half-tape view of stack tapes is injective
Used byDistinct tapes of non-blank symbols read as distinct TM0 tapes

AbbreviationNon-blank symbols#✓fully proved

For an alphabet \(\Gamma_0\) with a distinguished blank symbol \(b\), the non-blank symbols of \(\Gamma_0\) are the elements \(x \in \Gamma_0\) with \(x \ne b\). They form the tape alphabet of the single-tape machine that simulates a Post–Turing machine over \(\Gamma_0\).

abbrev NonBlank (Γ₀ : Type) [Inhabited Γ₀] : Type := {x : Γ₀ // x ≠ default}
Used by 40
Used byThe answer machine runs in one step · The decider within time · Problems in P are decided in polynomial time by single-tape machines · The answer machine · The answer machine outputs the answer of a one-cell input · The bottom cell of the start tape · The answer bit of a cell · The decider of a multi-stack machine · The decider outputs the answer bit · Finite single-tape emulation of a multi-stack machine · The recognizer halts iff the multi-stack machine does · Input cell of a bit · The bottom cell followed by the input word is the emulation's start tape · Computable predicates are decidable by single-tape machines · R.e. predicates are recognizable by single-tape machines · The recognizer of a multi-stack machine · Cell symbol · Value of the cell-symbol map · The cell-symbol map is injective · The simulating machine halts exactly when the Post–Turing machine halts · First symbol of a half-tape read from non-blank cells · Head symbol of a tape read from non-blank cells · Single-tape simulation of a Post–Turing machine · The single-tape simulation has the same output · The single-tape simulation outputs within one extra step · Runs of a TM0 machine are runs of its single-tape simulation · The simulation halts one step after the TM0 machine · Each TM0 step is one step of the simulation · Dropping the first cell of a stack tape of non-blank symbols · Half-tape of a stack tape of non-blank symbols · Pushing a cell onto a stack tape of non-blank symbols · Distinct stack tapes of non-blank symbols read as distinct half-tapes · A word of non-blank symbols reads as itself · The empty stack tape reads as the blank half-tape · Post–Turing reading of a tape over the non-blank symbols · Distinct tapes of non-blank symbols read as distinct TM0 tapes · The Post–Turing reading of an input tape · Head moves commute with the Post–Turing reading of a tape · Optional head moves commute with the Post–Turing reading of a tape · Writing commutes with the Post–Turing reading of a tape

DefinitionCell symbol#✓fully proved

Let \(\Gamma_0\) be an alphabet with blank symbol \(b\). A tape cell over the non-blank symbols of \(\Gamma_0\) is either blank or holds a symbol \(x \ne b\) of \(\Gamma_0\). Its cell symbol is \(b\) for the blank cell and \(x\) for the cell holding \(x\). This map from cells to \(\Gamma_0\) sends the blank cell to the blank symbol, so it is a pointed map.

def cellSymbol : PointedMap (Option (NonBlank Γ₀)) Γ₀ :=
  ⟨Equiv.optionSubtypeNe default, rfl⟩
Uses 1 · Used by 13
Statement usesNon-blank symbols
Used byValue of the cell-symbol map · The cell-symbol map is injective · First symbol of a half-tape read from non-blank cells · Dropping the first cell of a stack tape of non-blank symbols · Half-tape of a stack tape of non-blank symbols · Pushing a cell onto a stack tape of non-blank symbols · Distinct stack tapes of non-blank symbols read as distinct half-tapes · A word of non-blank symbols reads as itself · Post–Turing reading of a tape over the non-blank symbols · Distinct tapes of non-blank symbols read as distinct TM0 tapes · The Post–Turing reading of an input tape · Head moves commute with the Post–Turing reading of a tape · Writing commutes with the Post–Turing reading of a tape

TheoremValue of the cell-symbol map#✓fully proved

For every cell \(o\) over the non-blank symbols of an alphabet \(\Gamma_0\) with blank symbol \(b\), the cell symbol of \(o\) is \(b\) when \(o\) is the blank cell and is \(x\) when \(o\) holds the non-blank symbol \(x\).

@[simp]
theorem cellSymbol_apply (o : Option (NonBlank Γ₀)) :
    cellSymbol o = Equiv.optionSubtypeNe default o
Uses 2 · Used by 1
Statement usesNon-blank symbols · Cell symbol
Used byWriting commutes with the Post–Turing reading of a tape

TheoremThe cell-symbol map is injective#✓fully proved

Distinct cells over the non-blank symbols of an alphabet \(\Gamma_0\) have distinct cell symbols in \(\Gamma_0\).

theorem cellSymbol_injective : Function.Injective (cellSymbol (Γ₀ := Γ₀))
Uses 2 · Used by 2
Statement usesNon-blank symbols · Cell symbol
Used byDistinct stack tapes of non-blank symbols read as distinct half-tapes · Distinct tapes of non-blank symbols read as distinct TM0 tapes

DefinitionHalf-tape of a stack tape of non-blank symbols#✓fully proved

Let \(\Gamma_0\) be an alphabet with blank symbol \(b\) and \(N = \Gamma_0 \setminus \{b\}\) its non-blank symbols. A stack tape \(s\) over \(N\), a finite list of cells each blank or holding a symbol of \(N\) and not ending in a blank cell, is read as the TM0 half-tape over \(\Gamma_0\) whose \(i\)-th symbol is that of the \(i\)-th cell of \(s\): \(b\) for a blank cell, \(x\) for a cell holding \(x\), and \(b\) past the end of \(s\).

def toListBlank (s : StackTape (NonBlank Γ₀)) : ListBlank Γ₀ :=
  s.toListBlank.map cellSymbol
Uses 3 · Used by 6
Statement usesNon-blank symbols · Cell symbol · Half-tape view of a stack tape
Used byFirst symbol of a half-tape read from non-blank cells · Dropping the first cell of a stack tape of non-blank symbols · Pushing a cell onto a stack tape of non-blank symbols · Distinct stack tapes of non-blank symbols read as distinct half-tapes · A word of non-blank symbols reads as itself · The empty stack tape reads as the blank half-tape

DefinitionPost–Turing reading of a tape over the non-blank symbols#✓fully proved

Let \(\Gamma_0\) be an alphabet whose default symbol is the blank. The Post–Turing reading of a two-way tape \(t\) whose cells are blank or hold non-blank symbols of \(\Gamma_0\) is the Post–Turing machine tape over \(\Gamma_0\) obtained cell by cell: take the view of \(t\) as a tape of cells, each cell at its position relative to the head and blank cells past the ends, and replace each cell by its symbol, a non-blank symbol \(x\) by \(x\) itself and the blank cell by the blank of \(\Gamma_0\).

def toTape (t : BiTape (NonBlank Γ₀)) : Tape Γ₀ :=
  t.toTape.map cellSymbol
Uses 3 · Used by 11
Statement usesCell view of a two-way tape · Non-blank symbols · Cell symbol
Used byThe simulating machine halts exactly when the Post–Turing machine halts · Head symbol of a tape read from non-blank cells · The single-tape simulation outputs within one extra step · Runs of a TM0 machine are runs of its single-tape simulation · The simulation halts one step after the TM0 machine · Each TM0 step is one step of the simulation · Distinct tapes of non-blank symbols read as distinct TM0 tapes · The Post–Turing reading of an input tape · Head moves commute with the Post–Turing reading of a tape · Optional head moves commute with the Post–Turing reading of a tape · Writing commutes with the Post–Turing reading of a tape

TheoremThe empty stack tape reads as the blank half-tape#✓fully proved

For an alphabet \(\Gamma_0\) with blank symbol \(b\), the empty stack tape over the non-blank symbols of \(\Gamma_0\) reads as the half-tape of the empty list, all of whose symbols are \(b\).

@[simp]
theorem toListBlank_nil : toListBlank (StackTape.nil : StackTape (NonBlank Γ₀)) = ListBlank.mk []
Uses 2
Statement usesNon-blank symbols · Half-tape of a stack tape of non-blank symbols

TheoremPushing a cell onto a stack tape of non-blank symbols#✓fully proved

Let \(\Gamma_0\) be an alphabet with blank symbol \(b\) and \(N = \Gamma_0 \setminus \{b\}\). Read a cell over \(N\) as a symbol of \(\Gamma_0\): \(b\) for the blank cell, \(x\) for a cell holding \(x\). For every cell \(o\) and every stack tape \(s\) over \(N\), the half-tape read from the stack tape obtained by pushing \(o\) onto \(s\) is the half-tape read from \(s\) with the symbol of \(o\) pushed onto its front.

For the blank cell this holds because the half-tape is blank beyond its end.

@[simp]
theorem toListBlank_cons (o : Option (NonBlank Γ₀)) (s : StackTape (NonBlank Γ₀)) :
    toListBlank (StackTape.cons o s) =
      (toListBlank s).cons (Equiv.optionSubtypeNe default o)
Uses 5
Statement usesNon-blank symbols · Half-tape of a stack tape of non-blank symbols
Proof usesCell symbol · Half-tape view of a stack tape · Pushing a cell onto a stack tape

TheoremFirst symbol of a half-tape read from non-blank cells#✓fully proved

Let \(\Gamma_0\) be an alphabet with blank symbol \(b\). For every stack tape \(s\) of cells over the non-blank symbols of \(\Gamma_0\) (a finite list of cells, blank beyond its end), the first symbol of the half-tape over \(\Gamma_0\) read from \(s\) is the cell symbol of the first cell of \(s\); when \(s\) is empty this is \(b\).

@[simp]
theorem head_toListBlank (s : StackTape (NonBlank Γ₀)) :
    (toListBlank s).head = Equiv.optionSubtypeNe default s.head
Uses 5
Statement usesNon-blank symbols · Half-tape of a stack tape of non-blank symbols
Proof usesCell symbol · First cell of the half-tape view of a stack tape · Half-tape view of a stack tape

TheoremDropping the first cell of a stack tape of non-blank symbols#✓fully proved

For an alphabet \(\Gamma_0\) with blank symbol \(b\) and every stack tape \(s\) over the non-blank symbols of \(\Gamma_0\), dropping the first symbol of the half-tape read from \(s\) gives the half-tape read from \(s\) with its first cell removed (the empty stack tape staying empty).

@[simp]
theorem tail_toListBlank (s : StackTape (NonBlank Γ₀)) :
    (toListBlank s).tail = toListBlank s.tail
Uses 5
Statement usesNon-blank symbols · Half-tape of a stack tape of non-blank symbols
Proof usesCell symbol · Tail of the half-tape view of a stack tape · Half-tape view of a stack tape

TheoremA word of non-blank symbols reads as itself#✓fully proved

For an alphabet \(\Gamma_0\) with blank symbol \(b\) and a word \(w\) of non-blank symbols of \(\Gamma_0\), the half-tape read from the stack tape whose cells hold the letters of \(w\) in order is the half-tape of \(w\), viewed as a word over \(\Gamma_0\).

@[simp]
theorem toListBlank_mapSome (l : List (NonBlank Γ₀)) :
    toListBlank (StackTape.mapSome l) = ListBlank.mk (l.map Subtype.val)
Uses 3
Statement usesNon-blank symbols · Half-tape of a stack tape of non-blank symbols
Proof usesCell symbol

TheoremDistinct stack tapes of non-blank symbols read as distinct half-tapes#✓fully proved

For an alphabet \(\Gamma_0\) with blank symbol \(b\), two stack tapes over the non-blank symbols of \(\Gamma_0\) that read as the same half-tape over \(\Gamma_0\) are equal.

A stack tape does not end in a blank, so the trailing blanks of a half-tape do not come from cells.

theorem toListBlank_injective : Function.Injective (toListBlank (Γ₀ := Γ₀))
Uses 6
Statement usesNon-blank symbols · Half-tape of a stack tape of non-blank symbols
Proof usesCell symbol · The cell-symbol map is injective · Half-tape view of a stack tape · The half-tape view of stack tapes is injective

TheoremHead symbol of a tape read from non-blank cells#✓fully proved

For every two-way tape \(t\) of cells over the non-blank symbols of an alphabet \(\Gamma_0\), the symbol under the head of the tape over \(\Gamma_0\) read from \(t\) is the cell symbol of the cell under the head of \(t\).

@[simp]
theorem head_toTape (t : BiTape (NonBlank Γ₀)) :
    (toTape t).head = Equiv.optionSubtypeNe default t.head
Uses 2 · Used by 1
Statement usesNon-blank symbols · Post–Turing reading of a tape over the non-blank symbols
Used byEach TM0 step is one step of the simulation

TheoremWriting commutes with the Post–Turing reading of a tape#✓fully proved

Let \(\Gamma_0\) be an alphabet whose default symbol is the blank, and for a two-way tape \(t\) whose cells are blank or hold non-blank symbols of \(\Gamma_0\), let \(\tau(t)\) be the Post–Turing reading of \(t\), a Post–Turing machine tape over \(\Gamma_0\). For every such \(t\) and every cell \(o\), blank or holding a non-blank symbol, \(\tau\) of \(t\) with \(o\) written under the head is \(\tau(t)\) with the symbol of \(o\) written under the head, where the symbol of \(o\) is \(x\) if \(o\) holds \(x\) and the blank of \(\Gamma_0\) if \(o\) is blank.

@[simp]
theorem toTape_write (t : BiTape (NonBlank Γ₀)) (o : Option (NonBlank Γ₀)) :
    toTape (t.write o) = (toTape t).write (Equiv.optionSubtypeNe default o)
Uses 6 · Used by 1
Statement usesNon-blank symbols · Post–Turing reading of a tape over the non-blank symbols
Proof usesCell view of a two-way tape · The cell view commutes with writing · Cell symbol · Value of the cell-symbol map
Used byEach TM0 step is one step of the simulation

TheoremHead moves commute with the Post–Turing reading of a tape#✓fully proved

Let \(\Gamma_0\) be an alphabet whose default symbol is the blank, and for a two-way tape \(t\) whose cells are blank or hold non-blank symbols of \(\Gamma_0\), let \(\tau(t)\) be the Post–Turing reading of \(t\), a Post–Turing machine tape over \(\Gamma_0\). For every such \(t\) and every direction \(d\), left or right, \(\tau\) of \(t\) with its head moved in direction \(d\) is \(\tau(t)\) with its head moved in direction \(d\).

@[simp]
theorem toTape_move (t : BiTape (NonBlank Γ₀)) (d : Dir) :
    toTape (t.move d) = (toTape t).move d
Uses 5 · Used by 2
Statement usesNon-blank symbols · Post–Turing reading of a tape over the non-blank symbols
Proof usesCell view of a two-way tape · The cell view commutes with head moves · Cell symbol
Used byEach TM0 step is one step of the simulation · Optional head moves commute with the Post–Turing reading of a tape

TheoremOptional head moves commute with the Post–Turing reading of a tape#✓fully proved

Let \(\Gamma_0\) be an alphabet whose default symbol is the blank, and for a two-way tape \(t\) whose cells are blank or hold non-blank symbols of \(\Gamma_0\), let \(\tau(t)\) be the Post–Turing reading of \(t\), a Post–Turing machine tape over \(\Gamma_0\). For every such \(t\) and every optional move \(d\), which is either no move or a direction, \(\tau\) of \(t\) after the optional move \(d\) is \(\tau(t)\) when \(d\) is no move, and \(\tau(t)\) with its head moved in direction \(d\) when \(d\) is a direction.

theorem toTape_optionMove (t : BiTape (NonBlank Γ₀)) (d : Option Dir) :
    toTape (t.optionMove d) = d.elim (toTape t) fun d ↦ (toTape t).move d
Uses 3
Statement usesNon-blank symbols · Post–Turing reading of a tape over the non-blank symbols
Proof usesHead moves commute with the Post–Turing reading of a tape

TheoremThe Post–Turing reading of an input tape#✓fully proved

Let \(\Gamma_0\) be an alphabet whose default symbol is the blank. For every word \(l\) of non-blank symbols of \(\Gamma_0\), the Post–Turing reading of the two-way input tape of \(l\) (the head on the first symbol of \(l\), the rest of \(l\) to its right, every other cell blank) is the Post–Turing machine input tape of \(l\) read as a word over \(\Gamma_0\), with the head on the first symbol of \(l\) and the rest of \(l\) to its right.

@[simp]
theorem toTape_mk₁ (l : List (NonBlank Γ₀)) :
    toTape (BiTape.mk₁ l) = Tape.mk₁ (l.map Subtype.val)
Uses 5 · Used by 2
Statement usesNon-blank symbols · Post–Turing reading of a tape over the non-blank symbols
Proof usesCell view of a two-way tape · The cell view of an input tape · Cell symbol
Used byThe simulating machine halts exactly when the Post–Turing machine halts · The single-tape simulation outputs within one extra step

TheoremDistinct tapes of non-blank symbols read as distinct TM0 tapes#✓fully proved

For an alphabet \(\Gamma_0\) with blank symbol \(b\), two tapes over the non-blank symbols of \(\Gamma_0\) that read, cell by cell, as the same TM0 tape over \(\Gamma_0\) are equal.

theorem toTape_injective : Function.Injective (toTape (Γ₀ := Γ₀))
Uses 6 · Used by 1
Statement usesNon-blank symbols · Post–Turing reading of a tape over the non-blank symbols
Proof usesCell view of a two-way tape · The tape view is injective · Cell symbol · The cell-symbol map is injective
Used byThe single-tape simulation outputs within one extra step

DefinitionSingle-tape simulation of a Post–Turing machine#✓fully proved

Let \(\Gamma_0\) be a finite alphabet with blank symbol \(b\) and at least one non-blank symbol, and let \(M\) be a Post–Turing machine over \(\Gamma_0\) with start state \(q_0\), supported by the finite set of states \(S\) (so \(q_0 \in S\), and from a state in \(S\) the machine \(M\) only enters states in \(S\)). The single-tape machine simulating \(M\) has the non-blank symbols of \(\Gamma_0\) as tape alphabet, \(S\) as set of states and \(q_0\) as start state. In a state \(q\), reading a cell \(s\) whose cell symbol is \(a\), it acts as follows. If \(M\) halts in \(q\) on \(a\), it writes \(s\) back and halts. If \(M\) moves the head in direction \(d\) and enters \(q'\), it writes \(s\) back, moves in direction \(d\) and enters \(q'\). If \(M\) writes \(a'\) and enters \(q'\), it writes the blank cell when \(a' = b\) and otherwise the cell holding \(a'\), does not move, and enters \(q'\).

CSLib machines need a chosen symbol of their alphabet, so an alphabet whose only symbol is the blank is excluded.

def ofTM0 : SingleTapeTM (NonBlank Γ₀) where
  State := {q // q ∈ S}
  q₀ := ⟨default, hS.1⟩
  tr q s :=
    match h : M q.1 (Equiv.optionSubtypeNe default s) with
    | none => (⟨s, none⟩, none)
    | some (q', .move d) => (⟨s, some d⟩, some ⟨q', hS.2 h q.2⟩)
    | some (q', .write a) =>
      (⟨(Equiv.optionSubtypeNe default).symm a, none⟩, some ⟨q', hS.2 h q.2⟩)
Uses 1 · Used by 8
Statement usesNon-blank symbols
Used byFinite single-tape emulation of a multi-stack machine · The recognizer halts iff the multi-stack machine does · The simulating machine halts exactly when the Post–Turing machine halts · The single-tape simulation has the same output · The single-tape simulation outputs within one extra step · Runs of a TM0 machine are runs of its single-tape simulation · The simulation halts one step after the TM0 machine · Each TM0 step is one step of the simulation

TheoremThe simulation halts one step after the TM0 machine#✓fully proved

Let \(M\) be a TM0 machine over a finite alphabet \(\Gamma_0\) with blank symbol \(b\) and at least one non-blank symbol, supported by a finite set \(S\) of states, and let \(\widehat{M}\) be the single-tape machine over the non-blank symbols \(N = \Gamma_0 \setminus \{b\}\) simulating \(M\). For a tape \(t\) over \(N\), write \(\tau(t)\) for the TM0 tape read from \(t\) cell by cell. If \(q \in S\) and \(M\) has no step from the configuration \((q, \tau(t))\), then one step of \(\widehat{M}\) from the configuration \((q, t)\) leads to its halting state with the tape \(t\) unchanged.

theorem step_ofTM0_of_step_eq_none {q : Λ} (hq : q ∈ S) {t : BiTape (NonBlank Γ₀)}
    (h : TM0.step M ⟨q, toTape t⟩ = none) :
    (ofTM0 M S hS).step ⟨some ⟨q, hq⟩, t⟩ = some ⟨none, t⟩
Uses 3 · Used by 2
Statement usesNon-blank symbols · Single-tape simulation of a Post–Turing machine · Post–Turing reading of a tape over the non-blank symbols
Used byThe simulating machine halts exactly when the Post–Turing machine halts · The single-tape simulation outputs within one extra step

TheoremEach TM0 step is one step of the simulation#✓fully proved

Let \(M\) be a TM0 machine over a finite alphabet \(\Gamma_0\) with blank symbol \(b\) and at least one non-blank symbol, supported by a finite set \(S\) of states, and let \(\widehat{M}\) be the single-tape machine over the non-blank symbols \(N = \Gamma_0 \setminus \{b\}\) simulating \(M\). For a tape \(t\) over \(N\), write \(\tau(t)\) for the TM0 tape read from \(t\) cell by cell. If \(q \in S\) and one step of \(M\) takes the configuration \((q, \tau(t))\) to a configuration \((q', T')\), then \(q' \in S\) and there is a tape \(t'\) over \(N\) with \(\tau(t') = T'\) such that one step of \(\widehat{M}\) takes the configuration \((q, t)\) to the configuration \((q', t')\).

theorem step_ofTM0_of_step_eq_some {q : Λ} (hq : q ∈ S) {t : BiTape (NonBlank Γ₀)}
    {c : TM0.Cfg Γ₀ Λ} (h : TM0.step M ⟨q, toTape t⟩ = some c) :
    ∃ (hc : c.q ∈ S) (t' : BiTape (NonBlank Γ₀)), toTape t' = c.Tape ∧
      (ofTM0 M S hS).step ⟨some ⟨q, hq⟩, t⟩ = some ⟨some ⟨c.q, hc⟩, t'⟩
Uses 6 · Used by 2
Statement usesNon-blank symbols · Single-tape simulation of a Post–Turing machine · Post–Turing reading of a tape over the non-blank symbols
Proof usesHead symbol of a tape read from non-blank cells · Head moves commute with the Post–Turing reading of a tape · Writing commutes with the Post–Turing reading of a tape
Used byThe simulating machine halts exactly when the Post–Turing machine halts · Runs of a TM0 machine are runs of its single-tape simulation

TheoremRuns of a TM0 machine are runs of its single-tape simulation#✓fully proved

Let \(M\) be a TM0 machine over a finite alphabet \(\Gamma_0\) with blank symbol \(b\) and at least one non-blank symbol, supported by a finite set \(S\) of states, and let \(\widehat{M}\) be the single-tape machine over the non-blank symbols \(N = \Gamma_0 \setminus \{b\}\) simulating \(M\). For a tape \(t\) over \(N\), write \(\tau(t)\) for the TM0 tape read from \(t\) cell by cell. If \(M\) goes from a configuration \((q, T)\) to a configuration \((q', T')\) in exactly \(n\) steps, \(q \in S\), and \(\tau(t) = T\), then \(q' \in S\) and there is a tape \(t'\) over \(N\) with \(\tau(t') = T'\) such that \(\widehat{M}\) goes from the configuration \((q, t)\) to the configuration \((q', t')\) in exactly \(n\) steps.

theorem relatesInSteps_ofTM0 {c c' : TM0.Cfg Γ₀ Λ} {n : ℕ}
    (h : RelatesInSteps (fun a b ↦ b ∈ TM0.step M a) c c' n) (hc : c.q ∈ S)
    {t : BiTape (NonBlank Γ₀)} (ht : toTape t = c.Tape) :
    ∃ (hc' : c'.q ∈ S) (t' : BiTape (NonBlank Γ₀)), toTape t' = c'.Tape ∧
      RelatesInSteps (ofTM0 M S hS).TransitionRelation ⟨some ⟨c.q, hc⟩, t⟩
        ⟨some ⟨c'.q, hc'⟩, t'⟩ n
Uses 4 · Used by 2
Statement usesNon-blank symbols · Single-tape simulation of a Post–Turing machine · Post–Turing reading of a tape over the non-blank symbols
Proof usesEach TM0 step is one step of the simulation
Used byThe simulating machine halts exactly when the Post–Turing machine halts · The single-tape simulation outputs within one extra step

TheoremThe simulating machine halts exactly when the Post–Turing machine halts#✓fully proved

Let \(\Gamma_0\) be a finite alphabet with at least one non-blank symbol, let \(M\) be a Post–Turing machine over \(\Gamma_0\) supported by the finite set of states \(S\), and let \(l\) be a word of non-blank symbols of \(\Gamma_0\). The single-tape machine simulating \(M\) halts on the input \(l\) if and only if \(M\), started on \(l\), halts.

theorem haltsOn_ofTM0_iff (l : List (NonBlank Γ₀)) :
    (ofTM0 M S hS).HaltsOn l ↔ (TM0.eval M (l.map Subtype.val)).Dom
Uses 8 · Used by 1
Statement usesHalting on an input · Non-blank symbols · Single-tape simulation of a Post–Turing machine
Proof usesRuns of a TM0 machine are runs of its single-tape simulation · The simulation halts one step after the TM0 machine · Each TM0 step is one step of the simulation · Post–Turing reading of a tape over the non-blank symbols · The Post–Turing reading of an input tape
Used byThe recognizer halts iff the multi-stack machine does

TheoremThe single-tape simulation outputs within one extra step#✓fully proved

Let \(\Gamma_0\) be a finite alphabet with at least one non-blank symbol, let \(M\) be a Post–Turing machine over \(\Gamma_0\) supported by the finite set of states \(S\), and let \(l\) and \(l'\) be words of non-blank symbols of \(\Gamma_0\). If \(M\), started on \(l\), reaches in exactly \(n\) steps a configuration \(c\) in which it halts, and the tape of \(c\) holds \(l'\) starting at the head with blanks everywhere else, then the single-tape machine simulating \(M\) outputs \(l'\) on the input \(l\) within \(n + 1\) steps: its run from the initial configuration on \(l\) reaches, in at most \(n + 1\) steps, the halting state with the tape holding exactly \(l'\), starting at the head.

theorem outputsWithinTime_ofTM0 {l l' : List (NonBlank Γ₀)} {c : TM0.Cfg Γ₀ Λ} {n : ℕ}
    (hc : RelatesInSteps (fun a b ↦ b ∈ TM0.step M a) (TM0.init (l.map Subtype.val)) c n)
    (hh : TM0.step M c = none) (ht : c.Tape = Tape.mk₁ (l'.map Subtype.val)) :
    (ofTM0 M S hS).OutputsWithinTime l l' (n + 1)
Uses 7 · Used by 2
Statement usesNon-blank symbols · Single-tape simulation of a Post–Turing machine
Proof usesRuns of a TM0 machine are runs of its single-tape simulation · The simulation halts one step after the TM0 machine · Post–Turing reading of a tape over the non-blank symbols · Distinct tapes of non-blank symbols read as distinct TM0 tapes · The Post–Turing reading of an input tape
Used byThe decider within time · The single-tape simulation has the same output

TheoremThe single-tape simulation has the same output#✓fully proved

Let \(\Gamma_0\) be a finite alphabet with at least one non-blank symbol, let \(M\) be a Post–Turing machine over \(\Gamma_0\) supported by the finite set of states \(S\), and let \(l\) and \(l'\) be words of non-blank symbols of \(\Gamma_0\). If \(M\), started on \(l\), halts in a configuration whose tape holds \(l'\) starting at the head, with blanks everywhere else, then the single-tape machine simulating \(M\) outputs \(l'\) on the input \(l\): its run from the initial configuration on \(l\) reaches the halting state with the tape holding exactly \(l'\), starting at the head.

theorem outputs_ofTM0 {l l' : List (NonBlank Γ₀)} {c : TM0.Cfg Γ₀ Λ}
    (hc : c ∈ StateTransition.eval (TM0.step M) (TM0.init (l.map Subtype.val)))
    (ht : c.Tape = Tape.mk₁ (l'.map Subtype.val)) : (ofTM0 M S hS).Outputs l l'
Uses 3 · Used by 1
Statement usesNon-blank symbols · Single-tape simulation of a Post–Turing machine
Proof usesThe single-tape simulation outputs within one extra step
Used byThe decider outputs the answer bit
50 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.