Path: utzoo!utgpu!news-server.csri.toronto.edu!cs.utexas.edu!asuvax!ncar!elroy.jpl.nasa.gov!sdd.hp.com!wuarchive!uunet!mcsun!ukc!slxsys!ibmpcug!mantis!mathew From: mathew@mantis.co.uk (CNEWS MUST DIE!) Newsgroups: comp.lang.misc Subject: Re: Will this *thread* ever halt? Message-ID: Date: 28 May 91 16:09:31 GMT References: <31051@dime.cs.umass.edu> Organization: Mantis Consultants, Cambridge. UK. Lines: 75 yodaiken@chelm.cs.umass.edu (victor yodaiken) writes: > Forgive me if I mistake your meaning, but this seems like complete nonsense. > The expression x> 10 does not constrain x to an "exact amount". No. It does, however, constrain x to be greater than some exact amount. As opposed to being greater than some fuzzily-defined amount which is approximately 10. > If emacs requires at least 4 meg of memory in order to run correctly, > then knowing that x>4meg is certainly good enough. It depends. It might require significantly more memory than that if you're editing large files. The amount of memory required by Emacs is not an exact amount. It depends what you're doing with the program. Part of the job of determining whether an ANSI C program will halt will involve placing exact bounds on how much memory it might use in running, and hence producing exact specifications of input values/conditions for which it might not terminate. And remember that a single byte might make a difference; so if it's December, your calendar program might fail to work properly whereas it worked fine in May, because somewhere the program is allocating space for the name of the month and this is resulting in its not having enough space to complete some other task. > The halting problem involves deterministic machines. It does not > involve predicting the time of day which you will chose to run > a program or the next word which I will type into a keyboard. I didn't mean to imply that it did. > A computer program can be considered to be a deterministic machine > computing a function on its input. You want to say that program behavior > is not deterministic, because the input is not deterministic. Generally, > however, we are less interested in predicting system input than in making > sure that the program can cope correctly with *every* possible input. Right. So in addition, your Terminating ANSI C has to check whether all possible return values from standard library calls will result in termination or not. For example, if the program uses time.h, we must check to see that it terminates for all possible start times. Basically, it adds another dimension of complexity to the problem. > >You said "an arbitrary C program". Not "an arbitrary C program which is not > >allowed to look at the system time". > > Here, I'm considering the program as a function with input varying over > its domain. In this case, consider the domain to be the set of possible > time values. We don't want to attempt to predict which elements of this > domain will be encountered: i.e., we don't want to try to predict the > time of day when the program will be run. We just want to make sure that > the program behaves "correctly" for any time value. Right. That's fine. Basically, for any moderately complicated ANSI C program the dimensions of the input domain and the range of each dimension will be so large that trying all combinations will be infeasible on even the largest computers. I'll leave it to someone else to do some sums to demonstrate this. In short, determining the halting status of ANSI C programs is not feasible for real programs; and it's not possible for general ANSI C programs, because general ANSI C programs might have arbitrarily large input spaces making analysis require impossible amounts of memory and CPU time. If you want to write programs and be told whether they will halt or not, you will have to use a different language; one which is restricted so that you don't have to rely on brute-force methods for determining halting status. For example, a functional language which uses map operations (iteration over a structure) rather than while loops and which limits general recursion. mathew