Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2005/calculus-linear-algebra-discrete-mathematics-logic-and-proof-and-models-of-computation/10/c/solution

The halting problem asks, given the encoding of a Turing machine and an input string, whether that machine eventually halts on that input. Its formal language is
Suppose a Turing machine decided this formal language. Construct another Turing machine that, on an input encoding , runs on . If answers that halts on its own encoding, enters an infinite loop. If answers that does not halt, halts. Handling malformed encodings by immediate rejection makes well-defined on arbitrary strings.
Now run on its own encoding. If says that halts, the construction makes loop; if says that does not halt, the construction makes halt. Either answer contradicts the assumed correctness of . Therefore
The contradiction concerns a decider that must give a correct terminating answer for every encoded machine and input. Simulating does detect a halt when one occurs, but cannot in general certify that a running computation will continue forever.

New to topics? Read the docs here!