The halting problem is undecidable

Every word w describes a machine, Turing.MultiTapeTM.Universal.decodeDesc w, and the encoded description eDesc (desc eS eBit tm) of a machine tm with a binary alphabet and finitely many states describes tm itself. The halting problem asks, of a pair of words (w, x), whether the machine described by w halts on x, read as symbols under the coding Turing.MultiTapeTM.Universal.eBit (Turing.MultiTapeTM.haltingProblem); the acceptance problem asks whether it halts with output [true] (Turing.MultiTapeTM.acceptanceProblem). Their self-application forms ask the same of a word run on itself (Turing.MultiTapeTM.selfHaltingProblem, Turing.MultiTapeTM.selfAcceptanceProblem). None of the four is decidable Turing Sipser, Theorems 4.11 and 5.1.

All four results come from one diagonal argument, that of the time hierarchy theorem (Cslib.Complexity.not_forall_halted_diagonal, in Complexity.Computability.Complexity.Classes.Hierarchy) without the clock. A machine run on its own description can make its behavior depend on any computable verdict about that description (Turing.MultiTapeTM.exists_self_desc): Turing.MultiTapeTM.partialize turns a total machine computing the verdict, followed by a choice of a partial result for each verdict, into a machine that diverges or halts with the chosen output. So no computable verdict is true on the descriptions of all machines behaving in one way on their own descriptions and false on those of all machines behaving in another way (Turing.MultiTapeTM.not_separates_self_desc): some machine behaves, on its own description, in the way its verdict excludes. Halting separates divergence from halting with output [], and acceptance separates halting with output [false] from halting with output [true], so neither is decidable even on descriptions of machines (Turing.MultiTapeTM.halting_problem, Turing.MultiTapeTM.acceptance_problem and their self-application forms). The undecidability of the four sets of words follows (Turing.MultiTapeTM.not_isDecidable_of_separates_self_desc), the encoded-pair forms through the mapping reduction w ↦ (w, w).

Turing.MultiTapeTM.not_isDecidable_of_separates_self_desc is Rice's theorem for the behavior of machines on their own descriptions. The classical theorem Rice, about the behavior on all inputs, is Turing.MultiTapeTM.rice in Complexity.Computability.Machines.Turing.MultiTape.Halting.Rice; it needs in addition an s-m-n theorem for descriptions (Turing.MultiTapeTM.Universal.hardwire).

Mathlib proves corresponding theorems for its own model of computation, partial recursive codes. ComputablePred.halting_problem fixes the input: for each n, no computable predicate decides whether the code c halts on n. Its native counterpart, for each input of bits, is Turing.MultiTapeTM.not_isDecidable_halts, a corollary of Rice's theorem in Complexity.Computability.Machines.Turing.MultiTape.Halting.Rice; the halting problem here, Turing.MultiTapeTM.haltingProblem, takes the input as part of the instance instead. ComputablePred.rice and ComputablePred.rice₂ are Rice's theorem for codes. Transferring these results would need simulations in both directions between codes and the machines of this library, which are not developed here, so the native results are proved directly, on the universal simulation of Christian Reitwiessner (Turing.MultiTapeTM.Universal.simulate_desc) and the decoder of descriptions (Turing.MultiTapeTM.Universal.decodeDesc_eDesc).

Main definitions

• Turing.MultiTapeTM.haltingProblem, Turing.MultiTapeTM.selfHaltingProblem: halting.
• Turing.MultiTapeTM.acceptanceProblem, Turing.MultiTapeTM.selfAcceptanceProblem: acceptance.

Main results

• Turing.MultiTapeTM.IsComputable.exists_partialize: computable partial results are the behaviors of machines.
• Turing.MultiTapeTM.exists_self_desc, Turing.MultiTapeTM.not_separates_self_desc: self-reference by self-application, and the diagonal argument.
• Turing.MultiTapeTM.halting_problem, Turing.MultiTapeTM.halting_problem_self: no computable function decides halting on descriptions of machines.
• Turing.MultiTapeTM.acceptance_problem, Turing.MultiTapeTM.acceptance_problem_self: no computable function decides acceptance on descriptions of machines.
• Turing.MultiTapeTM.not_isDecidable_haltingProblem, Turing.MultiTapeTM.not_isDecidable_selfHaltingProblem, Turing.MultiTapeTM.not_isDecidable_acceptanceProblem, Turing.MultiTapeTM.not_isDecidable_selfAcceptanceProblem: the four problems are undecidable.
• Turing.MultiTapeTM.not_isDecidable_of_separates_self_desc: Rice's theorem for the behavior of machines on their own descriptions.

References

• A. M. Turing, On Computable Numbers, with an Application to the Entscheidungsproblem
• H. G. Rice, Classes of Recursively Enumerable Sets and Their Decision Problems
• M. Sipser, Introduction to the Theory of Computation

Machines from computable partial results

theorem Turing.MultiTapeTM.IsComputable.exists_partialize {α : Type u_1} {encIn : α ↪ List Bool} {f : α → Option (List Bool)} (hf : IsComputable f encIn encPartial) : ∃ (k : ℕ) (State : Type) (x : Fintype State) (tm : MultiTapeTM k Bool State), ∀ (a : α) (o : List Bool), tm.Computes (encIn a) o ↔ o ∈ f a

Computable partial results are the behaviors of machines: if f is computable with results encoded by encPartial, some machine with a binary alphabet and finitely many states halts on encIn a with output o exactly when f a = some o, and diverges when f a = none.

The diagonal argument

theorem Turing.MultiTapeTM.exists_self_desc {f : List Bool → Bool} (hf : IsComputable f encBits encBool) (r : Bool → Option (List Bool)) : ∃ (k : ℕ) (State : Type) (x : Fintype State) (eS : State ↪ ℕ) (tm : MultiTapeTM k Bool State), ∀ (o : List Bool), tm.Computes (Universal.eDesc (Universal.desc eS Universal.eBit tm)) o ↔ o ∈ r (f (Universal.eDesc (Universal.desc eS Universal.eBit tm)))

Self-reference by self-application. For every computable verdict f on words and every choice r of a partial result for each verdict, some machine with a binary alphabet and finitely many states, run on its own description w, has the partial result r (f w): it halts with output o exactly when r (f w) = some o, and diverges when r (f w) = none.

theorem Turing.MultiTapeTM.not_separates_self_desc {f : List Bool → Bool} (hf : IsComputable f encBits encBool) (r₀ r₁ : Option (List Bool)) (h₀ : ∀ ⦃k : ℕ⦄ ⦃State : Type⦄ [inst : Fintype State] (eS : State ↪ ℕ) (tm : MultiTapeTM k Bool State), (∀ (o : List Bool), tm.Computes (Universal.eDesc (Universal.desc eS Universal.eBit tm)) o ↔ o ∈ r₀) → f (Universal.eDesc (Universal.desc eS Universal.eBit tm)) = false) (h₁ : ∀ ⦃k : ℕ⦄ ⦃State : Type⦄ [inst : Fintype State] (eS : State ↪ ℕ) (tm : MultiTapeTM k Bool State), (∀ (o : List Bool), tm.Computes (Universal.eDesc (Universal.desc eS Universal.eBit tm)) o ↔ o ∈ r₁) → f (Universal.eDesc (Universal.desc eS Universal.eBit tm)) = true) : False

The diagonal argument. No computable verdict on words is false on the description of every machine whose behavior on its own description is r₀ and true on the description of every machine whose behavior on its own description is r₁: some machine behaves on its own description as r₀ when the verdict is true, and as r₁ when it is false. A behavior is a partial result: none for divergence, some o for halting with output o.

Halting and acceptance on descriptions of machines

theorem Turing.MultiTapeTM.halting_problem_self : ¬∃ (f : List Bool → Bool), IsComputable f encBits encBool ∧ ∀ ⦃k : ℕ⦄ ⦃State : Type⦄ [inst : Fintype State] (eS : State ↪ ℕ) (tm : MultiTapeTM k Bool State), f (Universal.eDesc (Universal.desc eS Universal.eBit tm)) = true ↔ tm.Halts (Universal.eDesc (Universal.desc eS Universal.eBit tm))

The halting problem, in self-application form. No computable function decides, on the description of every machine with a binary alphabet and finitely many states, whether the machine halts on its own description.

theorem Turing.MultiTapeTM.halting_problem : ¬∃ (f : List Bool × List Bool → Bool), IsComputable f (encPair encBits encBits) encBool ∧ ∀ ⦃k : ℕ⦄ ⦃State : Type⦄ [inst : Fintype State] (eS : State ↪ ℕ) (tm : MultiTapeTM k Bool State) (x : List Bool), f (Universal.eDesc (Universal.desc eS Universal.eBit tm), x) = true ↔ tm.Halts x

The halting problem. No computable function decides, on the description of every machine with a binary alphabet and finitely many states and every input, whether the machine halts on the input.

theorem Turing.MultiTapeTM.acceptance_problem_self : ¬∃ (f : List Bool → Bool), IsComputable f encBits encBool ∧ ∀ ⦃k : ℕ⦄ ⦃State : Type⦄ [inst : Fintype State] (eS : State ↪ ℕ) (tm : MultiTapeTM k Bool State), f (Universal.eDesc (Universal.desc eS Universal.eBit tm)) = true ↔ tm.Computes (Universal.eDesc (Universal.desc eS Universal.eBit tm)) [true]

The acceptance problem, in self-application form. No computable function decides, on the description of every machine with a binary alphabet and finitely many states, whether the machine halts with output [true] on its own description.

theorem Turing.MultiTapeTM.acceptance_problem : ¬∃ (f : List Bool × List Bool → Bool), IsComputable f (encPair encBits encBits) encBool ∧ ∀ ⦃k : ℕ⦄ ⦃State : Type⦄ [inst : Fintype State] (eS : State ↪ ℕ) (tm : MultiTapeTM k Bool State) (x : List Bool), f (Universal.eDesc (Universal.desc eS Universal.eBit tm), x) = true ↔ tm.Computes x [true]

The acceptance problem. No computable function decides, on the description of every machine with a binary alphabet and finitely many states and every input, whether the machine halts with output [true] on the input.

The halting and acceptance problems on words

def Turing.MultiTapeTM.haltingProblem : Set (List Bool × List Bool)

The halting problem: the pairs of words (w, x) such that the machine described by w halts on x.

def Turing.MultiTapeTM.selfHaltingProblem : Set (List Bool)

The words w such that the machine described by w halts on w.

def Turing.MultiTapeTM.acceptanceProblem : Set (List Bool × List Bool)

The acceptance problem: the pairs of words (w, x) such that the machine described by w halts on x with output [true].

def Turing.MultiTapeTM.selfAcceptanceProblem : Set (List Bool)

The words w such that the machine described by w halts on w with output [true].

theorem Turing.MultiTapeTM.mem_haltingProblem {p : List Bool × List Bool} : p ∈ haltingProblem ↔ (Universal.decodeDesc p.1).Halts (List.map (⇑Universal.eBit) p.2)

theorem Turing.MultiTapeTM.mem_selfHaltingProblem {w : List Bool} : w ∈ selfHaltingProblem ↔ (Universal.decodeDesc w).Halts (List.map (⇑Universal.eBit) w)

theorem Turing.MultiTapeTM.mem_acceptanceProblem {p : List Bool × List Bool} : p ∈ acceptanceProblem ↔ (Universal.decodeDesc p.1).Computes (List.map (⇑Universal.eBit) p.2) [Universal.eBit true]

theorem Turing.MultiTapeTM.mem_selfAcceptanceProblem {w : List Bool} : w ∈ selfAcceptanceProblem ↔ (Universal.decodeDesc w).Computes (List.map (⇑Universal.eBit) w) [Universal.eBit true]

theorem Turing.MultiTapeTM.desc_mem_haltingProblem_iff {k : ℕ} {State : Type} [Fintype State] (eS : State ↪ ℕ) (tm : MultiTapeTM k Bool State) (x : List Bool) : (Universal.eDesc (Universal.desc eS Universal.eBit tm), x) ∈ haltingProblem ↔ tm.Halts x

On the description of a machine, the halting problem asks whether the machine halts.

theorem Turing.MultiTapeTM.desc_mem_selfHaltingProblem_iff {k : ℕ} {State : Type} [Fintype State] (eS : State ↪ ℕ) (tm : MultiTapeTM k Bool State) : Universal.eDesc (Universal.desc eS Universal.eBit tm) ∈ selfHaltingProblem ↔ tm.Halts (Universal.eDesc (Universal.desc eS Universal.eBit tm))

On the description of a machine, the self-application form of the halting problem asks whether the machine halts on its own description.

theorem Turing.MultiTapeTM.desc_mem_acceptanceProblem_iff {k : ℕ} {State : Type} [Fintype State] (eS : State ↪ ℕ) (tm : MultiTapeTM k Bool State) (x : List Bool) : (Universal.eDesc (Universal.desc eS Universal.eBit tm), x) ∈ acceptanceProblem ↔ tm.Computes x [true]

On the description of a machine, the acceptance problem asks whether the machine halts with output [true].

theorem Turing.MultiTapeTM.desc_mem_selfAcceptanceProblem_iff {k : ℕ} {State : Type} [Fintype State] (eS : State ↪ ℕ) (tm : MultiTapeTM k Bool State) : Universal.eDesc (Universal.desc eS Universal.eBit tm) ∈ selfAcceptanceProblem ↔ tm.Computes (Universal.eDesc (Universal.desc eS Universal.eBit tm)) [true]

On the description of a machine, the self-application form of the acceptance problem asks whether the machine halts with output [true] on its own description.

theorem Turing.MultiTapeTM.not_isDecidable_of_separates_self_desc {P : Set (List Bool)} (r₀ r₁ : Option (List Bool)) (h₀ : ∀ ⦃k : ℕ⦄ ⦃State : Type⦄ [inst : Fintype State] (eS : State ↪ ℕ) (tm : MultiTapeTM k Bool State), (∀ (o : List Bool), tm.Computes (Universal.eDesc (Universal.desc eS Universal.eBit tm)) o ↔ o ∈ r₀) → Universal.eDesc (Universal.desc eS Universal.eBit tm) ∉ P) (h₁ : ∀ ⦃k : ℕ⦄ ⦃State : Type⦄ [inst : Fintype State] (eS : State ↪ ℕ) (tm : MultiTapeTM k Bool State), (∀ (o : List Bool), tm.Computes (Universal.eDesc (Universal.desc eS Universal.eBit tm)) o ↔ o ∈ r₁) → Universal.eDesc (Universal.desc eS Universal.eBit tm) ∈ P) : ¬IsDecidable P encBits

Rice's theorem for the behavior on self-descriptions. A set of words containing the description of every machine whose behavior on its own description is r₁, and the description of no machine whose behavior on its own description is r₀, is undecidable.

theorem Turing.MultiTapeTM.not_isDecidable_selfHaltingProblem : ¬IsDecidable selfHaltingProblem encBits

The halting problem is undecidable, in self-application form.

theorem Turing.MultiTapeTM.selfHaltingProblem_mappingReducible : MappingReducible encBits (encPair encBits encBits) selfHaltingProblem haltingProblem

Running a word on itself is a mapping reduction of the self-application form of halting to halting.

theorem Turing.MultiTapeTM.not_isDecidable_haltingProblem : ¬IsDecidable haltingProblem (encPair encBits encBits)

The halting problem is undecidable.

theorem Turing.MultiTapeTM.not_isDecidable_selfAcceptanceProblem : ¬IsDecidable selfAcceptanceProblem encBits

The acceptance problem is undecidable, in self-application form.

theorem Turing.MultiTapeTM.selfAcceptanceProblem_mappingReducible : MappingReducible encBits (encPair encBits encBits) selfAcceptanceProblem acceptanceProblem

Running a word on itself is a mapping reduction of the self-application form of acceptance to acceptance.

theorem Turing.MultiTapeTM.not_isDecidable_acceptanceProblem : ¬IsDecidable acceptanceProblem (encPair encBits encBits)

The acceptance problem is undecidable.