Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!think.com!zaphod.mps.ohio-state.edu!mips!apple!netcomsv!doug
From: doug@netcom.COM (Doug Merritt)
Newsgroups: comp.lang.misc
Subject: Re: Halting Problem Solved! Film at 11! (Was Re:
Message-ID: <1991May27.185155.6956@netcom.COM>
Date: 27 May 91 18:51:55 GMT
References: <3354@optima.cs.arizona.edu> <1991May25.135757.6912@sbcs.sunysb.edu>
Organization: Netcom - Online Communication Services  UNIX System {408 241-9760 guest}
Lines: 66

In article <1991May25.135757.6912@sbcs.sunysb.edu> jallen@eeserv1.ic.sunysb.edu (Joseph Allen) writes:
> [...]  The 64K question is can it be done symbolically on the
>language source code.  I believe the answer is sometimes.  If you don't have
>malloc and you don't have other forms of bignums then it might even be
>practicle.  Maybe.  It would be usefull because you could tell at compile time
>if you're going to overflow or go past array bounds or run out of stack space.

Bignums and malloc are important in the theoretical sense in which they
were brought up in this thread, but eliminating their consideration doesn't
help all that much in practice.

>At any rate, the halting problem proof should not be justification to not at
>least research this.

It gets researched all the time, the halting problem notwithstanding. It
is quite frequent to see papers that discuss heuristics, or actually more
often ones that assume certain simplifications that allow some progress
to be made, but which make the algorithm in question useless for general
application because of the difficulty/impossibility of proving that
the assumption holds for any particular real-world case.

If you actually try to design an analyzer that e.g. tries to predict whether
an array index will ever go out of bound (as good an example as any), you
almost always end up modeling behavior which is highly input-data-dependent,
dependent on the results of other function calls (whether they were called
or how often and what they computed), etc. In short you get a model which
represents significant chunks of the original program, with very few
possible simplifications, and hence can't make much progress.

A great deal of the work on this subject comes up under the heading "symbolic
execution", and it *is* useful, just not as much as you would like to hope.
Another related area is "the aliasing problem", which refers to the
problem of figuring out when/whether two names (or pointers, depending
on the language/problem being analyzed) refer to the same memory cell(s).
It turns out that a lot hangs on this, and an awful lot of people would
be very happy if some general solution to this could be found. Unfortunately
in most forms it maps to the halting problem, or impractical simplifying
assumptions need to be made.

So although it is generally thought to be hopeless in the completely
general case, people do tackle subsets, and some people hope that eventually
some significantly powerful subset of the problem may prove tractable.
But still, the halting problem says that you'll never get a hundred percent
solution.

Oh, btw: another interesting related problem is that there is no
"normalized form" for algorithms in any of the universal models of computation
developed thus far. I.e. you can express, say, a shell sort in any of
numerous different ways, and within broad limits, no single one of those
forms can be called "the base case"/"the natural form"/"the simplest form".
This means that even so simple a concept as trying to compare two algorithms
for functional equality is intractable. In number theory, positive numbers
have a unique factorization, and this makes a lot of things very tractable.
But most other things (e.g. general two- and multi- dimensional polynomials)
have no unique factorization. They can be factored several different ways.
And that significantly complicates things. Same thing with algorithms.

So if you discovered a universal model of computation that *did* have
a unique factorization, then that would be a breakthrough. Much would
become possible within that system. Only problem is that it would necessarily
be intractable or impossible to automatically translate algorithms from
other systems into that one, which probably means that it would be very
difficult to prove that it really was a universal model of computation.
	Doug
-- 
Doug Merritt	doug@netcom.com		apple!netcom!doug