Single-tape machines decide the recursive predicates

DefinitionThe machine that prepends a symbol#✓fully proved

For a symbol \(c\), this is the single-tape machine with two states that, from its start state, writes back the symbol under the head, moves left and enters its second state, and from its second state writes \(c\) and halts without moving.

On an input word \(l\) it outputs \(c\) followed by \(l\).

def consComputer (c : Symbol) : SingleTapeTM Symbol where
  State := Bool
  q₀ := false
  tr q s := match q with
    | false => (⟨s, some .left⟩, some true)
    | true => (⟨some c, none⟩, none)

Used by 6

Used byThe decider within time · Correctness of the prepending machine · Prepending a symbol takes at most two steps · The decider outputs the answer bit · The recognizer halts iff the multi-stack machine does · The recognizer of a multi-stack machine

TheoremPrepending a symbol by stepping left#✓fully proved

Let \(c\) be a symbol and \(l\) a list of symbols, and consider the tape holding \(l\) from the head rightwards, all other cells blank. Writing back the symbol under the head, moving the head one cell left, and then writing \(c\) gives the tape holding the list \(c\) followed by \(l\) from the head rightwards, all other cells blank.

theorem write_moveLeft_mk₁ (c : Symbol) (l : List Symbol) :
    (((BiTape.mk₁ l).write (BiTape.mk₁ l).head).optionMove (some .left)).write (some c) =
      BiTape.mk₁ (c :: l)

Used by 1

Used byPrepending a symbol takes at most two steps

TheoremPrepending a symbol takes at most two steps#✓fully proved

For every symbol \(c\) and every word \(l\), the machine that prepends \(c\), started on \(l\), halts with output the word \(c\) followed by \(l\) within at most two steps.

theorem consComputer_outputsWithinTime (c : Symbol) (l : List Symbol) :
    (consComputer c).OutputsWithinTime l (c :: l) 2

Uses 2 · Used by 2

Statement usesThe machine that prepends a symbol

Proof usesPrepending a symbol by stepping left

Used byThe decider within time · Correctness of the prepending machine

TheoremCorrectness of the prepending machine#✓fully proved

For every symbol \(c\) and every word \(l\), the machine that prepends \(c\), started on \(l\), halts with output the word \(c\) followed by \(l\).

theorem consComputer_outputs (c : Symbol) (l : List Symbol) :
    (consComputer c).Outputs l (c :: l)

Uses 2 · Used by 2

Statement usesThe machine that prepends a symbol

Proof usesPrepending a symbol takes at most two steps

Used byThe decider outputs the answer bit · The recognizer halts iff the multi-stack machine does

DefinitionInput code of a bit word#✓fully proved

For a list of bits \(w\), let \(b_0, \dots, b_n\) be the reversal of \(w\) followed by \(\mathsf{true}\), reading \(\mathsf{true}\) as \(1\) and \(\mathsf{false}\) as \(0\). The input code of \(w\) is the natural number \(\sum_{i=0}^{n} b_i 2^i\). Its binary expansion, least significant bit first, is \(b_0, \dots, b_n\): the input stack on which the single-tape emulation starts for the input word \(w\).

def inputCode (w : List Bool) : ℕ := bitsVal (w.reverse ++ [true])

Uses 1 · Used by 3

Statement usesValue of a little-endian bit list

Used byComputable predicates are decidable by single-tape machines · R.e. predicates are recognizable by single-tape machines · Recovering a word from its input code

TheoremRecovering a word from its input code#✓fully proved

For every list of bits \(w\), reversing the binary encoding (least significant bit first) of the input code of \(w\) and then dropping the first bit of the result gives back \(w\).

theorem reverse_tail_encodeNat_inputCode (w : List Bool) :
    (encodeNat (inputCode w)).reverse.tail = w

Uses 3 · Used by 2

Statement usesInput code of a bit word

Proof usesValue of a little-endian bit list · Binary encoding, least significant bit first

Used byComputable predicates are decidable by single-tape machines · R.e. predicates are recognizable by single-tape machines

DefinitionInput decoding#✓fully proved

For a natural number \(m > 0\), let \(b_0, \dots, b_n\) be its binary expansion, least significant bit first, without trailing zeros. The input decoding of \(m\) is \(\sum_{i=0}^{n-1} b_{n-1-i} 2^i\), the value, least significant bit first, of the reversed expansion with its first bit dropped. The input decoding of \(0\), whose expansion is empty, is \(0\).

It undoes the encoding of input words: for every natural number \(k\) with binary expansion \(w\), least significant bit first, the input decoding of the number whose binary expansion, least significant bit first, is the reversal of \(w\) followed by \(1\) is \(k\).

def inputDecode (m : ℕ) : ℕ := bitsVal (encodeNat m).reverse.tail

Uses 1 · Used by 2

Statement usesValue of a little-endian bit list

Used byComputable predicates are decidable by single-tape machines · R.e. predicates are recognizable by single-tape machines

DefinitionInput cell of a bit#✓fully proved

Let \(M\) be a multi-stack machine with finitely many stacks, labels and internal states, and let \(e\) be a bijection from the alphabet of its input stack to the bits. The input cell of a bit \(b\) is the non-blank cell of the single-tape emulation of \(M\) whose bottom-of-stack flag is off, whose entry for the input stack is \(e^{-1}(b)\), and whose entries for all other stacks are empty.

def inCell (b : Bool) : NonBlank (TM2to1.Γ' tm.K tm.Γ) :=
  ⟨(false, Function.update (fun _ ↦ none) tm.k₀ (some (e.symm b))), fun h ↦ by
    have := congrFun (congrArg Prod.snd h) tm.k₀
    simp only [Function.update_self] at this
    cases this⟩

Uses 1 · Used by 10

Statement usesNon-blank symbols

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 decider outputs the answer bit · The recognizer halts iff the multi-stack machine does · 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

DefinitionThe bottom cell of the start tape#✓fully proved

Let \(M\) be a finite multi-stack machine whose input stack alphabet is identified with the bits. The bottom cell of the emulation's start tape is the cell flagged as the stack bottom that holds the symbol for \(\mathrm{true}\) on the input stack and nothing on every other stack.

def botCell : NonBlank (TM2to1.Γ' tm.K tm.Γ) :=
  ⟨(true, Function.update (fun _ ↦ none) tm.k₀ (some (e.symm true))),
    fun h ↦ Bool.noConfusion (congrArg Prod.fst h)⟩

Uses 1 · Used by 5

Statement usesNon-blank symbols

Used byThe decider within time · The decider outputs the answer bit · The recognizer halts iff the multi-stack machine does · The bottom cell followed by the input word is the emulation's start tape · The recognizer of a multi-stack machine

AbbreviationStates of the single-tape emulation#✓fully proved

Let \(M\) be a multi-stack machine with finitely many stacks, labels and internal states and a finite input alphabet. Its plain single-tape emulation is the translation of \(M\) to a single-tape machine with a finite store, followed by the translation of that machine to a plain single-tape machine, whose states are pairs of a statement of the intermediate machine, or the halting state, and an internal state. This is the finite set of those pairs whose first entry is the halting state or a statement occurring in the program of one of the labels that the first translation produces from the labels of \(M\).

The emulation only visits states in this set.

noncomputable abbrev emuSupport : Finset (TM1to0.Λ' (TM2to1.tr tm.m)) :=
  TM1to0.trStmts (TM2to1.tr tm.m) (TM2to1.trSupp tm.m Finset.univ)

Used by 4

Used byThe decider within time · The decider outputs the answer bit · Finite single-tape emulation of a multi-stack machine · The recognizer halts iff the multi-stack machine does

DefinitionFinite single-tape emulation of a multi-stack machine#✓fully proved

Let \(M\) be a multi-stack machine with finitely many stacks, labels and internal states, and with finite stack alphabets. Its finite single-tape emulation is the single-tape machine that runs the plain single-tape emulation of \(M\) (through a single-tape machine with a finite store) step for step: its states are those in the finite set of states the emulation visits, and its tape alphabet is the set of non-blank cells of the emulation, where a cell is a bottom-of-stack flag together with an optional symbol for each stack.

noncomputable def emuTM : SingleTapeTM (NonBlank (TM2to1.Γ' tm.K tm.Γ)) :=
  ofTM0 (TM2ToTM0.tr tm.m) (emuSupport tm)
    (TM2ToTM0.tr_supports tm.m (TM2ToTM0.supports_univ tm.m))

Uses 6 · Used by 4

Statement usesNon-blank symbols · States of the single-tape emulation · Single-tape simulation of a Post–Turing machine · A multi-stack machine is supported by all its labels · Two-step single-tape translation of a multi-stack machine · The emulation visits finitely many states

Used byThe decider within time · The decider outputs the answer bit · The recognizer halts iff the multi-stack machine does · The recognizer of a multi-stack machine

DefinitionThe recognizer of a multi-stack machine#✓fully proved

Let \(M\) be a finite multi-stack machine all of whose stack alphabets are finite, and let \(e\) be an identification of the alphabet of its input stack with the booleans. The recognizer of \(M\) is the single-tape machine, over the non-blank cells of the multi-stack-to-single-tape translation of \(M\), that first runs the machine prepending the bottom cell determined by \(M\) and \(e\) (the bottom-flagged cell holding \(e^{-1}(\mathrm{true})\) on the input stack and nothing on the other stacks) to its input and, when that machine halts, runs the single-tape emulation of \(M\).

noncomputable def recognizerTM : SingleTapeTM (NonBlank (TM2to1.Γ' tm.K tm.Γ)) :=
  compComputer (consComputer (botCell tm e)) (emuTM tm)

Uses 4 · Used by 3

Statement usesNon-blank symbols · The bottom cell of the start tape · Finite single-tape emulation of a multi-stack machine · The machine that prepends a symbol

Used byThe decider of a multi-stack machine · The recognizer halts iff the multi-stack machine does · R.e. predicates are recognizable by single-tape machines

TheoremThe bottom cell followed by the input word is the emulation's start tape#✓fully proved

Let \(M\) be a multi-stack machine with finitely many stacks, labels and internal states, and let \(e\) be a bijection from the alphabet of its input stack to the bits. For every list of bits \(w\), the bottom cell followed by the input cells of the bits of \(w\), read as cells of the emulation, is the start tape that the single-tape emulation assigns to the input stack obtained by applying \(e^{-1}\) to each entry of the reversal of \(w\) followed by \(\mathsf{true}\).

theorem map_val_botCell_cons (w : List Bool) :
    (botCell tm e :: w.map (inCell tm e)).map Subtype.val =
      TM2to1.trInit tm.k₀ ((w.reverse ++ [true]).map e.symm)

Uses 3 · Used by 3

Statement usesNon-blank symbols · The bottom cell of the start tape · Input cell of a bit

Used byThe decider within time · The decider outputs the answer bit · The recognizer halts iff the multi-stack machine does

TheoremThe recognizer halts iff the multi-stack machine does#✓fully proved

Let \(M\) be a multi-stack machine with finitely many stacks, labels and internal states and with finite stack alphabets, and let \(e\) be a bijection from the alphabet of its input stack to the bits. For every list of bits \(w\), the recognizer built from \(M\) and \(e\) halts on the word of input cells of the bits of \(w\) if and only if \(M\) halts when started on the input stack obtained by applying \(e^{-1}\) to each entry of the reversal of \(w\) followed by \(\mathsf{true}\).

theorem haltsOn_recognizerTM_iff (w : List Bool) :
    (recognizerTM tm e).HaltsOn (w.map (inCell tm e)) ↔
      TM2HaltsOn tm ((w.reverse ++ [true]).map e.symm)

Uses 19 · Used by 1

Statement usesHalting on an input · Non-blank symbols · Input cell of a bit · The recognizer of a multi-stack machine · Halting of a multi-stack machine on an input

Proof usesHalting agrees with evaluation for multi-stack machines · The bottom cell of the start tape · States of the single-tape emulation · Finite single-tape emulation of a multi-stack machine · The bottom cell followed by the input word is the emulation's start tape · The machine that prepends a symbol · Correctness of the prepending machine · Halting of a composite · The simulating machine halts exactly when the Post–Turing machine halts · Single-tape simulation of a Post–Turing machine · A multi-stack machine is supported by all its labels · Two-step single-tape translation of a multi-stack machine · The emulation halts iff the multi-stack machine halts · The emulation visits finitely many states

Used byR.e. predicates are recognizable by single-tape machines

TheoremThe emulation's final tape#✓fully proved

Let \(M\) be a multi-stack machine with finitely many stacks, labels and internal states and a finite input alphabet, let \(L\) be a list of symbols of its input stack, and suppose that \(M\), started with \(L\) on its input stack and every other stack empty, halts at the configuration \(c\). Then its plain single-tape emulation, started on the tape that holds the symbols of \(L\) bottom first on the input stack with the first cell flagged as the bottom, halts at a configuration \(c_0\) for which there is a list \(L'\) of columns, each holding an optional symbol for every stack and padded with blank columns, such that for every stack \(k\) the entries of \(L'\) for \(k\) are the symbols of stack \(k\) of \(c\) listed bottom first, followed by blanks, and the tape of \(c_0\) is blank to the left of the head and holds \(L'\) from the head rightwards, with the bottom-of-stack flag set on its first cell and cleared on all others.

theorem exists_mem_eval_tr (L : List (tm.Γ tm.k₀)) {c : tm.Cfg}
    (hc : c ∈ StateTransition.eval tm.step (initList tm L)) :
    ∃ c₀ ∈ StateTransition.eval (TM0.step (TM2ToTM0.tr tm.m))
        (TM0.init (TM2to1.trInit tm.k₀ L)),
      ∃ L' : ListBlank (∀ k, Option (tm.Γ k)),
        (∀ k, L'.map (proj k) = ListBlank.mk ((c.stk k).map some).reverse) ∧
          c₀.Tape = Tape.mk' ∅ (TM2to1.addBottom L')

Uses 2 · Used by 1

Statement usesTwo-step single-tape translation of a multi-stack machine

Proof usesThe initial configuration of a bundled multi-stack machine

Used byThe decider outputs the answer bit

TheoremStacks of height at most one give a one-cell tape#✓fully proved

Let \(M\) be a finite multi-stack machine, and let \(S\) assign to every stack \(k\) of \(M\) a list \(S_k\) of length at most \(1\). Let \(L'\) be a tape of stack columns whose \(k\)-th track, for every \(k\), is \(S_k\) laid out bottom first and followed by blanks. Then adding the bottom marker to \(L'\), as in the translation of \(M\) to a single-tape machine, gives the tape whose first cell is flagged as the bottom and holds the top of \(S_k\) on every stack \(k\) (nothing if \(S_k\) is empty), followed by blank cells.

theorem addBottom_eq_of_length_le_one {S : ∀ k, List (tm.Γ k)} (hS : ∀ k, (S k).length ≤ 1)
    {L' : ListBlank (∀ k, Option (tm.Γ k))}
    (hL' : ∀ k, L'.map (proj k) = ListBlank.mk ((S k).map some).reverse) :
    TM2to1.addBottom L' = ListBlank.mk [((true, fun k ↦ (S k).head?) : TM2to1.Γ' tm.K tm.Γ)]

Used by 2

Used byThe decider within time · The decider outputs the answer bit

DefinitionThe answer bit of a cell#✓fully proved

Let \(M\) be a finite multi-stack machine whose output stack alphabet is identified with the bits. The answer read from a non-blank cell of the single-tape emulation of \(M\) is \(\mathrm{true}\) exactly when the cell holds the symbol for \(\mathrm{true}\) on the output stack.

noncomputable def cellAnswer (x : NonBlank (TM2to1.Γ' tm.K tm.Γ)) : Bool :=
  decide (x.1.2 tm.k₁ = some (e₁.symm true))

Uses 1 · Used by 5

Statement usesNon-blank symbols

Used byThe answer machine runs in one step · The decider within time · The answer machine · The answer machine outputs the answer of a one-cell input · The decider outputs the answer bit

DefinitionThe answer machine#✓fully proved

Let \(M\) be a finite multi-stack machine whose stack alphabets are all finite, with its input and output stack alphabets identified with the bits. The answer machine of \(M\) is the single-tape machine over the non-blank cells of the single-tape emulation of \(M\) with a single state that, in one step, replaces the symbol under the head by the input-bit cell for the answer read from that cell (the answer \(\mathrm{false}\) if the cell is blank), does not move, and halts.

noncomputable def answerTM : SingleTapeTM (NonBlank (TM2to1.Γ' tm.K tm.Γ)) where
  State := Unit
  q₀ := ()
  tr _ s := (⟨some (inCell tm e (s.elim false (cellAnswer tm e₁))), none⟩, none)

Uses 3 · Used by 5

Statement usesNon-blank symbols · The answer bit of a cell · Input cell of a bit

Used byThe answer machine runs in one step · The decider within time · The answer machine outputs the answer of a one-cell input · The decider of a multi-stack machine · The decider outputs the answer bit

TheoremThe answer machine outputs the answer of a one-cell input#✓fully proved

Let \(M\) be a finite multi-stack machine whose stack alphabets are all finite, with its input and output stack alphabets identified with the bits. For every non-blank cell \(x\) of the single-tape emulation of \(M\), the answer machine of \(M\), started on the one-cell input \(x\), halts with the one-cell output holding the input-bit cell for the answer read from \(x\).

theorem answerTM_outputs (x : NonBlank (TM2to1.Γ' tm.K tm.Γ)) :
    (answerTM tm e e₁).Outputs [x] [inCell tm e (cellAnswer tm e₁ x)]

Uses 4 · Used by 1

Statement usesNon-blank symbols · The answer machine · The answer bit of a cell · Input cell of a bit

Used byThe decider outputs the answer bit

DefinitionThe decider of a multi-stack machine#✓fully proved

Let \(M\) be a finite multi-stack machine whose stack alphabets are all finite, with its input and output stack alphabets identified with the bits. The decider of \(M\) is the single-tape machine over the non-blank cells of the single-tape emulation of \(M\) that runs the recognizer of \(M\) and, once the recognizer halts, runs the answer machine of \(M\) on the resulting tape.

noncomputable def deciderTM : SingleTapeTM (NonBlank (TM2to1.Γ' tm.K tm.Γ)) :=
  compComputer (recognizerTM tm e) (answerTM tm e e₁)

Uses 3 · Used by 4

Statement usesNon-blank symbols · The answer machine · The recognizer of a multi-stack machine

Used byThe decider within time · Problems in P are decided in polynomial time by single-tape machines · The decider outputs the answer bit · Computable predicates are decidable by single-tape machines

TheoremThe decider outputs the answer bit#✓fully proved

Let \(M\) be a finite multi-stack machine whose stack alphabets are all finite, with its input and output stack alphabets identified with the bits, and let \(w\) be a word of bits. Suppose that \(M\), started with the input stack holding the reverse of \(w\) followed by \(\mathrm{true}\), halts with the output stack holding a list \(u\) of length at most \(1\), every other stack empty and its variable back at its initial value. Then there is a bit \(b\) such that the decider of \(M\), started on the input-bit cells of \(w\), halts with the one-cell output holding the input-bit cell for \(b\), and \(b = \mathrm{true}\) exactly when \(u\) is nonempty and its first symbol is the symbol for \(\mathrm{true}\).

theorem deciderTM_outputs {w : List Bool} {out : List (tm.Γ tm.k₁)} (hout : out.length ≤ 1)
    (h : haltList tm out ∈
      StateTransition.eval tm.step (initList tm ((w.reverse ++ [true]).map e.symm))) :
    ∃ b : Bool, (deciderTM tm e e₁).Outputs (w.map (inCell tm e)) [inCell tm e b] ∧
      (b = true ↔ out.head? = some (e₁.symm true))

Uses 19 · Used by 1

Statement usesNon-blank symbols · The decider of a multi-stack machine · Input cell of a bit

Proof usesStacks of height at most one give a one-cell tape · 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 · States of the single-tape emulation · Finite single-tape emulation of a multi-stack machine · The emulation's final tape · The bottom cell followed by the input word is the emulation's start tape · Outputs compose · The machine that prepends a symbol · Correctness of the prepending machine · The single-tape simulation has the same output · A multi-stack machine is supported by all its labels · Two-step single-tape translation of a multi-stack machine · The emulation visits finitely many states

Used byComputable predicates are decidable by single-tape machines

TheoremR.e. predicates are recognizable by single-tape machines#✓fully proved

R.e. predicates are recognizable by single-tape machines.

theorem SingleTapeRecognizable.of_rePred {p : α → Prop} (hp : REPred p) :
    SingleTapeRecognizable p

Uses 15 · Used by 1

Statement usesPredicates recognizable by a single-tape Turing machine

Proof usesHalting on an input · Non-blank symbols · The recognizer halts iff the multi-stack machine does · Input cell of a bit · Input code of a bit word · Input decoding · The recognizer of a multi-stack machine · Recovering a word from its input code · Recursively enumerable predicates are closed under conjunction · Existential projection preserves recursive enumerability · Halting of a multi-stack machine on an input · Value of a little-endian bit list · Binary encoding, least significant bit first · Every r.e. predicate is the halting set of a machine with finite alphabets

Used bySingle-tape recognizable predicates are exactly the r.e. predicates

TheoremComputable predicates are decidable by single-tape machines#✓fully proved

Let \(\alpha\) be a type with a primitive recursive encoding into \(\mathbb{N}\), and let \(p\) be a computable predicate on \(\alpha\), that is, one whose indicator function \(\alpha \to \{0, 1\}\) is computable. Then \(p\) is decidable by a single-tape Turing machine.

theorem SingleTapeDecidable.of_computablePred {p : α → Prop} (hp : ComputablePred p) :
    SingleTapeDecidable p

Uses 12 · Used by 1

Statement usesPredicates decidable by a single-tape Turing machine

Proof usesNon-blank symbols · The decider of a multi-stack machine · The decider outputs the answer bit · Input cell of a bit · Input code of a bit word · Input decoding · Recovering a word from its input code · Value of a little-endian bit list · Binary encoding, least significant bit first · The wrapped machine of a code · The wrapped machine computes the function a code evaluates

Used bySingle-tape decidable predicates are exactly the computable predicates

DefinitionPushing a cell onto a coded tape#✓fully proved

For any type \(\Sigma\), an element \(x\) of \(\Sigma \cup \{\bot\}\) (with \(\bot\) the blank) and a finite list \(l\) over \(\Sigma \cup \{\bot\}\), the push of \(x\) onto \(l\) is the empty list when \(x = \bot\) and \(l\) is empty, and otherwise the list obtained by prepending \(x\) to \(l\).

def SingleTapeTM.codedCons {Symbol : Type} :
    Option Symbol → List (Option Symbol) → List (Option Symbol)
  | none, [] => []
  | x, l => x :: l

Used by 6

Used byAcceptance by an NTM with finite state and tape alphabets is r.e · One step of a single-tape machine on coded configurations · The coded step commutes with coding · Pushing a cell onto a coded tape is primitive recursive · The coded step of a single-tape machine is primitive recursive · Pushing onto a stack tape, on cell lists

TheoremThe head of a stack tape is the first entry of its list#✓fully proved

For every one-sided tape \(s\) over an alphabet \(\Sigma\), stored as a finite list of cells in \(\Sigma \cup \{\bot\}\) (with \(\bot\) the blank) that does not end in \(\bot\), the symbol at the head of \(s\) is the first entry of that list, and the blank \(\bot\) when the list is empty.

theorem head_eq_headI (s : StackTape Symbol) : s.head = s.toList.headI

Used by 2

Used byAcceptance by an NTM with finite state and tape alphabets is r.e · The coded step commutes with coding

TheoremTail of a stack tape, on cell lists#✓fully proved

Let \(s\) be a stack tape, a one-sided tape stored as its list of cells without trailing blanks. Then the cell list of the tail of \(s\) is the tail of the cell list of \(s\), the tail of the empty list being empty.

theorem toList_tail (s : StackTape Symbol) : s.tail.toList = s.toList.tail

Used by 3

Used byA machine that, on a blank cell, writes a blank and does not move is a linear bounded automaton · Acceptance by an NTM with finite state and tape alphabets is r.e · The coded step commutes with coding

TheoremPushing onto a stack tape, on cell lists#✓fully proved

Let \(s\) be a stack tape, a one-sided tape stored as its list of cells without trailing blanks, and \(x\) a cell content, either a symbol or blank. Then the cell list of the tape obtained by pushing \(x\) onto \(s\) is the coded push of \(x\) applied to the cell list of \(s\): \(x\) prepended to it, except that pushing a blank onto the empty tape gives the empty list.

theorem toList_cons (x : Option Symbol) (s : StackTape Symbol) :
    (cons x s).toList = SingleTapeTM.codedCons x s.toList

Uses 1 · Used by 2

Statement usesPushing a cell onto a coded tape

Used byAcceptance by an NTM with finite state and tape alphabets is r.e · The coded step commutes with coding

TheoremPushing a cell onto a coded tape is primitive recursive#✓fully proved

Let \(\Sigma\) be a type with a primitive recursive coding, and let \(x\) be a cell content, either a symbol of \(\Sigma\) or blank. Then the coded push of \(x\), the map on lists of cell contents that prepends \(x\) to a list, except that it sends the empty list to the empty list when \(x\) is blank, is primitive recursive.

theorem primrec_codedCons [Primcodable Symbol] (x : Option Symbol) :
    Primrec (codedCons x)

Uses 1 · Used by 2

Statement usesPushing a cell onto a coded tape

Used byAcceptance by an NTM with finite state and tape alphabets is r.e · The coded step of a single-tape machine is primitive recursive

TheoremBinary codes of natural numbers in a tape alphabet are primitive recursive#✓fully proved

Let \(\Sigma\) be a type with a primitive recursive coding and \(\iota\) any map from the Booleans to \(\Sigma\). Then the map sending \(n \in \mathbb{N}\) to the word over \(\Sigma\) obtained by applying \(\iota\) letterwise to the binary code of \(n\) (least significant bit first, the empty word for \(0\)) is primitive recursive.

theorem primrec_map_encodeNat [Primcodable Symbol] (ι : Bool → Symbol) :
    Primrec fun n ↦ (encodeNat n).map ι

Uses 1 · Used by 3

Proof usesBinary encoding, least significant bit first

Used byA predicate recognized by a single-tape NTM is recognized by a deterministic single-tape machine · A predicate decided by a single-tape machine is computable · The halting set of a single-tape machine on binary inputs is r.e

TheoremHalting is termination of the run#✓fully proved

A single-tape machine \(M\) halts on an input word \(l\) if and only if iterating the step function of \(M\) from the initial configuration on \(l\), until a configuration with no successor is reached, terminates.

theorem haltsOn_iff_dom_eval {l : List Symbol} :
    tm.HaltsOn l ↔ (StateTransition.eval tm.step (tm.initCfg l)).Dom

Uses 1 · Used by 1

Statement usesHalting on an input

Used byThe halting set of a single-tape machine is r.e

TheoremOutputs are the ends of runs#✓fully proved

A single-tape machine \(M\) outputs the word \(l'\) on the input word \(l\) if and only if iterating the step function of \(M\) from the initial configuration on \(l\), until a configuration with no successor is reached, terminates at the halting configuration for \(l'\): the halting state, with \(l'\) written from the head rightwards and every other cell blank.

theorem outputs_iff_mem_eval {l l' : List Symbol} :
    tm.Outputs l l' ↔ tm.haltCfg l' ∈ StateTransition.eval tm.step (tm.initCfg l)

Used by 1

Used byA predicate decided by a single-tape machine is computable

AbbreviationCoded configurations of a single-tape machine#✓fully proved

For a single-tape Turing machine with state set \(Q\) and tape alphabet \(\Sigma\), write \(\bot\) for an absent value. A coded configuration is a quadruple \((q, h, L, R)\) where \(q \in Q \cup \{\bot\}\) is the state (\(\bot\) meaning halted), \(h \in \Sigma \cup \{\bot\}\) is the symbol under the head (\(\bot\) being the blank), and \(L\) and \(R\) are finite lists over \(\Sigma \cup \{\bot\}\), meant as the cells to the left and to the right of the head.

abbrev CodedCfg : Type :=
  Option tm.State × Option Symbol × List (Option Symbol) × List (Option Symbol)

Used by 8

Used byHalting of a machine running in computable space is computable · One step of a single-tape machine on coded configurations · The coded step commutes with coding · Running the coded step mirrors running the machine · The final tape of a run is partial recursive in the input word · The coded step of a single-tape machine is primitive recursive · The code of the initial configuration is primitive recursive · Code of a single-tape configuration

DefinitionCode of a single-tape configuration#✓fully proved

The code of a configuration of a single-tape machine is the quadruple consisting of its state (or the halting state), the symbol under the head (or blank), and the lists of cells, without trailing blanks, of the tapes to the left and to the right of the head.

def Cfg.toCodedCfg {tm : SingleTapeTM Symbol} (c : tm.Cfg) : tm.CodedCfg :=
  (c.state, c.BiTape.head, c.BiTape.left.toList, c.BiTape.right.toList)

Uses 1 · Used by 5

Statement usesCoded configurations of a single-tape machine

Used byHalting of a machine running in computable space is computable · The coded step commutes with coding · Running the coded step mirrors running the machine · The final tape of a run is partial recursive in the input word · The code of the initial configuration is primitive recursive

DefinitionOne step of a single-tape machine on coded configurations#✓fully proved

Let \(M\) be a single-tape Turing machine with transition function \(\delta\), and write \(\bot\) both for the halting state and for the blank. For a finite list \(l\) of cells, let \(\mathrm{hd}(l)\) be the first entry of \(l\), the blank \(\bot\) when \(l\) is empty; let \(\mathrm{tl}(l)\) be \(l\) without its first entry, the empty list when \(l\) is empty; and for a cell \(w\) let \(w \cdot l\), the push of \(w\) onto \(l\), be \(l\) when \(w = \bot\) and \(l\) is empty, and \(w\) prepended to \(l\) otherwise. A coded configuration \((\bot, h, L, R)\) in the halting state has no successor. For a running state \(q\), write \(\delta(q, h) = ((w, d), q')\), where \(w\) is the symbol to write, \(d\) is either no move or a direction, and \(q'\) is the new state, possibly the halting state \(\bot\). The successor of \((q, h, L, R)\) is \((q', w, L, R)\) if \(d\) is no move, \((q', \mathrm{hd}(L), \mathrm{tl}(L), w \cdot R)\) if \(d\) is left, and \((q', \mathrm{hd}(R), w \cdot L, \mathrm{tl}(R))\) if \(d\) is right.

def codedStep : tm.CodedCfg → Option tm.CodedCfg
  | (none, _) => none
  | (some q, h, L, R) =>
    some <| match tm.tr q h with
      | (⟨wr, none⟩, q') => (q', wr, L, R)
      | (⟨wr, some .left⟩, q') => (q', L.headI, L.tail, codedCons wr R)
      | (⟨wr, some .right⟩, q') => (q', R.headI, codedCons wr L, R.tail)

Uses 2 · Used by 5

Statement usesCoded configurations of a single-tape machine · Pushing a cell onto a coded tape

Used byHalting of a machine running in computable space is computable · The coded step commutes with coding · Running the coded step mirrors running the machine · The final tape of a run is partial recursive in the input word · The coded step of a single-tape machine is primitive recursive

TheoremThe coded step commutes with coding#✓fully proved

For every configuration \(c\) of a single-tape machine \(M\), the code of \(c\) has no successor under the coded step exactly when \(c\) has no successor under the step function of \(M\), and otherwise the coded step sends the code of \(c\) to the code of the successor of \(c\).

theorem codedStep_toCodedCfg (c : tm.Cfg) :
    tm.codedStep c.toCodedCfg = (tm.step c).map Cfg.toCodedCfg

Uses 7 · Used by 2

Statement usesCode of a single-tape configuration · Coded configurations of a single-tape machine · One step of a single-tape machine on coded configurations

Proof usesPushing a cell onto a coded tape · The head of a stack tape is the first entry of its list · Pushing onto a stack tape, on cell lists · Tail of a stack tape, on cell lists

Used byHalting of a machine running in computable space is computable · Running the coded step mirrors running the machine

TheoremThe coded step of a single-tape machine is primitive recursive#✓fully proved

Let \(M\) be a single-tape Turing machine over a finite alphabet \(\Sigma\), and fix primitive recursive codings of \(\Sigma\) and of the states of \(M\). Then the coded step of \(M\), which maps a coded configuration to the coded configuration after one step of \(M\) and has no value when the state is the halting state, is primitive recursive.

theorem primrec_codedStep [Primcodable Symbol] [Primcodable tm.State] :
    Primrec tm.codedStep

Uses 5 · Used by 2

Statement usesCoded configurations of a single-tape machine · One step of a single-tape machine on coded configurations

Proof usesPushing a cell onto a coded tape · Pushing a cell onto a coded tape is primitive recursive · Joint primitive recursion over a finite first argument

Used byHalting of a machine running in computable space is computable · The final tape of a run is partial recursive in the input word

TheoremRunning the coded step mirrors running the machine#✓fully proved

For every configuration \(c\) of a single-tape machine \(M\), iterating the coded step from the code of \(c\) until a coded configuration with no successor is reached terminates exactly when iterating the step function of \(M\) from \(c\) until a configuration with no successor is reached does, and then it ends at the code of the configuration where the run of \(M\) from \(c\) ends.

theorem eval_codedStep (c : tm.Cfg) :
    StateTransition.eval tm.codedStep c.toCodedCfg =
      Cfg.toCodedCfg <$> StateTransition.eval tm.step c

Uses 4 · Used by 1

Statement usesCode of a single-tape configuration · Coded configurations of a single-tape machine · One step of a single-tape machine on coded configurations

Proof usesThe coded step commutes with coding

Used byThe final tape of a run is partial recursive in the input word

TheoremThe code of the initial configuration is primitive recursive#✓fully proved

Let \(M\) be a single-tape Turing machine over a finite alphabet \(\Sigma\), and fix primitive recursive codings of \(\Sigma\) and of the states of \(M\). Then the map sending an input word \(w\) over \(\Sigma\) to the code of the initial configuration of \(M\) on \(w\) is primitive recursive.

theorem primrec_toCodedCfg_initCfg [Primcodable Symbol] [Primcodable tm.State] :
    Primrec fun l : List Symbol ↦ (tm.initCfg l).toCodedCfg

Uses 2 · Used by 2

Statement usesCode of a single-tape configuration · Coded configurations of a single-tape machine

Used byHalting of a machine running in computable space is computable · The final tape of a run is partial recursive in the input word

TheoremThe final tape of a run is partial recursive in the input word#✓fully proved

Let \(M\) be a single-tape Turing machine whose finite alphabet \(\Sigma\) carries a primitive recursive coding. The partial function sending an input word \(l\) over \(\Sigma\) to the final tape of the run of \(M\) on \(l\) (the symbol under the head, and the lists of cells to the left and to the right of the head), defined exactly when \(M\) halts on \(l\), is partial recursive.

theorem partrec_eval [Primcodable Symbol] :
    Partrec fun l : List Symbol ↦ (StateTransition.eval tm.step (tm.initCfg l)).map
      fun c ↦ (c.BiTape.head, c.BiTape.left.toList, c.BiTape.right.toList)

Uses 6 · Used by 2

Proof usesCode of a single-tape configuration · Coded configurations of a single-tape machine · One step of a single-tape machine on coded configurations · Running the coded step mirrors running the machine · The coded step of a single-tape machine is primitive recursive · The code of the initial configuration is primitive recursive

Used byA predicate decided by a single-tape machine is computable · The halting set of a single-tape machine is r.e

TheoremThe halting set of a single-tape machine is r.e#✓fully proved

Let \(M\) be a single-tape Turing machine over a finite alphabet \(\Sigma\), and fix a primitive recursive coding of \(\Sigma\). Then the set of input words over \(\Sigma\) on which \(M\) halts is recursively enumerable.

theorem rePred_haltsOn [Primcodable Symbol] : REPred tm.HaltsOn

Uses 3 · Used by 1

Statement usesHalting on an input

Proof usesHalting is termination of the run · The final tape of a run is partial recursive in the input word

Used byThe halting set of a single-tape machine on binary inputs is r.e

TheoremThe halting set of a single-tape machine on binary inputs is r.e#✓fully proved

Let \(M\) be a single-tape Turing machine over a finite alphabet \(\Sigma\) and \(\iota\) any map from the Booleans to \(\Sigma\). Then the set of natural numbers \(n\) such that \(M\) halts on the word obtained by applying \(\iota\) letterwise to the binary code of \(n\) (least significant bit first, the empty word for \(0\)) is recursively enumerable.

theorem rePred_haltsOn_encodeNat (ι : Bool → Symbol) :
    REPred fun n : ℕ ↦ tm.HaltsOn ((encodeNat n).map ι)

Uses 3 · Used by 1

Statement usesHalting on an input

Proof usesBinary codes of natural numbers in a tape alphabet are primitive recursive · The halting set of a single-tape machine is r.e

Used byA predicate recognized by a single-tape machine is r.e

TheoremA predicate recognized by a single-tape machine is r.e#✓fully proved

A predicate recognized by a single-tape machine is r.e.

theorem SingleTapeRecognizable.rePred (h : SingleTapeRecognizable p) : REPred p

Uses 3 · Used by 1

Statement usesPredicates recognizable by a single-tape Turing machine

Proof usesHalting on an input · The halting set of a single-tape machine on binary inputs is r.e

Used bySingle-tape recognizable predicates are exactly the r.e. predicates

TheoremA predicate decided by a single-tape machine is computable#✓fully proved

The decider's answer is the symbol under the head of its final tape.

theorem SingleTapeDecidable.computablePred (h : SingleTapeDecidable p) : ComputablePred p

Uses 4 · Used by 1

Statement usesPredicates decidable by a single-tape Turing machine

Proof usesOutputs are the ends of runs · The final tape of a run is partial recursive in the input word · Binary codes of natural numbers in a tape alphabet are primitive recursive

Used bySingle-tape decidable predicates are exactly the computable predicates

TheoremSingle-tape decidable predicates are exactly the computable predicates#✓fully proved

Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). A predicate \(p\) on \(\alpha\) is decidable by a single-tape machine if and only if it is computable, that is, \(p\) is decidable and its Boolean characteristic function \(\alpha \to \mathrm{Bool}\) is computable.

theorem singleTapeDecidable_iff_computablePred : SingleTapeDecidable p ↔ ComputablePred p

Uses 3 · Used by 6

Statement usesPredicates decidable by a single-tape Turing machine

Proof usesA predicate decided by a single-tape machine is computable · Computable predicates are decidable by single-tape machines

Used byA single-tape machine decides the halting problem of a linear bounded automaton · A decidable predicate that no single-tape NTM recognizes · Single-tape decidable predicates are closed under complement · Post's theorem · Single-tape and multi-stack machines decide the same predicates · A URM-decidable predicate is decidable by a single-tape Turing machine

TheoremSingle-tape recognizable predicates are exactly the r.e. predicates#✓fully proved

Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). A predicate \(p\) on \(\alpha\) is recognizable by a single-tape machine if and only if it is recursively enumerable, that is, the partial function on \(\alpha\) that is defined, with a trivial value, exactly where \(p\) holds is partial recursive.

theorem singleTapeRecognizable_iff_rePred : SingleTapeRecognizable p ↔ REPred p

Uses 3 · Used by 7

Statement usesPredicates recognizable by a single-tape Turing machine

Proof usesR.e. predicates are recognizable by single-tape machines · A predicate recognized by a single-tape machine is r.e

Used byA predicate recognized by a single-tape NTM is recognized by a deterministic single-tape machine · Deterministic machines recognize NTM acceptance · Deterministic machines recognize NTM acceptance along a computable map · Single-tape co-recognizable predicates are those with an r.e. complement · Post's theorem · Single-tape and multi-stack machines recognize the same predicates · A URM-recognizable predicate is recognizable by a single-tape Turing machine

TheoremSingle-tape co-recognizable predicates are those with an r.e. complement#✓fully proved

Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). A predicate \(p\) on \(\alpha\) is co-recognizable by a single-tape machine if and only if its complement \(\neg p\) is recursively enumerable, that is, the partial function on \(\alpha\) that is defined, with a trivial value, exactly where \(\neg p\) holds is partial recursive.

theorem singleTapeCoRecognizable_iff_rePred_not :
    SingleTapeCoRecognizable p ↔ REPred fun a ↦ ¬p a

Uses 2 · Used by 1

Statement usesCo-recognizability by single-tape machines

Proof usesSingle-tape recognizable predicates are exactly the r.e. predicates

Used byPost's theorem

TheoremSingle-tape and multi-stack machines decide the same predicates#✓fully proved

Single-tape and multi-stack machines decide the same predicates.

theorem singleTapeDecidable_iff_tm2Decidable : SingleTapeDecidable p ↔ TM2Decidable p

Uses 4 · Used by 1

Statement usesPredicates decidable by a single-tape Turing machine · Decidability by multi-stack machines

Proof usesSingle-tape decidable predicates are exactly the computable predicates · Multi-stack decidable predicates are exactly the computable predicates

Used byThe halting problem for partial recursive codes is undecidable on single-tape machines

TheoremSingle-tape and multi-stack machines recognize the same predicates#✓fully proved

Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). A predicate \(p\) on \(\alpha\) is recognizable by a single-tape machine if and only if it is recognizable by a multi-stack machine.

theorem singleTapeRecognizable_iff_tm2Recognizable :
    SingleTapeRecognizable p ↔ TM2Recognizable p

Uses 4 · Used by 2

Statement usesPredicates recognizable by a single-tape Turing machine · Recognizability by multi-stack machines

Proof usesSingle-tape recognizable predicates are exactly the r.e. predicates · Multi-stack recognizable predicates are exactly the r.e. predicates

Used byThe halting problem for partial recursive codes is not co-recognizable on single-tape machines · The halting problem for partial recursive codes is recognizable on single-tape machines

TheoremPost's theorem#✓fully proved

Post's theorem for single-tape machines: a predicate is decidable iff it is recognizable and co-recognizable.

theorem singleTapeDecidable_iff_singleTapeRecognizable_and_singleTapeCoRecognizable :
    SingleTapeDecidable p ↔ SingleTapeRecognizable p ∧ SingleTapeCoRecognizable p

Uses 6 · Used by 2

Statement usesCo-recognizability by single-tape machines · Predicates decidable by a single-tape Turing machine · Predicates recognizable by a single-tape Turing machine

Proof usesSingle-tape co-recognizable predicates are those with an r.e. complement · Single-tape decidable predicates are exactly the computable predicates · Single-tape recognizable predicates are exactly the r.e. predicates

Used bySingle-tape decidable predicates are co-recognizable · Decidable predicates are recognizable by single-tape machines

TheoremDecidable predicates are recognizable by single-tape machines#✓fully proved

Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). If a predicate \(p\) on \(\alpha\) is decidable by a single-tape machine, then \(p\) is recognizable by a single-tape machine.

theorem SingleTapeDecidable.singleTapeRecognizable (h : SingleTapeDecidable p) :
    SingleTapeRecognizable p

Uses 4

Statement usesPredicates decidable by a single-tape Turing machine · Predicates recognizable by a single-tape Turing machine

Proof usesCo-recognizability by single-tape machines · Post's theorem

TheoremSingle-tape decidable predicates are co-recognizable#✓fully proved

Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). If a predicate \(p\) on \(\alpha\) is decidable by a single-tape machine, then \(p\) is co-recognizable by a single-tape machine, that is, its complement \(\neg p\) is recognizable by a single-tape machine.

theorem SingleTapeDecidable.singleTapeCoRecognizable (h : SingleTapeDecidable p) :
    SingleTapeCoRecognizable p

Uses 4

Statement usesCo-recognizability by single-tape machines · Predicates decidable by a single-tape Turing machine

Proof usesPredicates recognizable by a single-tape Turing machine · Post's theorem

TheoremSingle-tape decidable predicates are closed under complement#✓fully proved

Let \(\alpha\) be a primcodable type (it has an encoding \(\mathrm{encode} : \alpha \to \mathbb{N}\) whose decoding is primitive recursive). If a predicate \(p\) on \(\alpha\) is decidable by a single-tape machine, then so is its complement \(\neg p\).

theorem SingleTapeDecidable.not (h : SingleTapeDecidable p) :
    SingleTapeDecidable fun a ↦ ¬p a

Uses 2

Statement usesPredicates decidable by a single-tape Turing machine

Proof usesSingle-tape decidable predicates are exactly the computable predicates

TheoremThe halting problem for partial recursive codes is undecidable on single-tape machines#✓fully proved

For every \(n \in \mathbb{N}\), no single-tape machine decides whether a partial recursive code halts on input \(n\).

theorem not_singleTapeDecidable_halting (n : ℕ) :
    ¬SingleTapeDecidable fun c : Code ↦ (c.eval n).Dom

Sources

• Sipser, Theorem 5.1, for codes of partial recursive functions run on \(n\).

Uses 4

Statement usesPredicates decidable by a single-tape Turing machine

Proof usesDecidability by multi-stack machines · The halting problem is undecidable by multi-stack machines · Single-tape and multi-stack machines decide the same predicates

TheoremThe halting problem for partial recursive codes is recognizable on single-tape machines#✓fully proved

For every \(n \in \mathbb{N}\), the set of partial recursive codes whose program halts on input \(n\) is recognizable by a single-tape machine.

theorem singleTapeRecognizable_halting (n : ℕ) :
    SingleTapeRecognizable fun c : Code ↦ (c.eval n).Dom

Uses 4 · Used by 1

Statement usesPredicates recognizable by a single-tape Turing machine

Proof usesRecognizability by multi-stack machines · Single-tape and multi-stack machines recognize the same predicates · The halting problem is recognizable by multi-stack machines

Used byEmptiness of a linear bounded automaton on computable input slices is undecidable

TheoremThe halting problem for partial recursive codes is not co-recognizable on single-tape machines#✓fully proved

The halting problem for partial recursive codes is not co-recognizable on single-tape machines. For every \(n \in \mathbb{N}\), the set of partial recursive codes whose program halts on input \(n\) is not co-recognizable by a single-tape machine: no single-tape machine halts on exactly the codes whose program does not halt on input \(n\).

theorem not_singleTapeCoRecognizable_halting (n : ℕ) :
    ¬SingleTapeCoRecognizable fun c : Code ↦ (c.eval n).Dom

Sources

• Sipser, Corollary 4.23 (there for \(A_{TM}\)), with partial recursive codes run on \(n\).

Uses 5

Statement usesCo-recognizability by single-tape machines

Proof usesPredicates recognizable by a single-tape Turing machine · Recognizability by multi-stack machines · The halting problem is not co-recognizable by multi-stack machines · Single-tape and multi-stack machines recognize the same predicates

55 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.