comp.lang.ada
 help / color / mirror / Atom feed
From: max@gac.edu (Max Hailperin)
Subject: Re: What good is halting prob?
Date: 1995/04/20
Date: 1995-04-20T00:00:00+00:00	[thread overview]
Message-ID: <MAX.95Apr20162220@andretti.gac.edu> (raw)
In-Reply-To: dewar.798093453@gnat

In article <cppD77EIB.D79@netcom.com> cpp@netcom.com (Robin Rowe) writes:

   ..., it's still not clear what about 
   the halting problem is actually useful. How can it be used in design? What 
   problems does it help you solve?...

The way it is used in design is as a way to help you distinguish
between two situations that on the surface look very similar:

 1) You're trying to figure out how to program something, and can't
    figure out how -- everything you try runs into insurmountable
    obstacles.  You start to wonder whether the problem can be solved
    at all.  It turns out it can, you just need to approach it
    differently.

 2) You're trying to figure out how to program something, and can't
    figure out how -- everything you try runs into insurmountable
    obstacles.  You start to wonder whether the problem can be solved
    at all.  It turns out it can't, you need to find a way to live
    without a solution -- maybe by accepting some approximation.

When you hit that point of doubting whether the problem you're working
on is solvable, it is valuable to take some time off from trying to
solve it and instead try to prove it unsolvable.  If you succeed in
your proof, then you know you are in situation 2 and should work on
re-defining the problem instead of trying futilely to solve it. If you
fail in your proof, you may well have in the course of the failed
proof attempt done enough thinking about the problem in different ways
to be able to now approach solving it differently and succeed.

The way these proofs are usually constructed is by showing that if you
could solve the problem at hand, you could use that to solve the
halting problem.  Hence, since the halting problem is unsolvable, so
is the problem at hand.

Here's an example; this is a semi-plausible "real-life-ish" scenario;
I'm aware its not perfect in this regard, but its the best I could
come up with off the top of my head just now, and I hope that it will
help convince you that "really real" scenarios might arise:

J. Programmer is working on an package for arbitrary-precision
calculations.  The user is supposed to be able to select any of the
result values and request that it be redisplayed to a higher
precision, which the user gets to specify.

J. Programmer builds an approximation class (where each instance
represents some particular number to some particular precision), and
gives it a complete set of overloaded operations, so that you can do
things like add two approximations and get an approximation.  (The
precision of the resulting approximation is suitably derived from the
precision of the input approximations.)

After this is working, J.'s next step is an "arbitrary precision
number" class; each instance represents the abstract
precision-independent "essence" of a number, and supports an operation
which, when given the precision, will return an approximation of that
precision.  For example, if pi is an instance of this class, you can
ask pi for an approximation of itself good to within 10^-2, and get
back the approximation that would display as 3.14, or you can ask it
for an approximation of itself good to within 10^-5 and get back the
approximation that would display as 3.14159, etc.  The way this is
achieved varies from subclass to subclass; any given subclass of
arbitrary precision number needs some way of doing it, but it can
vary.  J. Programmer none the less can and does supply the abstract
super-class with a full complement of arithmetic operators; for
example, you can add any two arbitrary precision numbers and get an
arbitrary precision sum.  The way J. makes this work is that the sum
is of a subclass that has two instance variables, one for the augend
and one for the addend.  It provides an implementation for the "return
an approximation of yourself good to this precision" method, namely,
it turns around and asks the addend and augend for suitably more
precise approximations of themselves than is desired for the sum, and
then adds those approximations to get the approximation to the sum.

This general strategy works for operations other than addition as
well, and J. Programmer is busily buzzing along, picking off
operations one by one and implementing them for the general arbitrary
precision number class, until one day the == operator (i.e., equality
testing) comes to the top of the to-do list.  Nothing works.  In fact,
J. doesn't see any way it could be possible.  But, the last time
J. loudly declared a programming problem to be "impossible,"
C. Scientist from down the hall overheard and said "no, it's not
impossible, in fact, it's in Knuth."

So, remembering this, J. goes down the hall to see C.  C. says "yes,
this time I think you're right that its impossible -- I bet we can
reduce the halting problem to it."  The proof goes like this: if you
had some procedure (let's call it P) that you wanted to test to see
whether it halts, you could encapsulate it into an instance of a new
subclass of arbitrary precision number.  The way this subclass
implements the "return an approximation of yourself to this precision"
method is as follows: when asked to return an approximation good to
within 10^-n, it simulates execution of P for n steps, or until P
terminates, if it terminates in less than n steps.  If P terminated in
less than n steps, let's say in k steps, then the approximation
returned is 10^-k.  Otherwise, it is 0.  Now, if you had an ==
operator, you could just check whether this number was == to 0 [or
rather, to 0 converted to an arbitrary precision number].  If they are
equal, then P doesn't halt. If they aren't equal, then P does halt.
So, you've solved the halting problem!  So, since that's impossible,
it must be impossible to write a general == too.

Armed with this knowledge, J. Programmer now can stop trying to
implement == for arbitrary precision numbers, and instead work on
finding some way to live without them.




  parent reply	other threads:[~1995-04-20  0:00 UTC|newest]

Thread overview: 75+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
1995-03-17  0:24 Should internet support software be written in Ada? Bill Brooks
1995-03-17  8:47 ` Anthony Shipman
1995-03-19 22:06 ` David Weller
1995-03-23 15:05   ` Theodore Dennison
1995-03-24 10:26     ` Fred J. McCall
1995-03-27  9:50       ` Robb Nebbe
1995-03-27 19:43         ` State machines and Goto's (was Re: Should internet support software be written in Ada?) Robert I. Eachus
1995-03-27 23:14           ` Arthur Evans Jr
1995-03-29  0:00           ` Dan
1995-04-01  0:00             ` Mike White
1995-04-04  0:00               ` Robert Dewar
1995-04-06  0:00                 ` Theodore Dennison
1995-04-06  0:00                   ` Norman H. Cohen
1995-04-07  0:00                   ` Robert Dewar
1995-04-07  0:00                   ` Tucker Taft
1995-04-07  0:00                 ` Mike White
     [not found]                   ` <3ma7rt$smt@kaiwan009.kaiwan.com>
     [not found]                     ` <dewar.797514490@gnat>
     [not found]                       ` <3meunj$66u@felix.seas.gwu.edu>
1995-04-20  0:00                         ` CS teachers who can't code their way outta a paper bag Richard A. O'Keefe
1995-03-27 14:24       ` Should internet support software be written in Ada? Theodore Dennison
1995-03-28  0:00         ` Robert Dewar
1995-03-28  9:32         ` Fred J. McCall
1995-03-29  0:00           ` Theodore Dennison
1995-03-29  0:00   ` Robert I. Eachus
1995-03-31  0:00     ` Theodore Dennison
1995-04-05  0:00   ` Wes Groleau
1995-04-07  0:00   ` State machines and Goto's (was Re: Should internet support software be written in Ada?) Wes Groleau
1995-04-07  0:00     ` Robert Firth
     [not found]       ` <D6qyv0.6Jv@nntpa.cb.att.com>
1995-04-19  0:00         ` Fergus Henderson
1995-04-19  0:00           ` Fred J. McCall
1995-04-19  0:00             ` George Haddad
1995-04-20  0:00             ` Mark A Biggar
1995-04-20  0:00             ` State machines and Goto's (was Re: Sho Brian Hanson
1995-04-20  0:00             ` State machines and Goto's (was Re: Should internet support software be written in Ada?) Bill Winn
1995-04-20  0:00               ` Robert Dewar
1995-03-22 23:08 ` Should internet support software be written in Ada? Keith Thompson
     [not found] ` <dewar.798207931@gnat>
     [not found]   ` <cppD78ywq.B31@netcom.com>
     [not found]     ` <dewar.798240702@gnat>
1995-04-19  0:00       ` Problems with proofs Brian Harvey
1995-04-19  0:00         ` Robert Dewar
1995-04-20  0:00       ` Robin Rowe
1995-04-20  0:00         ` Robert Dewar
1995-04-21  0:00           ` Robin Rowe
1995-04-21  0:00             ` Robert Dewar
1995-04-20  0:00         ` Robert Dewar
1995-04-20  0:00         ` Steve Tate
1995-04-20  0:00           ` Apology to Steve Robin Rowe
1995-04-21  0:00         ` Problems with proofs Larry Kahn
1995-04-20  0:00       ` Robin Rowe
     [not found]     ` <3n1fsv$lgd@butch.lmsc.lockheed.com>
1995-04-20  0:00       ` Robin Rowe
1995-04-20  0:00         ` Garlington KE
     [not found] ` <dewar.798093453@gnat>
1995-04-20  0:00   ` Max Hailperin [this message]
     [not found] ` <3me1qs$n4a@theopolis.orl.mmc.com>
     [not found]   ` <3mevmu$8an@felix.seas.gwu.edu>
     [not found]     ` <3mh75i$8eu@rational.rational.com>
     [not found]       ` <3mjihr$iqq@felix.seas.gwu.edu>
     [not found]         ` <3mp20f$80t@kaiwan009.kaiwan.com>
1995-04-20  0:00           ` Academic CS Losers? Phillip Fanous
1995-04-21  0:00             ` Bill Winn
     [not found] ` <3mrv7h$3mq@larry.rice.edu>
     [not found]   ` <3msnu4$6am@kaiwan009.kaiwan.com>
     [not found]     ` <KUBEK.95Apr18213646@insage.gerii.insa-tlse.fr>
     [not found]       ` <cppD792GC.1uI@netcom.com>
1995-04-20  0:00         ` Teaching OO/C++ Philip Machanick
     [not found] ` <cppD75t6F.47M@netcom.com>
     [not found]   ` <EACHUS.95Apr17172831@spectre.mitre.org>
     [not found]     ` <cppD77Ex6.E77@netcom.com>
     [not found]       ` <3mve9b$gaj@news.cais.com>
1995-04-18  0:00         ` What good is halting prob? Jay M Martin
1995-04-19  0:00           ` Steve Tate
1995-04-20  0:00             ` Jay M Martin
1995-04-21  0:00               ` Steve Tate
1995-04-21  0:00             ` Ray Toal
     [not found]         ` <cppD7880n.32B@netcom.com>
1995-04-19  0:00           ` Randolph Crawford
1995-04-19  0:00             ` Robert Dewar
1995-04-20  0:00             ` Robin Rowe
1995-04-20  0:00               ` Robert Dewar
1995-04-20  0:00                 ` Robin Rowe
1995-04-21  0:00                   ` Brian Hanson
1995-04-21  0:00           ` sxc
     [not found]       ` <dewar.798172270@gnat>
     [not found]         ` <cppD786FM.1u9@netcom.com>
     [not found]           ` <dewar.798207364@gnat>
     [not found]             ` <cppD78xMv.49w@netcom.com>
1995-04-19  0:00               ` Robb Nebbe
     [not found]             ` <3n0ka7$b57@hermes.unt.edu>
     [not found]               ` <dewar.798232482@gnat>
1995-04-19  0:00                 ` Mark A Biggar
1995-04-19  0:00                   ` Robert Dewar
1995-04-19  0:00                   ` Steve Tate
1995-04-19  0:00           ` Mark A Biggar
1995-04-19  0:00             ` Richard Ladd Kirkham
1995-04-19  0:00               ` Robert Dewar
1995-04-20  0:00                 ` Richard Ladd Kirkham
1995-04-20  0:00                   ` Robert Dewar
1995-04-21  0:00               ` Mark A Biggar
1995-04-21  0:00       ` Robert I. Eachus
1995-04-21  0:00         ` Robert Dewar
replies disabled

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox