Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!mips!ptimtc!nntp-server.caltech.edu!mustang!data.nas.nasa.gov!sun418.nas.nasa.gov!truesdel From: truesdel@nas.nasa.gov (David A. Truesdell) Newsgroups: comp.lang.misc Subject: Re: Halting Problem Solved! Film at 11! (Was Re: definitions) Message-ID: Date: 6 May 91 01:57:22 GMT References: <333124@socrates.umd.edu> <30040@dime.cs.umass.edu> <1991May4.192440.5527@sctc.com> <30095@dime.cs.umass.edu> Sender: news@nas.nasa.gov Organization: NAS Program, NASA Ames Research Center, Moffett Field, CA Lines: 36 yodaiken@chelm.cs.umass.edu (victor yodaiken) writes: >If the halting problem applied to actual computers, then there would >be no bound on any algorithm to solve the problem. There is an obvious, >although impractical algorithm, however, so the invocation of Turing's >theorem is misplaced. Large numbers are not equal to infinite numbers, >hard problems are not equivalent to impossible problems. If you want to >say that deciding type problems for programing languages is unlikely >because the immense state spaces are not tractable to analysis, then fine. >But, if you want to say that Turing's theorem, or Herbrands theorem, >or Fermats theorem tells us that type checking real programs is >impossible, then you don't understand any of these theorems ( or you've >figured out something that it would be interesting to hear about). >>I would say that this is close enough to insoluble for government >>work, as the saying goes. Am I missing something in your post? I'd >While "hard = insoluble" may be close >enough for government work, it's not true. There may be a wonderful >algorithm out there that in practice can verify type safety of >very complex programs in a reasonable time. Is there such an >algorithm? I don't know. But I do know that there is no proof >that such an algorithm is impossible. It's getting fairly obvious that you don't really understand what the problem in the halting problem is. The halting problem does not exist because a turing machine has an potentially infinite state space and infinite storage. It arises from the fact that, for certain cases, the question "will this program reach the halting state" is inherently undecidable, even given infinite time. The physical limits of "actual computers" have no bearing on the problem. Your "obvious, although impractical algorithm" does not exist. -- T.T.F.N., dave truesdell (truesdel@nas.nasa.gov) 'And Ritchie said, "Let there be portability!" And nothing happened, so Ritchie realized that he had his work cut out for him.'