Halting Problem

The halting problem is a decision problem that asks if it is possible to know in advance if a given Turing machine eventually halts. The implications of the Halting Problem applies to automatic program verification, since most programs can be reduced to the Halting Problem.

Historical Context §

The Entscheidungsproblem (German for decision problem), also known as the Halting Problem is a challenge posed by mathematician David Hilbert. The problem requires an algorithm that, given all the axioms of math, can determine whether a mathematical statement can be proven.

This problem was given a negative answer (a proof that it is impossible/undecidable) by Alan Turing by using Turing machines. Since the Halting problem asks for a finite procedure, the solving algorithm (if it exists) would fall under the definition of a effectively calculable procedure, and by the Church-Turing thesis, can be run on a Turing Machine.

Problem Description §

Original §

Given a an arbitrary proof system $\psi$, is it possible to prove a statement $S$ in $\psi$?

Turing’s Equivalent Restatement §

Given a Turing Machine $T$, can we determine if $T$ halts on a string $w$, or runs forever?

Decidability §

The Halting Problem is undecidable ^theorem

$${\text{HALT}}_{TM}=\{⟨T,w⟩|\text{T halts on w}\}\text{ is undecidable}$$

Proof (By Reduction)

This proof by reduction is straightforward, but depends on other theorems:

• The TM acceptance problem reduces to the Halting problem
• The TM acceptance problem is undecidable
• Hence, the Hating problem is also undecidable

Also, if ${\text{HALT}}_{TM}$ was decidable, it would mean:

$$\text{L is recognisable}⟹\text{L is decidable}$$

Applications §

• static code analysis: Determining if any program would get trapped in a infinite loop for any input!
  • https://en.wikipedia.org/wiki/Rice%27s_theorem

Resources §

• Tom Scott’s Summary