Halting problem and Rice's theorem

TheoremThe halting problem is undecidable by multi-stack machines#✓fully proved

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

theorem not_tm2Decidable_halting (n : ℕ) : ¬TM2Decidable fun c : Code ↦ (c.eval n).Dom

Uses 2 · Used by 4

Statement usesDecidability by multi-stack machines

Proof usesMulti-stack decidable predicates are exactly the computable predicates

Used bySome multi-stack machine has an undecidable halting set · Halting is undecidable · The halting problem for single-tape machines is undecidable · The halting problem for partial recursive codes is undecidable on single-tape machines

TheoremThe halting problem is recognizable by multi-stack 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 multi-stack machine.

theorem tm2Recognizable_halting (n : ℕ) : TM2Recognizable fun c : Code ↦ (c.eval n).Dom

Uses 2 · Used by 2

Statement usesRecognizability by multi-stack machines

Proof usesMulti-stack recognizable predicates are exactly the r.e. predicates

Used byThe complement of the halting set is not many-one reducible to it · The halting problem for partial recursive codes is recognizable on single-tape machines

TheoremThe halting problem is not co-recognizable by multi-stack machines#✓fully proved

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

theorem not_tm2CoRecognizable_halting (n : ℕ) :
    ¬TM2CoRecognizable fun c : Code ↦ (c.eval n).Dom

Uses 2 · Used by 9

Statement usesCo-recognizability by multi-stack machines

Proof usesMulti-stack co-recognizable predicates are exactly the co-r.e. predicates

Used byEquivalence is not co-recognizable · Finiteness is not co-recognizable · Finiteness is not recognizable · Rice–Shapiro, finite approximation · Rice–Shapiro, upward closure · Totality is not co-recognizable · Totality is not recognizable · The complement of the halting set is not many-one reducible to it · The halting problem for partial recursive codes is not co-recognizable on single-tape machines

TheoremSome multi-stack machine has an undecidable halting set#✓fully proved

There is a multi-stack machine \(M\), with a bijection between its input alphabet and the Booleans, such that no multi-stack machine decides, for \(n \in \mathbb{N}\), whether \(M\) halts when started on the binary representation of \(n\) (written in \(M\)'s input alphabet through the bijection).

The halting set of a code interpreter on input \(0\) is r.e., hence the halting set of a multi-stack machine, and deciding it would decide the halting problem.

theorem exists_not_tm2Decidable_tm2HaltsOn :
    ∃ (tm : FinTM2) (e : tm.Γ tm.k₀ ≃ Bool),
      ¬TM2Decidable fun n : ℕ ↦ TM2HaltsOn tm ((encodeNat n).map e.symm)

Uses 4

Statement usesDecidability by multi-stack machines · Halting of a multi-stack machine on an input

Proof usesThe halting problem is undecidable by multi-stack machines · Every r.e. predicate is the halting set of a multi-stack machine

TheoremRice's theorem for multi-stack machines#✓fully proved

Let \(C\) be a set of partial functions \(\mathbb{N} \to \mathbb{N}\). If a multi-stack machine decides, for each partial recursive code, whether the function the code computes lies in \(C\), then for all partial recursive functions \(f\) and \(g\), \(f \in C\) implies \(g \in C\).

theorem rice_tm2 (C : Set (ℕ →. ℕ)) (h : TM2Decidable fun c : Code ↦ c.eval ∈ C)
    {f g : ℕ →. ℕ} (hf : Nat.Partrec f) (hg : Nat.Partrec g) (hfC : f ∈ C) : g ∈ C

Uses 2 · Used by 2

Statement usesDecidability by multi-stack machines

Proof usesMulti-stack decidable predicates are exactly the computable predicates

Used byEmptiness is undecidable · Rice's theorem for partial recursive codes

TheoremMapping reductions are computed by multi-stack machines#✓fully proved

Let \(p\) and \(q\) be predicates on primitive recursively encodable types \(\alpha\) and \(\beta\), and write \(\langle x \rangle \in \mathbb{N}\) for the code of \(x\). Then \(p\) is many-one reducible to \(q\) if and only if there is a function \(f : \alpha \to \beta\) with \(p(a) \iff q(f(a))\) for all \(a \in \alpha\), together with a function \(F : \mathbb{N} \to \mathbb{N}\) that a multi-stack machine computes on binary representations and that satisfies \(F(\langle a \rangle) = \langle f(a) \rangle\) for all \(a \in \alpha\).

theorem manyOneReducible_iff_exists_tm2 {p : α → Prop} {q : β → Prop} :
    ManyOneReducible p q ↔ ∃ f : α → β, (∃ F : ℕ → ℕ,
      Nonempty (TM2Computable encodeNat encodeNat F) ∧ ∀ a, F (encode a) = encode (f a)) ∧
        ∀ a, p a ↔ q (f a)

Uses 2

Proof usesTuring-computable functions are recursive · Recursive functions are Turing-computable

TheoremDecidability transfers along mapping reductions#✓fully proved

Let \(p\) and \(q\) be predicates on primitive recursively encodable types \(\alpha\) and \(\beta\). If \(p\) is many-one reducible to \(q\) and \(q\) is decidable by a multi-stack machine, then \(p\) is decidable by a multi-stack machine.

theorem tm2Decidable_of_manyOneReducible {p : α → Prop} {q : β → Prop}
    (h : ManyOneReducible p q) (hq : TM2Decidable q) : TM2Decidable p

Uses 2 · Used by 16

Statement usesDecidability by multi-stack machines

Proof usesMulti-stack decidable predicates are exactly the computable predicates

Used byAcceptance is undecidable · Halting is undecidable · Regularity of halting sets is undecidable · The halting problem for single-tape machines is undecidable · Some finite Thue system has an undecidable word problem · MPCP is undecidable · The Post correspondence problem is undecidable · Reachability for string rewriting is undecidable · The uniform word problem for Thue systems is undecidable · The Post correspondence problem is undecidable over the binary alphabet · Regularity of context-free languages is undecidable · Whether a context-free grammar is ambiguous is undecidable · Equivalence of context-free grammars is undecidable · Inclusion of context-free languages is undecidable · Whether two context-free languages intersect is undecidable · Whether a context-free grammar generates every word is undecidable

TheoremRecognizability transfers along mapping reductions#✓fully proved

Let \(p\) and \(q\) be predicates on primitive recursively encodable types \(\alpha\) and \(\beta\). If \(p\) is many-one reducible to \(q\) and \(q\) is recognizable by a multi-stack machine, then \(p\) is recognizable by a multi-stack machine.

theorem tm2Recognizable_of_manyOneReducible {p : α → Prop} {q : β → Prop}
    (h : ManyOneReducible p q) (hq : TM2Recognizable q) : TM2Recognizable p

Uses 2 · Used by 13

Statement usesRecognizability by multi-stack machines

Proof usesMulti-stack recognizable predicates are exactly the r.e. predicates

Used byEquivalence is not co-recognizable · Equivalence is not recognizable · Finiteness is not co-recognizable · Finiteness is not recognizable · Effective Rice–Shapiro, necessity · Rice–Shapiro, finite approximation · Rice–Shapiro, upward closure · Totality is not co-recognizable · Totality is not recognizable · The complement of the halting set is not many-one reducible to it · Equivalence of context-free grammars is not recognizable · Inclusion of context-free languages is not recognizable · Universality of context-free grammars is not recognizable

TheoremRice's theorem for partial recursive codes#✓fully proved

Let \(C\) be a set of partial functions \(\mathbb{N} \rightharpoonup \mathbb{N}\), and suppose there are partial recursive functions \(f \in C\) and \(g \notin C\). Then the property of a partial recursive code \(c\) that the partial function computed by \(c\) belongs to \(C\) is not decidable by a multi-stack Turing machine.

theorem not_tm2Decidable_of_nontrivial (C : Set (ℕ →. ℕ)) {f g : ℕ →. ℕ} (hf : Nat.Partrec f)
    (hg : Nat.Partrec g) (hfC : f ∈ C) (hgC : g ∉ C) :
    ¬TM2Decidable fun c : Code ↦ c.eval ∈ C

Uses 2 · Used by 1

Statement usesDecidability by multi-stack machines

Proof usesRice's theorem for multi-stack machines

Used byRice's theorem for languages

TheoremRice's theorem for languages#✓fully proved

Let \(P\) be a set of subsets of \(\mathbb{N}\), and suppose there are partial recursive codes \(c_1\) and \(c_2\) such that the domain of \(c_1\) (the set of inputs on which it halts) belongs to \(P\) and the domain of \(c_2\) does not. Then the property of a partial recursive code \(c\) that the domain of \(c\) belongs to \(P\) is not decidable by a multi-stack Turing machine.

theorem not_tm2Decidable_language (P : Set (Set ℕ)) {c₁ c₂ : Code} (h₁ : c₁.eval.Dom ∈ P)
    (h₂ : c₂.eval.Dom ∉ P) : ¬TM2Decidable fun c : Code ↦ c.eval.Dom ∈ P

Uses 2

Statement usesDecidability by multi-stack machines

Proof usesRice's theorem for partial recursive codes

DefinitionAcceptance by a code#✓fully proved

A partial recursive code \(c\) accepts a natural number \(n\) when \(c\) halts on input \(n\) with output \(0\). Acceptance is a predicate on pairs \((c, n)\); it is the analogue of Sipser's \(A_{\mathrm{TM}}\), where a machine may halt without accepting.

def Accepts (p : Code × ℕ) : Prop := 0 ∈ p.1.eval p.2

Used by 3

Used byAcceptance reduces to halting · Halting reduces to acceptance · Acceptance is undecidable

DefinitionHalting of a code on an input#✓fully proved

A partial recursive code \(c\) halts on a natural number \(n\) when its evaluation at \(n\) is defined. Halting is a predicate on pairs \((c, n)\); it is the analogue of Sipser's \(\mathrm{HALT}_{\mathrm{TM}}\).

def Halts (p : Code × ℕ) : Prop := (p.1.eval p.2).Dom

Used by 6

Used byAcceptance reduces to halting · Halting reduces to acceptance · Halting reduces to regularity of halting sets · Acceptance is undecidable · Halting is undecidable · Regularity of halting sets is undecidable

TheoremA code that halts only on zero#✓fully proved

There is a partial recursive code \(z\) that on input \(0\) halts with output \(0\) and on every input \(x \ne 0\) does not halt.

theorem exists_code_zero_or_loop :
    ∃ z : Code, z.eval = fun x ↦ if x = 0 then Part.some 0 else Part.none

Used by 1

Used byAcceptance reduces to halting

TheoremAcceptance reduces to halting#✓fully proved

Say a partial recursive code \(c\) accepts a natural number \(n\) when \(c\) halts on input \(n\) with output \(0\). Acceptance many-one reduces to halting: there is a computable map \(f\) from pairs \((c, n)\) of a partial recursive code and a natural number to such pairs, such that for every pair \((c, n)\), the code \(c\) accepts \(n\) if and only if, writing \(f(c, n) = (c', n')\), the code \(c'\) halts on \(n'\).

The reduction runs the code, then loops unless the output is \(0\).

theorem manyOneReducible_accepts_halts : ManyOneReducible Accepts Halts

Uses 3

Statement usesAcceptance by a code · Halting of a code on an input

Proof usesA code that halts only on zero

TheoremHalting reduces to acceptance#✓fully proved

Say a partial recursive code \(c\) accepts a natural number \(n\) when \(c\) halts on input \(n\) with output \(0\). Halting many-one reduces to acceptance: there is a computable map \(f\) from pairs \((c, n)\) of a partial recursive code and a natural number to such pairs, such that for every pair \((c, n)\), the code \(c\) halts on \(n\) if and only if, writing \(f(c, n) = (c', n')\), the code \(c'\) accepts \(n'\).

The reduction runs the code, then outputs \(0\).

theorem manyOneReducible_halts_accepts : ManyOneReducible Halts Accepts

Uses 2 · Used by 1

Statement usesAcceptance by a code · Halting of a code on an input

Used byAcceptance is undecidable

TheoremHalting is undecidable#✓fully proved

No multi-stack Turing machine decides, for pairs \((c, n)\) of a partial recursive code and a natural number, whether \(c\) halts on \(n\).

theorem not_tm2Decidable_halts : ¬TM2Decidable Halts

Uses 4 · Used by 2

Statement usesHalting of a code on an input · Decidability by multi-stack machines

Proof usesThe halting problem is undecidable by multi-stack machines · Decidability transfers along mapping reductions

Used byAcceptance is undecidable · Regularity of halting sets is undecidable

TheoremAcceptance is undecidable#✓fully proved

No multi-stack Turing machine decides, for pairs \((c, n)\) of a partial recursive code and a natural number, whether \(c\) accepts \(n\), that is, halts on \(n\) with output \(0\).

This is Sipser's Theorem 4.11, with partial recursive codes in place of Turing machines.

theorem not_tm2Decidable_accepts : ¬TM2Decidable Accepts

Uses 6

Statement usesAcceptance by a code · Decidability by multi-stack machines

Proof usesHalting of a code on an input · Halting reduces to acceptance · Halting is undecidable · Decidability transfers along mapping reductions

DefinitionUnary language of a set of naturals#✓fully proved

For a set \(S \subseteq \mathbb{N}\), the unary language of \(S\) is the language over the one-letter alphabet \(\{\ast\}\) consisting of the words whose length lies in \(S\).

def unaryLang (S : Set ℕ) : Language Unit := {w | w.length ∈ S}

Used by 3

Used byHalting reduces to regularity of halting sets · The unary squares are not regular · Codes with a regular halting set

DefinitionCodes with a regular halting set#✓fully proved

A partial recursive code \(c\) has a regular halting set when the unary language of its domain (the set of inputs on which \(c\) halts), that is, the language of the words over a one-letter alphabet whose length lies in the domain of \(c\), is regular.

This is a domain analogue of Sipser's \(\mathrm{REGULAR}_{\mathrm{TM}}\), which asks about the accepted words instead.

def RegularDomainCode (c : Code) : Prop := (unaryLang c.eval.Dom).IsRegular

Uses 1 · Used by 2

Statement usesUnary language of a set of naturals

Used byHalting reduces to regularity of halting sets · Regularity of halting sets is undecidable

TheoremThe unary squares are not regular#✓fully proved

The unary language of the perfect squares, the set of words over a one-letter alphabet whose length is \(m^2\) for some \(m \in \mathbb{N}\), is not regular.

The proof uses the pumping lemma: if a DFA with \(N\) states accepted this language, pumping the word of length \(N^2\) by a block of length between \(1\) and \(N\) would give a length strictly between \(N^2\) and \((N + 1)^2\).

theorem not_isRegular_unaryLang_squares :
    ¬(unaryLang {n | ∃ m, n = m * m}).IsRegular

Uses 1 · Used by 1

Statement usesUnary language of a set of naturals

Used byHalting reduces to regularity of halting sets

DefinitionPartial function of the halting-to-regularity reduction#✓fully proved

For a partial recursive code \(c\) and natural numbers \(n\) and \(x\), the value at \(((c, n), x)\) is \(0\) if \(x\) is a perfect square; otherwise it is defined exactly when \(c\) halts on input \(n\), and then it is \(0\).

def regularRedFun (q : Code × ℕ) (x : ℕ) : Part ℕ :=
  if Nat.sqrt x * Nat.sqrt x = x then Part.some 0 else (q.1.eval q.2).map fun _ ↦ 0

Used by 2

Used byA single code for the regularity reduction function · Halting reduces to regularity of halting sets

TheoremA single code for the regularity reduction function#✓fully proved

For a pair \(q = (c, n)\) of a partial recursive code and a natural number, let \(g_q\) be the partial function on \(\mathbb{N}\) that on input \(x\) halts with output \(0\) if \(x\) is a perfect square, and otherwise runs \(c\) on \(n\) and, if that halts, outputs \(0\) (and is undefined if it does not). Write \(\ulcorner q \urcorner\) for the standard encoding of \(q\) as a natural number, and \(\langle a, b \rangle\) for the standard pairing of natural numbers \(a\) and \(b\). There is a partial recursive code \(U\) such that for every such pair \(q\) and every \(x \in \mathbb{N}\), the value of \(U\) at \(\langle \ulcorner q \urcorner, x \rangle\) equals \(g_q(x)\) as a partial value: one is defined exactly when the other is, and then they agree.

theorem exists_code_regularRedFun :
    ∃ U : Code, ∀ q x, U.eval (Nat.pair (encode q) x) = regularRedFun q x

Uses 1 · Used by 1

Statement usesPartial function of the halting-to-regularity reduction

Used byHalting reduces to regularity of halting sets

TheoremHalting reduces to regularity of halting sets#✓fully proved

There is a computable map \(f\) from pairs \((c, n)\) of a partial recursive code and a natural number to partial recursive codes such that for every pair \((c, n)\), the code \(c\) halts on \(n\) if and only if the halting set of \(f(c, n)\) (the set of inputs on which it halts), read as a unary language, is regular. That is, halting many-one reduces to regularity of halting sets.

The construction follows Sipser's proof of Theorem 5.3: \(f(c, n)\) halts on every perfect square, and on every input if \(c\) halts on \(n\).

theorem manyOneReducible_halts_regularDomain : ManyOneReducible Halts RegularDomainCode

Uses 6 · Used by 1

Statement usesHalting of a code on an input · Codes with a regular halting set

Proof usesA single code for the regularity reduction function · The unary squares are not regular · Partial function of the halting-to-regularity reduction · Unary language of a set of naturals

Used byRegularity of halting sets is undecidable

TheoremRegularity of halting sets is undecidable#✓fully proved

For a partial recursive code \(c\), let \(\operatorname{dom}(c) \subseteq \mathbb{N}\) be the set of inputs on which \(c\) halts. The property of \(c\) that the unary language \(\{w \in \{\ast\}^* : |w| \in \operatorname{dom}(c)\}\) is regular is not decidable by a multi-stack Turing machine.

theorem not_tm2Decidable_regularDomain : ¬TM2Decidable RegularDomainCode

Uses 6

Statement usesCodes with a regular halting set · Decidability by multi-stack machines

Proof usesHalting of a code on an input · Halting reduces to regularity of halting sets · Halting is undecidable · Decidability transfers along mapping reductions

24 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.