Section 9.4 Turing Machines
773
example 46
The decision problem for propositional wffs asks whether an algorithm exists to
decide whether any given propositional wff is a tautology. This is a solvable decision problem; the solution algorithm consists of constructing and examining the
truth table for the wff. The decision problem for predicate wffs asks whether an
algorithm exists to decide the validity of any given predicate wff. This is an undecidable problem; such an algorithm does not exist, which is exactly why we resorted to
the formal derivation rules of predicate logic to help establish validity for any given
wff. Because of the completeness and correctness of predicate logic, a wff is valid
if and only if we can produce a proof sequence for it. However, this has only shifted
one decision problem to an equivalent one—there is no algorithm to decide whether
a proof sequence exists for any given predicate wff, much less a mechanical way to
know what steps to use to produce a proof sequence if one does exist.
An alternative formulation to the logic systems we discussed in Chapter 1
is to identify certain strings of symbols as axioms and to give rules of inference
whereby a new string can be obtained from old strings. Any string that is the last
one in a finite list of strings consisting of either axioms or strings obtainable by
the rules of inference from earlier strings in the list is said to be a theorem. The
decision problem for such a formal theory is: Does an algorithm exist to decide
whether a given string in the formal theory is a theorem of the theory?
The work of Church and the famous twentieth-century logician Kurt Gödel
showed that any formal theory that axiomatizes properties of arithmetic (making
commutativity of addition an axiom, for example) and is not completely trivial (not
everything is a theorem) is undecidable. Their work can be considered good news
for working mathematicians because it means that ingenuity in answering questions
in number theory will never be replaced by a mechanical procedure.
example 47
A particular Turing machine T begun on a tape containing a string a will either
eventually halt or never halt. The halting problem for Turing machines is a decision problem: Does an algorithm exist to decide, given a Turing machine T and
string a, whether T begun on a tape containing a will eventually halt? Turing
proved the unsolvability of the halting problem in the late 1930s.
Halting Problem
We will prove the unsolvability of the halting problem after two observations.
First, it might occur to us that “run T on a” would constitute an algorithm to see
whether T halts on a. If within 25 steps of T’s computation T has halted, then
we know T halts on a. But if within 25,000 steps T has not halted, what can we
conclude? T may still eventually halt. How long should we wait? This so-called
algorithm will not always give us the answer to our question.
A second observation is that the halting problem asks for one algorithm to be
applied to a large class of statements. The halting problem asks, Does an algorithm
exist to decide, for any given (T, a) pair, whether T halts when begun on a tape
containing a? The algorithm comes first, and that single algorithm has to give the
correct answer for all (T, a) pairs. In the notation of predicate logic, the halting
problem asks about the truth value of a statement in the form
( E algorithm)(4(T, a))( … )
773
example 46
The decision problem for propositional wffs asks whether an algorithm exists to
decide whether any given propositional wff is a tautology. This is a solvable decision problem; the solution algorithm consists of constructing and examining the
truth table for the wff. The decision problem for predicate wffs asks whether an
algorithm exists to decide the validity of any given predicate wff. This is an undecidable problem; such an algorithm does not exist, which is exactly why we resorted to
the formal derivation rules of predicate logic to help establish validity for any given
wff. Because of the completeness and correctness of predicate logic, a wff is valid
if and only if we can produce a proof sequence for it. However, this has only shifted
one decision problem to an equivalent one—there is no algorithm to decide whether
a proof sequence exists for any given predicate wff, much less a mechanical way to
know what steps to use to produce a proof sequence if one does exist.
An alternative formulation to the logic systems we discussed in Chapter 1
is to identify certain strings of symbols as axioms and to give rules of inference
whereby a new string can be obtained from old strings. Any string that is the last
one in a finite list of strings consisting of either axioms or strings obtainable by
the rules of inference from earlier strings in the list is said to be a theorem. The
decision problem for such a formal theory is: Does an algorithm exist to decide
whether a given string in the formal theory is a theorem of the theory?
The work of Church and the famous twentieth-century logician Kurt Gödel
showed that any formal theory that axiomatizes properties of arithmetic (making
commutativity of addition an axiom, for example) and is not completely trivial (not
everything is a theorem) is undecidable. Their work can be considered good news
for working mathematicians because it means that ingenuity in answering questions
in number theory will never be replaced by a mechanical procedure.
example 47
A particular Turing machine T begun on a tape containing a string a will either
eventually halt or never halt. The halting problem for Turing machines is a decision problem: Does an algorithm exist to decide, given a Turing machine T and
string a, whether T begun on a tape containing a will eventually halt? Turing
proved the unsolvability of the halting problem in the late 1930s.
Halting Problem
We will prove the unsolvability of the halting problem after two observations.
First, it might occur to us that “run T on a” would constitute an algorithm to see
whether T halts on a. If within 25 steps of T’s computation T has halted, then
we know T halts on a. But if within 25,000 steps T has not halted, what can we
conclude? T may still eventually halt. How long should we wait? This so-called
algorithm will not always give us the answer to our question.
A second observation is that the halting problem asks for one algorithm to be
applied to a large class of statements. The halting problem asks, Does an algorithm
exist to decide, for any given (T, a) pair, whether T halts when begun on a tape
containing a? The algorithm comes first, and that single algorithm has to give the
correct answer for all (T, a) pairs. In the notation of predicate logic, the halting
problem asks about the truth value of a statement in the form
( E algorithm)(4(T, a))( … )