The Halting Problem is _not_ solvable on real com 
Author Message
 The Halting Problem is _not_ solvable on real com

(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

noao!arizona!gudeman



Mon, 25 Oct 1993 14:53:29 GMT  
 The Halting Problem is _not_ solvable on real com
This is an interesting discussion, and I have learned a lot from it.
There are quite a few subtle points that I had not realized before.

Quote:

>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.

....[ stuff deleted ] .....

Quote:
>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.

The problem here is that if you are dealing with a specific machine,
with one particular piece of hardware, then the description of M1 may
fill up the machine, and likewise with M2 and M3. In that case you may
very well have no room to store the description of M1->M2;M3. I think
this is Victor Yodaiken's point, or at least one of them. It's no use
saying you will put the description on tape because that can get too
large as well. If the number of tapes is larger than the memory of the
computer you will almost certainly be in trouble.

The discussion is quite difficult, because on the one hand we are
working with abstract constructs and mathematical proofs, and on the
other hand with practical computers. To relate the two, we make a
mathematical model of the computer. But mathematical models are never
fully accurate descriptions. For example, I never have to call out an
engineer to fix my finite state automaton :-). And I don't have to
worry about the effect of gamma rays on it, nor about how the end of
the universe may affect it. We have therefore to choose, from among
various possible mathematical models, not the model which *IS* the
computer, but the model which most faithfully follows the particular
behaviour we are trying to investigate. This is a matter of judgement, not
of irrefutable logic, and is
likely to depend on which kind of behaviour of the practical computer one is
interested in. If you are interested in error correction in hardware,
your mathematical model is not going to be a finite state automaton,
because that never makes errors.

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

Is this a misprint, David? You can't define Paradox in terms of
itself. If it is a misprint, can you please repost, as I would like to
study this.

                        David Epstein.



Mon, 25 Oct 1993 20:25:26 GMT  
 The Halting Problem is _not_ solvable on real com

Quote:

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

>Is this a misprint, David? You can't define Paradox in terms of
>itself. If it is a misprint, can you please repost, as I would like to
>study this.

Paradox is not really defined in terms of itself in a recursive-call sense.
E(Paradox) is the "source code" for the program Paradox. If you know how
Halt, CLoop, and CAccept are written, then you know how Paradox is
written (see the >> lines :-).  Feed the Paradox program to Halt, and
if Halt says it halts then loop, otherwise halt. Paradox never explicity
calls itself (altho Halt might "call" Paradox in some way, in which case
Halt doesn't halt and thus gives a "wrong" answer).

--
--- Darren New --- Grad Student --- CIS --- Univ. of Delaware ---
----- Network Protocols, Graphics, Programming Languages, FDTs -----
+=+ Nails work better than screws, when both are driven with hammers +=+



Tue, 26 Oct 1993 02:53:14 GMT  
 The Halting Problem is _not_ solvable on real com

]
]>Proof: Suppose that Halt exists.  Then define
]>    Paradox = (Halt::E(Paradox)) -> CLoop ; CAccept
]>what is the result of running Paradox?
]
]Is this a misprint, David? You can't define Paradox in terms of
]itself.

It was sort of a misprint, I guess I should have asked about the
behavior of Halt::E(Paradox).  But the definition of Paradox is OK.
E(Paradox) is a representation of Paradox in the input language so I'm
defining Paradox in terms of a representation of itself.  This is
certainly possible on a real computer, since you can have the program
Paradox open the file that contains its own source code and read it.

Incidentally, I'm not happy with the conditions I stated for the
theorem since some of them should be assumptions about all classes of
automata.  The existence of an encoding E seems to apply for any
alphabet with two or more characters as long as C is a countable set.
It seems that the existence of 'CAccept' and 'M1->M2;M3' are immediate
consequences of the definition of an automaton (I obviously didn't
give a full definition), and I'm also inclined to believe that 'M::S'
is a consequence of the definition an automaton.
--
                                        David Gudeman

noao!arizona!gudeman



Tue, 26 Oct 1993 03:32:38 GMT  
 The Halting Problem is _not_ solvable on real com

Quote:


>N. Walker) writes:
>>Suppose you write a [purported] halting problem solver.  I'll
>>assume it's in C, so you have a program source called, say, "fred.c",
>>which compiles into a binary program "fred", running under Unix.  The
>>idea is that you call
>>        $ fred jim.c
>Suppose jim.c halts when given certain inputs and does not halt when
>given certain other inputs.  The halting problem in this case has not
>been correctly defined, since the command line "fred jim.c" does not
>specify the inputs given to jim.c.  We we really ought to be saying
>     % fred jim.c fred.c
>where jim.c is the program whose halting characteristics are being
>tested, and fred.c is the input that jim.c will be assumed to read when
>it executes.

And therein lies the madness:
The next step is:

    % fred jim.c fred.c jim.c

Then:

    % fred jim.c fred.c jim.c fred.c

Then:

    % fred jim.c fred.c jim.c fred.c jim.c ...

And so on.  Thus, the "run it, and see if it halts" suggestion falls flat on
its face.  There is at least one problem which would take an infinite amount of
time and resources to set up, much less attempt to run.
--
T.T.F.N.,

'And Ritchie said, "Let there be portability!"  And nothing happened, so
 Ritchie realized that he had his work cut out for him.'



Wed, 27 Oct 1993 06:58:23 GMT  
 The Halting Problem is _not_ solvable on real com

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

        I was intending to, but news takes *ages* to get here, so I was
too late ....

        Anyway, I think I still have something to say.  As David says,
the halting problem really isn't a problem of large machines.  I like to
think in more concrete terms than these abstract machines with inputs over
Sigma and so on, so here is the same argument more concretely.

        Suppose you write a [purported] halting problem solver.  I'll
assume it's in C, so you have a program source called, say, "fred.c",
which compiles into a binary program "fred", running under Unix.  The
idea is that you call

        $ fred jim.c

and the computer clunks away for a while, and then prints out "Halts"
if "jim.c" describes a program that eventually halts, and prints out
"Loops" if the program would run for ever.  Let us assume that the
structure of "fred.c" is such that it computes away for a while, but
eventually must run through a final chunk of code that looks like:

        if (halt)
                printf ("Halts\n");
        else
                printf ("Loops\n");
        exit (0);

I now subvert "fred" by writing a new program whose source is "bert.c",
identical with "fred.c" except that the above chunk is replaced by

        if (halt)
                while (1);      /* ie, loop forever */
        else
                exit (0);

Now, whenever "fred" would print "Halts", "bert" will loop forever,
and whenever it prints "Loops", "bert" stops.

        What does "bert bert.c" do?  It stops if "fred bert.c" would print
"Loops", and goes on forever if "fred bert.c" would print "Halts".  So,
"fred bert.c" cannot tell the truth.  There are three ways out of this:

        (a) "fred" can lie [but then it's not much use];
        (b) "fred" can go on for ever without printing anything [that's
                not much use either!];
        (c) "fred" can admit, after a while, that it cannot tell, and give up.

Note, however, that, in any sensible implementation, "bert" is, if anything,
rather simpler than "fred".  The conclusion is that the best we can hope for
from a "halting problem program" is for it to be able to analyse simple
programs, but that anything complicated will be beyond it.  In particular,
it cannot be powerful enough to introspect itself.  [Finding and curing
the bugs in the above argument is left as an exercise for the reader.]

        As David says, there is nothing particularly "large" in this
sort of argument.  The best source I know for all this material is
*still* Minsky's "Computation:  Finite and Infinite Machines", which
is now terribly out of date, but is brilliantly written.  A new edition
would be a delight.

--
Andy Walker, Maths Dept., Nott'm Univ., UK.



Tue, 26 Oct 1993 23:54:54 GMT  
 The Halting Problem is _not_ solvable on real com

Quote:
N. Walker) writes:
>Suppose you write a [purported] halting problem solver.  I'll
>assume it's in C, so you have a program source called, say, "fred.c",
>which compiles into a binary program "fred", running under Unix.  The
>idea is that you call
>    $ fred jim.c

Suppose jim.c halts when given certain inputs and does not halt when
given certain other inputs.  The halting problem in this case has not
been correctly defined, since the command line "fred jim.c" does not
specify the inputs given to jim.c.  We we really ought to be saying

     % fred jim.c fred.c

where jim.c is the program whose halting characteristics are being
tested, and fred.c is the input that jim.c will be assumed to read when
it executes.
--

UUCP:  oliveb!cirrusl!dhesi



Wed, 27 Oct 1993 03:18:48 GMT  
 The Halting Problem is _not_ solvable on real com
Kenneth Walker:
   Is there any hope (in a theoretical sense) of a finite state
   machine computing interesting properties of an arbitrary finite
   state machine of its own size?

I don't think this is an interesting question.  :-)

An interesting question would be:  what properties should a
computation device have such that most practical programs can be
determined to halt.

This is related to proving a program correct.

I should note that functional languages seem to be rather promising
in this regard.

Raul Rockwell



Wed, 27 Oct 1993 09:52:04 GMT  
 The Halting Problem is _not_ solvable on real com

For the moment, lets assume our analysis routine manages to place a bound
on the number of states (size of memory) that will exist in the compiled
program and that the analysis program must itself execute within the same
finite-state machine. Because the analysis routine must itself be coded
in some of the states, it does not have enough states to represent the
states of the program it is analysing. Is there any hope (in a theoretical
sense) of a finite state machine computing interesting properties of
an arbitrary finite state machine of its own size?

  Ken Walker / Computer Science Dept / Univ of Arizona / Tucson, AZ 85721



Wed, 27 Oct 1993 06:56:01 GMT  
 The Halting Problem is _not_ solvable on real com

Quote:
(David A. Truesdell) writes:

>>Suppose jim.c halts when given certain inputs and does not halt when
>>given certain other inputs.  The halting problem in this case has not
>>been correctly defined, since the command line "fred jim.c" does not
>>specify the inputs given to jim.c.

        Quite right, but the distinction is uninteresting, because all
interesting [:-)] variants of the halting problem are equally insoluble.
E.g., it is generally undecidable whether "jim.c" halts when given *no*
input, when given *specified* input, when given *some* input or when
given *any* input.  In my original submission, I carefully left all this
to the reader!

Quote:
>>                                      We we really ought to be saying
>>     % fred jim.c fred.c

>And therein lies the madness:
>The next step is:

>    % fred jim.c fred.c jim.c

>Then:

>    % fred jim.c fred.c jim.c fred.c

>Then:

        Then you define "fred" to [attempt to] determine whether its
parameter halts or loops *when given itself* as input, and the paradox
comes back and bites you again without Rahul's objection.  See Minsky,
op previously cit, for a full discussion.

--
Andy Walker, Maths Dept., Nott'm Univ., UK.



Sat, 30 Oct 1993 01:19:51 GMT  
 The Halting Problem is _not_ solvable on real com

Quote:

>For the moment, lets assume our analysis routine manages to place a bound
>on the number of states (size of memory) that will exist in the compiled
>program and that the analysis program must itself execute within the same
>finite-state machine. Because the analysis routine must itself be coded
>in some of the states, it does not have enough states to represent the
>states of the program it is analysing. Is there any hope (in a theoretical
>sense) of a finite state machine computing interesting properties of
>an arbitrary finite state machine of its own size?

No. But, a finite machine of size X can solve the halting problem for
finite machines of size Y, supposing that Y is sufficiently smaller than X.
In practical terms, this means a cross-compiler on a CRAY might be able
to detect failure to halt in programs being compiled for a small micro.
But, the exact ratio between X and Y depends on your ingenuity,the
programming language, and  the class of programs you find interesting.


Sat, 30 Oct 1993 22:17:30 GMT  
 The Halting Problem is _not_ solvable on real com

Here's the latest version of the FTP List--an extract from The Language List
giving all of the ftp-able languages that I have located to date.  It's more
than doubled from the last posting a month ago.

Further additions and corrections welcome!

*LISP - think.com:/public/starsim-f18-sharfile, a *LISP simulator

ABC - hp4nl.nluug.nl, Unix source, MSDOS and Mac executables

ADVSYS - uunet.uu.net:comp.sources.games/Volume2

ALLOY - cs.nyu.edu:pub/local/alloy.

Anna - anna.stanford.edu

CAML - nuri.inria.fr

CLOS - arisia.xerox.com:pcl

CLU - pion.lcs.mit.edu, for Sun, VAX

ELP - gargoyle.uchicago.edu, for Sun and DEC

FORM - acm.princeton.edu, nikhefh.nikhef.nl

FP - apple.com:ArchiveVol1/unix_lang

fpc - comp.sources.unix/Volume20

FX-87 - brokaw.lcs.mit.edu

GAP - math.ucla.edu, for Sun

Yale Haskell - nebula.systemsz.cs.yale.edu
Glasgow Haskell - piggy.cs.chalmers.se

Hermes - software.watson.ibm.com

Hope - brolga.cc.uq.oz.au, PC Hope and a lazy variant for Unix, Mac

Icon - arizona.edu

IFP - cs.uiuc.edu and comp.sources.unix/volume10

INTERCAL - snow.white.toronto.edu, also comp.sources.misc/Volume16

ISETL - sun.soe.clarkson.edu, for MSDOS, Mac, Unix, VAX/VMS, and source

J - watserv1.waterloo.edu

Janus - cs.arizona.edu

KCL - rascal.ics.utexas.edu

Little Smalltalk - cs.orst.edu

LML - piggy.cs.chalmers.se

Macaulay - zariski.harvard.edu, Version 3 for Sun, Mac Amiga, source in C

MAS - alice.fmi.uni-passau.de, for PC, Atari, Amiga

Mathematica - otter.stanford.edu, ftp.ncsa.uiuc.edu

Mma - ucbarpa.berkeley.edu

Modula-3 - gatekeeper.dec.com

Oberon - neptune.inf.ethz.ch, for Mac, SPARC, DECstation

occam - watserv1.waterloo.edu, simulator for VAX, Tahoe

PARI - math.ucla.edu

Perl - jpl-devvax.jpl.nasa.gov, for Unix, MS-DOS, Amiga

Python - wuarchive.wustl.edu, gatekeeper.dec.com and hp4nl.nluug.nl

rc - archone.tamu.edu

Russell - watserv1.waterloo.edu

Self - otis.stanford.edu

SETL2 - cs.nyu.edu, for MSDOS, OS/2, Mac, Unix Workstations

SIMULA67 - rascal.ics.utexas.edu, for Mac

Small-C - apple.com:ArchiveVol1/unix_lang

SML - cs.yale.edu
    - sbcs.sunysb.edu, lazy variant

SNOBOL4 - apple.com:ArchiveVol1/unix_lang

SR - cs.arizona.edu, watserv1.waterloo.edu

Tcl - ucbvax.berkeley.edu

TECO - usc.edu, for VAX/VMS, Unix, MSDOS, Mac, Amiga

TeX-82 - june.cs.washington.edu

TXL - qusuna.qucis.queensu.ca, for Sun, source in Turing Plus

XLISP - gatekeeper.dec.com and comp.sources.misc/Vol10

--
--Bill Kinnersley

226 Transfer complete.



Mon, 01 Nov 1993 00:34:12 GMT  
 The Halting Problem is _not_ solvable on real com
An earlier poster said that thinking of computers as analog devices is not
a very useful view of computation.  This is true.  The problem is that the
operation of a real computer is not the same as our abstract notion of
computation.  When considering real machines at lower and lower levels of
abstraction eventually statistics enters in and we lose determinacy.

In arguing that an FSM is a more appropriate abstraction than a TM for
modelling execution of a program on a real computer, three points come
to mind:

1) Undoubtedly sometimes an FSM is more appropriate, but

2) The FSM view ties us to a particular machine.  I don't think this is a
   very useful view of computation. :-)  Generally we want our  programs
   to behave similarly on different machines.  I want to say "This program
   will terminate with result foo or with an error condition if not enough
   memory is available."  I don't want to say "This program will terminate
   with result foo if run on a small enough machine but I don't know what
   it will do otherwise."

3) When considering termination, an FSM has only two posssible behaviors
   on any given input:  termination or infinite loop.  A TM can terminate or
   it can fail to terminate either by entering an infinite loop or by simply
   running forever never repeating any earlier state.  Since most programming
   languages do not specify that they must be run on a finite machine we can
   consider these programs as FSMs on a finite machine or as TMs on an
   infinite machine.  Now, the 64K question is:

* What useful programs terminate as FSMs and fail to terminate as TMs?

   The most obvious example is a memory testing program, but I think that
   nearly all programs that terminate only on FSMs are bugged or useless.
   It would be very interesting, however, to have you folks think up a
   bunch of useful programs to prove me wrong.  In general it seems to me
   that having to resort to finiteness of the machine to prove termination
   is a sign that something is wrong (unless we are considering the
   memory test).

(In an earlier post I referred to the Goldbach Conjecture as the Goldbach
hypothesis.  My apology for the blunder.)
If the halting problem were solvable, then it could be used to decide any
mathematical problem involving only a countably infinite number of test
cases.  In addition to Fermat's Last Theorem, the Riemann Hypothesis and
Goldbach's Conjecture, I'd like to know whether or not there are any odd
perfect numbers....

-- Doug Quale



Sun, 31 Oct 1993 22:53:59 GMT  
 
 [ 24 post ]  Go to page: [1] [2]

 Relevant Pages 

1. I am not deaf, but am I mute?

2. Problem with my split routine I am not understanding

3. Halt doesn't halt.

4. halt/stop command not working

5. i do not want to halt main vi while executing sub vi

6. Is this solvable in functional programming?

7. Problem : Real raised to a real number

8. support@dyadic.com, is it not working, or am I not sending?

9. Problem with HALT Statement

10. HALTING PROBLEM

11. Apple Solves the Halting Problem!

12. Halting Problem

 

 
Powered by phpBB® Forum Software