Halting problem for single-tape Turing machines

DefinitionHalting of a single-tape machine#✓fully proved

A single-tape Turing machine \(M\) halts on an input word \(l\) when its run, started in its start state with \(l\) on the tape, reaches a halting configuration.

def TM0HaltsOn {Γ Λ : Type*} [Inhabited Γ] [Inhabited Λ] (M : TM0.Machine Γ Λ) (l : List Γ) :
    Prop :=
  (TM0.eval M l).Dom

Used by 9

Used byThe halting problem for single-tape machines is undecidable · Some finite Thue system has an undecidable word problem · Reachability for string rewriting is undecidable · Invariant of the rewriting simulation of a single-tape machine · Single-tape halting many-one reduces to the word problem of a fixed Thue system · Single-tape halting many-one reduces to string rewriting reachability · Every rewrite preserves the invariant of reachable words · A single-tape machine halts iff its start word rewrites to the halting word · A single-tape machine halts iff its start word is Thue equivalent to the halting word

TheoremHalting agrees with evaluation for multi-stack machines#✓fully proved

A multi-stack machine halts on a word \(l\) over the alphabet of its input stack if and only if the evaluation of its transition function, started at its main label and initial internal state with \(l\) on the input stack and all other stacks empty, is defined.

theorem tm2HaltsOn_iff_eval_dom (tm : FinTM2) (l : List (tm.Γ tm.k₀)) :
    TM2HaltsOn tm l ↔ (TM2.eval tm.m tm.k₀ l).Dom

Uses 2 · Used by 2

Statement usesHalting of a multi-stack machine on an input

Proof usesThe initial configuration of a bundled multi-stack machine

Used byThe halting problem for single-tape machines is undecidable · The recognizer halts iff the multi-stack machine does

DefinitionPrimitive recursive coding of a finite type#✓fully proved

A finite type \(\alpha\) with \(n\) elements gets the primitive recursive coding transported from \(\{0, \dots, n - 1\}\) along a fixed (noncanonically chosen) bijection between \(\alpha\) and \(\{0, \dots, n - 1\}\).

@[instance_reducible]
noncomputable def primcodableOfFintype (α : Type*) [Fintype α] : Primcodable α :=
  Primcodable.ofEquiv (Fin (Fintype.card α)) (Fintype.equivFin α)

Used by 3

Used byThe halting problem for single-tape machines is undecidable · Some finite Thue system has an undecidable word problem · Reachability for string rewriting is undecidable

TheoremThe input encoding of the single-tape emulation is primitive recursive#✓fully proved

Let \(M\) be a multi-stack machine together with a bijection \(e\) from the alphabet of its input stack to the Booleans, and suppose the tape alphabet \(\Gamma'\) of the single-tape emulation of \(M\) is finite and carries a primitive recursive coding. Then the map sending \(n \in \mathbb{N}\) to the initial tape of the emulation on the input word \(e^{-1}(b_1) \cdots e^{-1}(b_m)\), where \(b_1 \cdots b_m\) is the binary code of \(n\), is primitive recursive.

theorem primrec_trInit_encodeNat (tm : FinTM2) [Primcodable (TM2to1.Γ' tm.K tm.Γ)]
    [Finite (TM2to1.Γ' tm.K tm.Γ)] (e : tm.Γ tm.k₀ ≃ Bool) :
    Primrec fun n ↦ TM2to1.trInit tm.k₀ ((encodeNat n).map e.symm)

Uses 1 · Used by 1

Proof usesBinary encoding, least significant bit first

Used byThe halting problem for single-tape machines is undecidable

TheoremThe halting problem for single-tape machines is undecidable#✓fully proved

There are a finite tape alphabet \(\Gamma\) with a blank symbol, decidable equality and a primitive recursive coding, a type of states \(\Lambda\) with a start state, a single-tape Turing machine \(M\) with alphabet \(\Gamma\) and states \(\Lambda\), and a finite set \(S\) of states that contains the start state and is closed under the transitions of \(M\), such that the set of input words on which \(M\) halts is not decidable by a multi-stack machine.

theorem exists_not_tm2Decidable_tm0HaltsOn :
    ∃ (Γ Λ : Type) (_ : Inhabited Γ) (_ : Inhabited Λ) (_ : Fintype Γ) (_ : DecidableEq Γ)
      (_ : Primcodable Γ) (M : TM0.Machine Γ Λ) (S : Finset Λ),
      TM0.Supports M ↑S ∧ ¬TM2Decidable (TM0HaltsOn M)

Uses 13 · Used by 2

Statement usesHalting of a single-tape machine · Decidability by multi-stack machines

Proof usesThe halting problem is undecidable by multi-stack machines · Primitive recursive coding of a finite type · The input encoding of the single-tape emulation is primitive recursive · Decidability transfers along mapping reductions · Halting agrees with evaluation for multi-stack machines · Halting of a multi-stack machine on an input · Every r.e. predicate is the halting set of a machine with finite alphabets · 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 bySome finite Thue system has an undecidable word problem · Reachability for string rewriting is undecidable

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.