Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!ncar!ico!auto-trol!davgot From: davgot@auto-trol.com (David Gottner) Newsgroups: comp.lang.misc Subject: Re: Halting Problem Solved! Film at 11! (Was Re: Message-ID: <1991May13.041310.26492@auto-trol.com> Date: 13 May 91 04:13:10 GMT References: <1991May9.205401.12382@auto-trol.com> Sender: news@auto-trol.com Organization: Auto-trol Technology Corporation Lines: 38 Nntp-Posting-Host: davgot In article stephen@estragon.uchicago.edu (Stephen P Spackman) writes: > >First of all, I would be more interested in a verifier that told me >about what my programme would do *if compiled* than one that told me >what it would do if run on a non-realisable machine. > You are right, a good verifier should be able to tell you approximately how much time/space overhead a program will require. (After all, humans can do this for algorithms, so a verifier should be able to do so also) However suppose the verifier said "This program will not halt on a machine with no more than 16 MB" Well, we can get a 32MB machine and run it. In otherwords if the verifier can show the program works or doesn't work on a machine with memory <= M, then we can run it on a machine with memory M+1. Thus, there is really no way to avoid Turing undecideability. >Secondly, your argument applies to languages as they are presently >defined; personally I wouldn't BOTHER writing a verifier for C (though >if I had one there are times when I'd use it). A *new* type system, >for instance, might be able to get very good mileage out of the >assumption that resources are finite (though I'd be very unhappy if it >assumed any PARTICULAR bound, I think). I wouldn't know, of course; >I'm no theorist. > >But I grant your point: a C programme could consume an unbounded >amount of stack and still be correct by the standard (though it would >take a VERY imaginative implementation to get the heap to contain >more than ULONG_MAX distinct objects, whatever ULONG_MAX is). > I don't think I'd want to use a language that placed limits on the number of active objects (unless it is a large limit like ULONG_MAX :-) ) -- David Gottner davgot@auto-trol.COM Auto-trol Technology Corporation {...}ncar!ico!auto-trol!younam 12500 North Washington Street (303) 252-2321 Denver, CO 80241-2404