Turing's Halting Problem - Proof

[lpetrich]

I finally was able to understand a proof of this theorem.
The Halting Problem - An Impossible Problem to Solve - YouTube
Turing & The Halting Problem - Computerphile - YouTube
Halting Problem -- Simple Proof
 Halting problem

Let us say that we have a function that can test whether or not some function will halt when it is given some input. In pseudocode form:

function halt(function f, input data i) -> boolean

Its action:

if evaluation of f(i) will halt
. return true
else // it will run forever
. return false
end if

In 1936, Alan Turing showed that that program is undecidable. He did that by constructing a program that includes the halting tester and constructs a negation of its results:

function turing(function f)
. if halt(f,f)
. . . while true
. . . . // infinite loop
. . . end while
. else
. . return // it halts
. end if
end function

Now try to run that function called on itself: turing(turing)

If it will halt, it will run forever, while if it will run forever, it will halt. A contradiction. Thus, the halting problem is undecidable.

 

[lpetrich]

This proof is much like the liar paradox. Consider a statement S: "This statement is false". If S is false, then it must be true, while if it is true, then it must be false.

-

Goedel's Incompleteness Theorems are related. They state that any formal system that includes the natural numbers will include at least one theorem that cannot be proved within the system. That theorem is

Theorem T: T is not a theorem.

If T is a theorem, then it is not, and if it is not, then it is. Much like

The natural numbers are there to provide the self-reference that this theorem needs.

-

There is a similar theorem within the "lambda calculus", essentially using only functions, named from writing lambda in these functions' definitions. It is that there is no function of two lambda-calculus expressions exists that can test whether or not those expressions are equivalent.

 

[lpetrich]

Some 2300 years ago, a certain Eukleides of Alexandria, a.k.a. Euclid, wrote a book on mathematics, Elements, a book that some people have described as the best-selling textbook of mathematics for all time. It features derivation of all of its math from a small number of axioms. Over the last few centuries, some mathematicians have found various problems with his axioms, but the basic idea remained.

In 1883, Giuseppe Peano improved on Euclid by presenting axioms of arithmetic, defining natural numbers with the notions of a successor number and a first number. One could then get integers, rational numbers, algebraic numbers, real numbers, and complex numbers from them by requiring closure under various operations:

• Natural numbers N: Peano's axioms
• Integers Z from N: closure under additive inversion (negative numbers)
• Rational numbers Q from Z: closure under multiplicative inversion (reciprocals)
• Algebraic numbers A from Q: algebraic closure (polynomial roots)
• Real numbers R from Q: Cauchy-sequence closure
• Complex numbers C from Q: both algebraic and Cauchy-sequence closure

In 1908, Ernst Zermelo went even further, proposing axioms of set theory, axioms that were improved in 1922 by Abraham Fraenkel.

How far could one go? In 1920, David Hilbert presented  Hilbert's program, which was to find:

[*]A formulation of all mathematics; in other words all mathematical statements should be written in a precise formal language, and manipulated according to well defined rules.
[*]Completeness: a proof that all true mathematical statements can be proved in the formalism.
[*]Consistency: a proof that no contradiction can be obtained in the formalism of mathematics. This consistency proof should preferably use only "finitistic" reasoning about finite mathematical objects.
[*]Conservation: a proof that any result about "real objects" obtained using reasoning about "ideal objects" (such as uncountable sets) can be proved without using ideal objects.
[*]Decidability: there should be an algorithm for deciding the truth or falsity of any mathematical statement.

Thus finishing what Euclid started.

But with their incompleteness theorems, Turing, Goedel, and Church proved that this process could never be complete.

 

[steve_bank]

I look at it as

start
print "executed"
stop

Can it be proven that the algorithm will stop? It is easy to see this example by inspection. How about a 100,000 line program?

 

[lpetrich]

I look at it as

start
print "executed"
stop

Can it be proven that the algorithm will stop? It is easy to see this example by inspection. How about a 100,000 line program?

Yes, that example is easy. It has a straight flow of control. It gets difficult when flow of control is not completely straight. A simple way of doing so is the "go to" statement:

if (condition) go to (location)

In its bare form, it is considered to be a risky construction, so in most high-level languages, it is hidden inside of other control-flow constructs. But I will leave it out in the open.

Halting is guaranteed if all the goto's are forward ones. This is the case for the goto's in if-then-else constructions. Switch-case constructions can easily be implemented using if-then-else ones.

Loops have backward goto's, though halting is guaranteed for loops that have some maximum number of repeats. Without such a maximum, one can get an infinite loop and thus run forever. Turing's proof involves being able to get into an infinite loop.

 

[steve_bank]

Compilers to a degree detect and flag infinite loops.

I look at it from this. You build an algorithm using logic. You build another algorithm to verify the first, but then how do you test the second algorithm? You end up with infinite regression.

When I worked on avionics Boeing would specify a set of logic equations that had to be implemented in software. Anything outside of that was a don't care. Software was verified by hardware inputs and outputs.

That is why software like Windows is only as reliable as the test cases it is run against.

 

[Kharakov]

A point at the origin, is at the angle pi in relation to the x axis. <-- liar's paradox. Does a null vector have direction?

Single closed loop looped quasi-vector that points at its origin, is at angle pi in relation to the x axis. <-- this is only true at certain point on the looped quasi-vector- not all tangent lines are angle pi to the x axis.

This has truth value at some point, and false value at others. Still, not a paradox. And not really a vector (unless one assumes an infinitesimal Kaluza Klein type of loop "vector" comprising of an infinite amount of infinitesimal vectors, only one of which points in the pi direction- which would mean the truth value is infinitesimal, not non-existent).


I basically see these true/false "paradoxes" as trying to measure the direction of a 0 length vector. What does (0,0) point towards? What is atan2(0,0)? (note: atan2 is arg is not atan(y/x), atan2 is a function that returns from 0 to 2pi, with inputs of x and y, not y/x).



This statement is pi true. So what. It has no magnitude- it doesn't reach outside of the origin, which is the statement, to point at something. It's literally atan2(0,0).

 

[steve_bank]

A point at the origin, is at the angle pi in relation to the x axis. <-- liar's paradox. Does a null vector have direction?

Single closed loop looped quasi-vector that points at its origin, is at angle pi in relation to the x axis. <-- this is only true at certain point on the looped quasi-vector- not all tangent lines are angle pi to the x axis.

This has truth value at some point, and false value at others. Still, not a paradox. And not really a vector (unless one assumes an infinitesimal Kaluza Klein type of loop "vector" comprising of an infinite amount of infinitesimal vectors, only one of which points in the pi direction- which would mean the truth value is infinitesimal, not non-existent).


I basically see these true/false "paradoxes" as trying to measure the direction of a 0 length vector. What does (0,0) point towards? What is atan2(0,0)? (note: atan2 is arg is not atan(y/x), atan2 is a function that returns from 0 to 2pi, with inputs of x and y, not y/x).



This statement is pi true. So what. It has no magnitude- it doesn't reach outside of the origin, which is the statement, to point at something. It's literally atan2(0,0).

Sounds like pie in the sky. The halting problem is about Turing Machines and algorithms.