🚀 go-pugleaf

(I didn't want to go to this much work, but no one else has pointed
this out, so here goes.)

There seems to be a misconception floating around: that the reason the
halting problem is unsolvable is because there are an infinite number
of possible states in a TM.  That is not the reason.  There are
theoretical machines that can solve the halting problem for a TM --
machines that can do an infinite amount of work in finite time.  The
_unsolvable_ halting problem is the problem of writing a TM that can
take the encoding of any other TM and tell whether that TM will halt.

The classic proof that this is unsolvable does not rely on the
infinite number of available states, it just generates a paradox based
on the assumption that the halting problem is solvable.  The same
paradox can be generated for _any_ class of machines meeting certain
very innocuous criteria.

Let C be any class of machines.  An input to C is a string over the
alphabet Sigma (that is, an element of Sigma*).  An encoding of
C-machines is a total one-to-one function E:C->Sigma from C-machines
to inputs.  If M is a C-machine and S is an input, then you can run C
on S: if the computation terminates then it ends in either an
accepting or a rejecting state.

If you have three C-machines M1, M2 and M3 you can form a compound
machine M1->M2;M3 with the behavior that if M1 terminates in an
accepting state then M2 is executed on the remainder of the input, and
if it terminates in a rejecting state then M3 is executed on the
remainder of the input.  If you have a C-machine M and an input S,
then M::S is the machine that always behaves exactly as M would behave
if run on S.  The machine CLoop is a C-machine that never halts,
CAccept is a C-machine that halts immediately and accepts.

Theorem: For any class of machines C over inputs Sigma* such that
    (1) there exists an encoding E from Sigma* to C,
    (2) M1->M2;M3 and M::S are defined,
and (3) CLoop and CAccept are defined,
it is impossible to construct a C-machine Halt that for all C-machines
M: (a) halts on E(M), (b) accepts E(M) if M terminates and (c) rejects
E(M) if M does not terminate.

Proof: Suppose that Halt exists.  Then define 
    Paradox = (Halt::E(Paradox)) -> CLoop ; CAccept
what is the result of running Paradox?

Computer programs certainly meet the 3 criteria in the theorem, so it
is not possible to write a computer program that solves the halting
problem for computer programs.

However, this is a theoretical result much like the theory that you
can't go faster than light.  The fact that there is a speed we can't
reach does not make it worthless to work on vehicles that go faster.
In the same way, just because it is impossible to solve the halting
problem with a program that always answers correctly, that does not
mean that we can't work on a program that always answers "yes", "no",
or "I can't tell".  And a lot can be done in that area.
--
					David Gudeman
gudeman@cs.arizona.edu
noao!arizona!gudeman