
Theorem:
--------
The question whether a given Turing machine (or program) p will halt on input i
in finite time is undecidable. (This is known as the halting problem. The
following proof is due to Alan Mathison Turing.)

Proof (by contradiction):
-------------------------
Let's assume there exists a function "halt(program p, input i)" which expects
the digital presentation of a computer program and some input that is given to
that program as its arguments and returns (in finite time) "yes" if program p
halts on this input in finite time, "no" otherwise.

We can use this function in any program. Let program s be the following
program:

program s (program m, input n):
	if (halt(m, n) == "yes") {
		infinite_loop;
	} else {
		print "That program never halts."
	}

Programs s expects the digital representation of a computer program as its
argument and checks if *that* program will halt on the given input n by calling
said function "halt(program p, input i)".

Now since program s is a program like any other program that our computer can
execute, it surely has a digital representation itself. The question now is
what does

	halt(s, s)

return? (That's program s with the digital representation of itself as its
argument.)

We know that the function "halt" can only return either "yes" or "no".

Case 1)

If "halt(s, s)" returns "yes", it means that the call "halt(m, n)" in program s
(see above) also returned yes (because its arguments were also s and s). We
know that program s would then have branched into an infinite loop, so our
assumption that "yes" is returned must be wrong and "yes" can not be returned.

Case 2)

If "halt(s, s)" returns "no", it means that the call "halt(m, n)" in programs s
(see above) also returned "no". Since programs s then would simply print out
"That program never halts" and exit, the call to halt(s, s) can not possibly
return "no", because we know that program s halts nearly immediately.

Since either return value can not possibly have been returned if the function
"halt" works correctly, we conclude that our assumption must be wrong and such
a function can not exist.
