Skip to content

Decidable and recognizable predicates on single-tape Turing machines

15 fully proved

Single Tape TM

DefinitionHalting on an input#✓fully proved

A single-tape Turing machine \(M\) halts on an input word \(w\) when its run from the initial configuration on \(w\) (the start state, with \(w\) written from the head position rightwards on an otherwise blank tape) reaches, in finitely many steps (possibly none), a configuration in the halting state.

def HaltsOn (tm : SingleTapeTM Symbol) (l : List Symbol) : Prop :=
  ∃ c : tm.Cfg, ReflTransGen tm.TransitionRelation (tm.initCfg l) c ∧ c.state = none
Used by 19
Used byHalting of a machine running in computable space is computable · Halting of a linear bounded automaton is decidable · Halting of a linear bounded automaton on binary codes is decidable · Space-bounded machines halt within the configuration bound · A single-tape machine decides the halting problem of a linear bounded automaton · Halting is termination of the run · The recognizer halts iff the multi-stack machine does · R.e. predicates are recognizable by single-tape machines · A predicate recognized by a single-tape machine is r.e · The halting set of a single-tape machine is r.e · The halting set of a single-tape machine on binary inputs is r.e · A machine that produces an output halts · Halting on an input is halting from the initial configuration · Predicates recognizable by a single-tape Turing machine · The simulating machine halts exactly when the Post–Turing machine halts · Halting of a composite · The fenced machine halts on some padding of a word iff the machine halts on it · Emptiness of a linear bounded automaton on computable input slices is undecidable · The fenced machine halts on no padding of a word iff the machine does not halt on it

DefinitionHalting from a configuration#✓fully proved

A single-tape Turing machine \(M\) halts from a configuration \(c\) when its run from \(c\) reaches, in finitely many steps (possibly none), a configuration in the halting state.

Equivalently, \(c\) is normalizable for the transition relation of \(M\), since the configurations in the halting state are exactly those without a successor; the same holds for CSLib's register machines.

def HaltsFrom (tm : SingleTapeTM Symbol) (c : tm.Cfg) : Prop :=
  ∃ c' : tm.Cfg, ReflTransGen tm.TransitionRelation c c' ∧ c'.state = none
Used by 5
Used byHalting from a configuration is normalizability · Halting from a configuration is invariant along a run · Configurations with the same successor halt together · Halting on an input is halting from the initial configuration · The fenced machine halts on some padding of a word iff the machine halts on it

TheoremHalting on an input is halting from the initial configuration#✓fully proved

A single-tape Turing machine \(M\) halts on an input word \(w\) if and only if \(M\) halts from the initial configuration on \(w\).

theorem haltsOn_iff_haltsFrom {tm : SingleTapeTM Symbol} {l : List Symbol} :
    tm.HaltsOn l ↔ tm.HaltsFrom (tm.initCfg l)
Uses 2 · Used by 1
Statement usesHalting from a configuration · Halting on an input
Used byThe fenced machine halts on some padding of a word iff the machine halts on it

TheoremOne step of a single-tape Turing machine#✓fully proved

Let \(M\) be a single-tape Turing machine, \(q\) a state of \(M\) other than the halting state and \(t\) a tape, and let the transition function of \(M\) at \(q\) and the symbol under the head of \(t\) (possibly blank) give the symbol \(s\) to write (possibly blank), the head movement \(d\) (left, right or none) and the next state \(q'\) (possibly the halting state). Then the configuration in state \(q\) with tape \(t\) has a successor, namely the configuration in state \(q'\) whose tape is obtained from \(t\) by writing \(s\) under the head and then moving the head by \(d\).

theorem step_some (tm : SingleTapeTM Symbol) (q : tm.State) (t : BiTape Symbol) :
    tm.step ⟨some q, t⟩ =
      some ⟨(tm.tr q t.head).2, (t.write (tm.tr q t.head).1.symbol).optionMove
        (tm.tr q t.head).1.movement⟩
Used by 2
Used byA machine that, on a blank cell, writes a blank and does not move is a linear bounded automaton · The fenced machine halts on some padding of a word iff the machine halts on it

TheoremA machine that produces an output halts#✓fully proved

If a single-tape Turing machine \(M\) outputs a word \(w'\) on an input word \(w\), then \(M\) halts on \(w\).

theorem Outputs.haltsOn {tm : SingleTapeTM Symbol} {l l' : List Symbol} (h : tm.Outputs l l') :
    tm.HaltsOn l
Uses 1
Statement usesHalting on an input

TheoremSingle-tape Turing machines are deterministic#✓fully proved

For a single-tape Turing machine \(M\), every configuration of \(M\) has at most one successor under the transition relation of \(M\).

theorem rightUnique_transitionRelation (tm : SingleTapeTM Symbol) :
    Relator.RightUnique tm.TransitionRelation
Used by 3
Used byHalting from a configuration is invariant along a run · Outputs are unique · Halting of a composite

TheoremHalting configurations are exactly those without a successor#✓fully proved

For a single-tape Turing machine \(M\) and a configuration \(c\) of \(M\), one step of \(M\) from \(c\) gives no configuration if and only if \(c\) is in the halting state.

theorem step_eq_none_iff {tm : SingleTapeTM Symbol} {c : tm.Cfg} :
    tm.step c = none ↔ c.state = none
Used by 2
Used byHalting from a configuration is normalizability · Configurations with the same successor halt together

TheoremHalting from a configuration is normalizability#✓fully proved

Let \(M\) be a single-tape Turing machine and \(c\) a configuration of \(M\). Then \(M\) halts from \(c\) if and only if \(c\) is normalizable for the transition relation of \(M\), that is, the run of \(M\) from \(c\) reaches, in finitely many steps (possibly none), a configuration that has no successor.

The configurations without a successor are exactly those in the halting state.

theorem haltsFrom_iff_normalizable {tm : SingleTapeTM Symbol} {c : tm.Cfg} :
    tm.HaltsFrom c ↔ Normalizable tm.TransitionRelation c
Uses 2
Statement usesHalting from a configuration
Proof usesHalting configurations are exactly those without a successor

TheoremHalting from a configuration is invariant along a run#✓fully proved

Let \(M\) be a single-tape Turing machine and let \(a\) and \(b\) be configurations of \(M\) such that the run of \(M\) from \(a\) reaches \(b\) in finitely many steps (possibly none). Then \(M\) halts from \(a\) if and only if \(M\) halts from \(b\).

The backward direction holds for any relation; the forward direction uses that \(M\) is deterministic.

theorem haltsFrom_iff_of_reflTransGen {tm : SingleTapeTM Symbol} {a b : tm.Cfg}
    (h : ReflTransGen tm.TransitionRelation a b) : tm.HaltsFrom a ↔ tm.HaltsFrom b
Uses 2 · Used by 2
Statement usesHalting from a configuration
Proof usesSingle-tape Turing machines are deterministic
Used byConfigurations with the same successor halt together · The fenced machine halts on some padding of a word iff the machine halts on it

TheoremConfigurations with the same successor halt together#✓fully proved

Let \(M\) be a single-tape Turing machine and let \(a\) and \(b\) be configurations of \(M\) that have the same successor, or that both have no successor. Then \(M\) halts from \(a\) if and only if \(M\) halts from \(b\).

theorem haltsFrom_iff_of_step_eq {tm : SingleTapeTM Symbol} {a b : tm.Cfg}
    (h : tm.step a = tm.step b) : tm.HaltsFrom a ↔ tm.HaltsFrom b
Uses 3 · Used by 1
Statement usesHalting from a configuration
Proof usesHalting from a configuration is invariant along a run · Halting configurations are exactly those without a successor
Used byThe fenced machine halts on some padding of a word iff the machine halts on it

TheoremDistinct words give distinct tapes#✓fully proved

The map sending a word \(w\) to the tape that holds \(w\) from the head position rightwards, every other cell blank, is injective.

theorem mk₁_injective : Function.Injective (BiTape.mk₁ : List Symbol → BiTape Symbol)
Used by 1
Used byOutputs are unique

TheoremOutputs are unique#✓fully proved

If a single-tape Turing machine \(M\) outputs the word \(l_1\) on the input \(l\) and also outputs the word \(l_2\) on the input \(l\), then \(l_1 = l_2\). Here \(M\) outputs a word \(w\) on \(l\) when its run from the initial configuration on \(l\) halts with exactly \(w\) on the tape, every other cell blank and the head on the first symbol of \(w\) (an all-blank tape if \(w\) is empty).

The run of a machine is determined by its input, and a halting configuration has no successor.

theorem Outputs.unique {tm : SingleTapeTM Symbol} {l l₁ l₂ : List Symbol} (h₁ : tm.Outputs l l₁)
    (h₂ : tm.Outputs l l₂) : l₁ = l₂
Uses 2
Proof usesDistinct words give distinct tapes · Single-tape Turing machines are deterministic

Decidability

DefinitionPredicates decidable by a single-tape Turing machine#✓fully proved

Let \(\alpha\) be a type with a primitive recursive encoding into \(\mathbb{N}\). A predicate \(p\) on \(\alpha\) is decidable by a single-tape machine when there are a finite, nonempty tape alphabet \(\Sigma\), an injective map \(\iota\) from the bits \(\{0, 1\}\) to \(\Sigma\) and a single-tape Turing machine \(M\) over \(\Sigma\) such that for every \(a \in \alpha\) there is a bit \(b\) for which \(M\) outputs the one-symbol word \(\iota(b)\) on the input word obtained by writing the binary encoding of the code of \(a\) in \(\mathbb{N}\) letter by letter through \(\iota\), and \(b = 1\) exactly when \(p(a)\) holds. Here \(M\) outputs a word \(w\) on an input when its run from the input halts with exactly \(w\) on the tape, every other cell blank and the head on the first symbol of \(w\).

def SingleTapeDecidable (p : α → Prop) : Prop :=
  ∃ (Symbol : Type) (_ : Inhabited Symbol) (_ : Fintype Symbol) (ι : Bool → Symbol),
    Function.Injective ι ∧ ∃ tm : SingleTapeTM Symbol, ∀ a, ∃ b : Bool,
      tm.Outputs ((encodeNat (encode a)).map ι) [ι b] ∧ (b = true ↔ p a)
Used by 12
Used byA single-tape machine decides the halting problem of a linear bounded automaton · A decidable predicate that no single-tape NTM recognizes · A predicate decided by a single-tape machine is computable · Single-tape decidable predicates are closed under complement · The halting problem for partial recursive codes is undecidable on single-tape machines · Computable predicates are decidable by single-tape machines · Single-tape decidable predicates are co-recognizable · Single-tape decidable predicates are exactly the computable predicates · Post's theorem · Single-tape and multi-stack machines decide the same predicates · Decidable predicates are recognizable by single-tape machines · A URM-decidable predicate is decidable by a single-tape Turing machine

DefinitionPredicates recognizable by a single-tape Turing machine#✓fully proved

Let \(\alpha\) be a type with a primitive recursive encoding into \(\mathbb{N}\). A predicate \(p\) on \(\alpha\) is recognizable by a single-tape machine when there are a finite, nonempty tape alphabet \(\Sigma\), an injective map \(\iota\) from the bits \(\{0, 1\}\) to \(\Sigma\) and a single-tape Turing machine \(M\) over \(\Sigma\) such that for every \(a \in \alpha\), the run of \(M\) on the input word obtained by writing the binary encoding of the code of \(a\) in \(\mathbb{N}\) letter by letter through \(\iota\) reaches the halting state if and only if \(p(a)\) holds.

def SingleTapeRecognizable (p : α → Prop) : Prop :=
  ∃ (Symbol : Type) (_ : Inhabited Symbol) (_ : Fintype Symbol) (ι : Bool → Symbol),
    Function.Injective ι ∧ ∃ tm : SingleTapeTM Symbol,
      ∀ a, tm.HaltsOn ((encodeNat (encode a)).map ι) ↔ p a
Uses 1 · Used by 15
Statement usesHalting on an input
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 · The halting problem for partial recursive codes is not co-recognizable on single-tape machines · R.e. predicates are recognizable by single-tape machines · A predicate recognized by a single-tape machine is r.e · Single-tape decidable predicates are co-recognizable · Post's theorem · Decidable predicates are recognizable by single-tape machines · The halting problem for partial recursive codes is recognizable on single-tape machines · Single-tape recognizable predicates are exactly the r.e. predicates · Single-tape and multi-stack machines recognize the same predicates · A URM-recognizable predicate is recognizable by a single-tape Turing machine · Co-recognizability by single-tape machines · Emptiness of a linear bounded automaton on computable input slices is undecidable

DefinitionCo-recognizability by single-tape machines#✓fully proved

Let \(\alpha\) be a primcodable type. A predicate \(p\) on \(\alpha\) is co-recognizable by a single-tape Turing machine when its complement \(\neg p\) is recognizable by a single-tape Turing machine.

def SingleTapeCoRecognizable (p : α → Prop) : Prop :=
  SingleTapeRecognizable fun a ↦ ¬p a
Uses 1 · Used by 5
Statement usesPredicates recognizable by a single-tape Turing machine
Used byThe halting problem for partial recursive codes is not co-recognizable on single-tape machines · Single-tape decidable predicates are co-recognizable · Single-tape co-recognizable predicates are those with an r.e. complement · Post's theorem · Decidable predicates are recognizable by single-tape machines

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.